@[inline]

def StrataDDM.Lean.arrayToExpr (level : Lean.Level) (type : Lean.Expr) (a : Array Lean.Expr) : Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Lean.listToExpr (level : Lean.Level) (type : Lean.Expr) (es : List Lean.Expr) : Lean.Expr

Equations

• StrataDDM.Lean.listToExpr level type es = List.foldr (Lean.mkApp2 (Lean.mkApp (Lean.mkConst `List.cons [level]) type)) (Lean.mkApp (Lean.mkConst `List.nil [level]) type) es

@[inline]

def StrataDDM.Lean.optionToExpr (type : Lean.Expr) (a : Option Lean.Expr) : Lean.Expr

Equations

• StrataDDM.Lean.optionToExpr type none = Lean.mkApp (Lean.mkConst `Option.none [Lean.levelZero]) type
• StrataDDM.Lean.optionToExpr type (some a_2) = Lean.mkApp2 (Lean.mkConst `Option.some [Lean.levelZero]) type a_2