def LeanSubst.Subst.Syntax.MetaM.promote {α : Type} (x : Lean.MetaM α) : Lean.Elab.TermElabM α

Equations

• LeanSubst.Subst.Syntax.MetaM.promote x = liftM x

def LeanSubst.Subst.Syntax.form_list : List Lean.Expr → Lean.Elab.TermElabM (Lean.TSyntax `term)

Equations

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

def LeanSubst.Subst.Syntax.form_prod (b : Lean.Elab.TermElabM (Lean.TSyntax `term)) : List Lean.Expr → Lean.Elab.TermElabM (Lean.TSyntax `term)

Equations

• One or more equations did not get rendered due to their size.
• LeanSubst.Subst.Syntax.form_prod b [] = b

def LeanSubst.Subst.Syntax.get_ty_arg (e : Lean.Elab.TermElabM Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Equations

• LeanSubst.Subst.Syntax.get_ty_arg e = do let e ← e match e with | fn.app ty => pure ty | x => Lean.Elab.throwUnsupportedSyntax