CommandElab

Lean.Elab.Command.CommandElab は、コマンドの内部実装を表現しています。

CommandElab 型の項は、Syntax → CommandElabM Unit 型の関数です。

import Lean

open Lean Elab Command in

example : CommandElab = (Syntax → CommandElabM Unit) := rfl

[command_elab] 属性を利用することで、CommandElab 型の関数からコマンドを作ることができます。

/-- 挨拶をするコマンド -/
syntax (name := helloCommand) "#hello" : command

open Lean Elab Command in

@[command_elab helloCommand]
def evalHello : CommandElab := fun _stx => do
  let msg := s!"Hello, Lean!"
  logInfo msg

/- info: Hello, Lean! -/
#hello

コマンド作例

以下に、CommandElab 型の関数からコマンドを作る例を示します。

型を確かめるコマンド

以下は、与えられた項と型が一致するかどうかを確かめるコマンドの例です。¹

import Lean

open Lean Elab Command Term

-- メタ変数を表示しない
set_option pp.mvars false

/-- 与えられた項の型をチェックするコマンド -/
syntax (name := assertType) "#assert_type " term " : " term : command

@[command_elab assertType]
def evalAssertType : CommandElab := fun stx => do
  match stx with
  | `(command| #assert_type $termStx : $typeStx) =>
    liftTermElabM
      try
        let type ← elabType typeStx
        let _ ← elabTermEnsuringType termStx type
        logInfo "success"
      catch | _ => throwError "failure"
  | _ => throwUnsupportedSyntax

/- info: success -/
#assert_type 5 : Nat

/- info: success -/
#assert_type 42 : ?_

/-
error: Type mismatch
  [1, 2, 3]
has type
  List ?_
but is expected to have type
  Nat
-/
#assert_type [1, 2, 3] : Nat

---

1. このコード例は、Metaprogramming in Lean 4 を参考にしました。 ↩