search

gebner / hott3

HoTT in Lean 3
Apache License 2.0
75 stars 11 forks source link

fix unit.rec_on in init/trunc.lean #12

Closed forked-from-1kasper closed 6 years ago

forked-from-1kasper commented 6 years ago

In Lean now unit is an abbreviation for punit (https://github.com/leanprover/lean/commit/3fefe947574d0133fcbf96eda17330e929b76f59), so we need to replace unit.rec_on withpunit.rec_on to avoid errors.

fpvandoorn commented 6 years ago

Thanks, I merged it.