search

lean-ja / lean-by-example

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

metaprogramming book: 何をもって同じ expression とみなすのか #254

Open Seasawher opened 2 weeks ago

Seasawher commented 2 weeks ago

MetaMの章に「～に相当する expression を作れ」という問題がいくつかあるが，どういうテストコードを満たせばよいのかが不明

  1. eval ppExpr の結果が同じものになることを目標にすると，そもそも模範解答が間違いになる

  2. isDefEq の Expr なら良いかというと，それは違いそうに思える（大雑把すぎる）
Seasawher commented 2 weeks ago

＋とか∀とかをきちんと表示させることは (universe level とかインスタンスとかをきちんと指定すれば)可能なので，ppExpr の表示結果が exact に同じものになることをもって「同じ expression」 とみなすのがよさそう

Seasawher commented 2 weeks ago

完全に解いた例

https://gist.github.com/spinylobster/82ccc15982e36660e8021a7374f5d62b