source
def Lean.Meta.CheckTactic.mkCheckGoalType (val type : Expr) :
MetaM Expr
Equations

- Lean.Meta.CheckTactic.mkCheckGoalType val type = do let lvl ← Lean.Meta.mkFreshLevelMVar pure (Lean.mkApp2 (Lean.mkConst `Lean.Meta.CheckTactic.CheckGoalType [lvl]) type val)

Instances For

source
def Lean.Meta.CheckTactic.matchCheckGoalType (stx : Syntax) (goalType : Expr) :
MetaM (Expr × Expr × Level)
Equations

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

Instances For