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

Returns the type of e.

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.

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