search

lean-ja / lean-by-example

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

糖衣構文の展開結果を確かめるには？ #328

Closed Seasawher closed 3 months ago

Seasawher commented 3 months ago

一般に exists e₁, e₂, .. は refine ⟨e₁, e₂, ..⟩; try trivial の糖衣構文です．

exists の項でこのように書いたが、これを確かめるコード例がない。タクティクに展開されるマクロがあったとして、その展開結果を確かめるにはどうしたらよいだろう？

Seasawher commented 3 months ago

see: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/see.20result.20of.20tactic.20macro/near/446289064

Seasawher commented 3 months ago

353 と関連していて，これで可能

set_option trace.Elab.step true

example : ∃ x : Nat, x = 1 := by
  /-
  [Elab.step] exists 1 ▼
    [] exists 1 ▼
    [] exists 1 ▼
    [] (refine ⟨1, ?_⟩; try trivial) ▼
    [] refine ⟨1, ?_⟩; try trivial ▼
    [] refine ⟨1, ?_⟩; try trivial ▶
  -/
  exists 1
Seasawher commented 3 months 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