search

leanprover / theorem_proving_in_lean4

Theorem Proving in Lean 4
https://leanprover.github.io/theorem_proving_in_lean4/
Apache License 2.0
164 stars 92 forks source link

"Coercion" confuses newbies #63

Closed VhRvo closed 5 months ago

VhRvo commented 1 year ago

This book doesn't mention this coercion, I think we should write it explicitly.