Lean4 Cheat-sheet

Extracting information

Extract the goal: Lean.Elab.Tactic.getMainGoal

Use as let goal ← Lean.Elab.Tactic.getMainGoal
Extract the declaration out of a metavariable: mvarId.getDecl when mvarId : Lean.MVarId is in context. For instance, mvarId could be the goal extracted using getMainGoal
Extract the type of a metavariable: mvarId.getType when mvarId : Lean.MVarId is in context.
Extract the type of the main goal: Lean.Elab.Tactic.getMainTarget

Use as let goal_type ← Lean.Elab.Tactic.getMainTarget

Achieves the same as

let goal ← Lean.Elab.Tactic.getMainGoal
let goal_type ← goal.getType

Extract local context: Lean.MonadLCtx.getLCtx

Use as let lctx ← Lean.MonadLCtx.getLCtx
Extract the name of a declaration: Lean.LocalDecl.userName ldecl when ldecl : Lean.LocalDecl is in context
Extract the type of an expression: Lean.Meta.inferType expr when expr : Lean.Expr is an expression in context

Use as let expr_type ← Lean.Meta.inferType expr

Convert a declaration into an expression: Lean.LocalDecl.toExpr

Use as ldecl.toExpr, when ldecl : Lean.LocalDecl is in context

For instance, ldecl could be let ldecl ← Lean.MonadLCtx.getLCtx
Check whether two expressions are definitionally equal: Lean.Meta.isDefEq ex1 ex2 when ex1 ex2 : Lean.Expr are in context. Returns a Lean.MetaM Bool
Close a goal: Lean.Elab.Tactic.closeMainGoal expr when expr : Lean.Expr is in context

meta-sorry: Lean.Elab.admitGoal goal, when goal : Lean.MVarId is the current goal

Print a "permanent" message in normal usage:

Lean.logInfo f!"Hi, I will print\n{Syntax}"
Print a message while debugging:

dbg_trace f!"1) goal: {Syntax_that_will_be_interpreted}".
Throw an error: Lean.Meta.throwTacticEx name mvar message_data where name : Lean.Name is the name of a tactic and mvar contains error data.

Use as Lean.Meta.throwTacticEx tac goal (m!"unable to find matching hypothesis of type ({goal_type})")where them!formatting builds aMessageData` for better printing of terms

TODO: Add?