メタプロ：Syntax から Expr 型の値を得る

lean-ja / lean-by-example

コード例で学ぶ Lean 言語

https://lean-ja.github.io/lean-by-example/

MIT License

15 stars 5 forks source link

メタプロ：Syntax から Expr 型の値を得る #352

Open Seasawher opened 1 week ago

Seasawher commented 1 week ago

#eval show Lean.Elab.Term.TermElabM _ from do
  let a ← `(?a = 1)
  let stx : Syntax ← `($a ∨ ?b)
  let expr ← Elab.Term.elabTermAndSynthesize stx none
  dbg_trace ← ppExpr expr -- ?a✝ = 1 ∨ ?b✝