def Lean.Meta.CheckTactic.mkCheckGoalType (val : Lean.Expr) (type : Lean.Expr) : Lean.MetaM Lean.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 : Lean.Syntax) (goalType : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr × Lean.Level)

Equations

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