Lean4 チートシート

情報の抽出

• ゴールの抽出：Lean.Elab.Tactic.getMainGoal

  これは let goal ← Lean.Elab.Tactic.getMainGoal のように使います。

• メタ変数からの宣言の抽出：mvarId.getDecl、ここで mvarId : Lean.MVarId がコンテキストにあるとします。例えば、ゴールの mvarId は getMainGoal を使用して抽出することができます。

• メタ変数の型の抽出：mvarId.getType、ここで mvarId : Lean.MVarId がコンテキストにあるとします。

• メインのゴールの型の抽出：Lean.Elab.Tactic.getMainTarget

  これは let goal_type ← Lean.Elab.Tactic.getMainTarget のように使います。

  これは下記と同じ結果になります。

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

• ローカルコンテキストの抽出：Lean.MonadLCtx.getLCtx

  これは let lctx ← Lean.MonadLCtx.getLCtx のように使います。

• 宣言の名前の抽出：Lean.LocalDecl.userName ldecl、ここで ldecl : Lean.LocalDecl がコンテキストにあるとします。

• 式の型の抽出：Lean.Meta.inferType expr、ここで expr : Lean.Expr がコンテキストにあるとします。

  これは let expr_type ← Lean.Meta.inferType expr のように使います。

式で遊ぶ

• 宣言を式に変換する：Lean.LocalDecl.toExpr

  これは ldecl : Lean.LocalDecl がコンテキストにある場合に ldecl.toExpr のように使います。

  この ldecl は例えば、let ldecl ← Lean.MonadLCtx.getLCtx などで取得されます。

• 2つの式が definitionally equal かどうかのチェック：Lean.Meta.isDefEq ex1 ex2、ここで ex1 ex2 : Lean.Expr がコンテキストにあるとします。これは Lean.MetaM Bool を返します。

• ゴールを閉じる：Lean.Elab.Tactic.closeMainGoal expr、ここで expr : Lean.Expr がコンテキストにあるとします。

さらなるコマンド

• メタ-sorry：Lean.Elab.admitGoal goal、ここで goal : Lean.MVarId がコンテキストにあるとします。

表示とエラー

• 通常の用途での「永久な」メッセージの表示：

  Lean.logInfo f!"Hi, I will print\n{Syntax}"

• デバッグ中のメッセージの表示：

  dbg_trace f!"1) goal: {Syntax_that_will_be_interpreted}".

• 例外を投げる：Lean.Meta.throwTacticEx name mvar message_data、ここで name : Lean.Name はタクティクの名前で mvar はエラーのデータを保持しているとします。

  これは Lean.Meta.throwTacticEx `tac goal (m!"unable to find matching hypothesis of type ({goal_type})") のように用い、ここでフォーマッタ m! は項をより見やすく表示する MessageData を構築します。

TODO: Add?

• Lean.LocalContext.forM
• Lean.LocalContext.findDeclM?