theorem_proving_in_lean4 icon indicating copy to clipboard operation
theorem_proving_in_lean4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

Fix creation of Trans instance in calculational proof section

Open Shiney opened this issue 1 year ago • 0 comments

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

Shiney avatar Oct 25 '23 20:10 Shiney