def Lean.Meta.Sym.inferType (e : Expr) : SymM Expr

Returns the type of e.

Equations

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

def Lean.Meta.Sym.getLevel (type : Expr) : SymM Level

If type : sort and sort reduces to Sort u for some u, then getLevel type returns u.

If sort is an assignable MVar, then getLevel type produces a fresh level metavariable ?u, assigns the MVar to Sort ?u and returns ?u.

Equations

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

def Lean.Meta.Sym.mkEqRefl (e : Expr) : SymM Expr

Equations

• Lean.Meta.Sym.mkEqRefl e = do let α ← Lean.Meta.Sym.inferType e let u ← Lean.Meta.Sym.getLevel α pure (Lean.mkApp2 (Lean.mkConst `Eq.refl [u]) α e)