issues
search
lean-ja
/
lean-by-example
コード例で学ぶ Lean 言語
https://lean-ja.github.io/lean-by-example/
MIT License
15
stars
5
forks
source link
ac_rfl で n + 0 = n が示せる…?
#372
Open
Seasawher
opened
1 week ago
Seasawher
commented
1 week ago
なんでやねん(rfl が通らない状況でも通るので、可換性を暗黙に使ってる?)
なんでやねん(rfl が通らない状況でも通るので、可換性を暗黙に使ってる?)