def Lean.MVarId.safeAssign (mvarId : MVarId) (val : Expr) : MetaM Unit

Variant of Batteries' Lean.MVarId.assignIfDefEq, using MVarId.checkedAssign (even safer).

Equations

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

def Lean.MVarId.assignTypeclassInstance (mvarId : MVarId) : MetaM Unit

Equations

• mvarId.assignTypeclassInstance = do let __do_lift ← mvarId.getType let __do_lift ← Lean.Meta.synthInstance __do_lift mvarId.safeAssign __do_lift

def Lean.Expr.sanitize (val : Expr) : MetaM Expr

This function applies sanitization on expressions to avoid common footguns. There are (at least) two footguns while working with expressions:

• uninstantiated metavariables
• metadata These may cause functions such as getAppFnArgs to fail, although when printing the expressions, they should clearly succeed: indeed, the pretty-printer instantiate metavariables first, preventing the success from any debugging attempts. To improve the debugging experience, one may use the option

set_option pp.instantiateMVars false To avoid problems in the first place, one may use this function pervasively.

Equations

• val.sanitize = do let __do_lift ← Lean.instantiateMVars val pure __do_lift.consumeMData

def prepend (s : String) (n : Lean.Name) : Lean.Name

Equations

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

def makeTuple (arr : Array Lean.Expr) : Lean.MetaM Lean.Expr

Equations

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