search

leanprover / theorem_proving_in_lean4

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

Fix creation of Trans instance in calculational proof section #83

Open Shiney opened 11 months ago

Shiney commented 11 months ago

Two issues,

If you use the code as written it doesn't have the right type for Trans, also there's a clash with the existing | operator