search

dselsam / binport

A tool for building Lean4 .olean files from Lean3 export data
Apache License 2.0
10 stars 1 forks source link

Aligning `dite`/`ite` #16

Closed dselsam closed 3 years ago

dselsam commented 3 years ago

Fixes not yet merged:

dselsam commented 3 years ago

https://github.com/leanprover-community/lean/commit/c248e38671ebca7d0513180887daf60a6433bc37 https://github.com/leanprover-community/mathlib/commit/0035e2dd30b71232b3bf7d0827eeaa0c002c1825