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)

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.