search

lean-ja / lean-by-example

コード例で学ぶ Lean 言語
https://lean-ja.github.io/lean-by-example/
MIT License
15 stars 5 forks source link

オプション `trace.Elab.step` でマクロ展開を確認する #353

Open Seasawher opened 1 week ago

Seasawher commented 1 week ago 
open Lean
syntax (name := myExfalsoParser) "myExfalso" : tactic

-- remember that `Macro` is a synonym for `Syntax -> TacticM Unit`
@[macro myExfalsoParser] def implMyExfalso : Macro :=
fun stx => `(tactic| apply False.elim)

set_option trace.Elab.step true

example (p : Prop) (h : p) (f : p -> False) : 3 = 2 := by
  myExfalso
  exact f h
Seasawher commented 1 week ago

Zulip: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Multi.20commands.20macro/near/368144284

Seasawher commented 1 week ago

なんとコマンドを自分で定義すれば検証できることがわかった！

import Lean

open Lean

elab "#tactic_expand " t:tactic : command => do
  let some t ← Elab.liftMacroM <| Lean.Macro.expandMacro? t | logInfo m!"Not a macro"
  logInfo m!"{t}"

/-- info: (refine ⟨1, ?_⟩; try trivial) -/
#guard_msgs in #tactic_expand exists 1