atttibute [coe]でインフォビュー上での表示を↑に換える

lean-ja / lean-by-example

コード例で学ぶ Lean 言語

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

MIT License

15 stars 5 forks source link

Open Seasawher opened 2 weeks ago

Seasawher commented 2 weeks ago

MILで，CoeFun の表示を変えるという話があった

Seasawher commented 2 weeks ago

Nat.succ を Coe ぽく表示できる

attribute [coe] Nat.succ
#check Nat.succ 1