search

dselsam / binport

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

Control #19

Closed dselsam closed 3 years ago

dselsam commented 3 years ago

Currently, applicative and monad cannot be aligned because the seq_left and seq_right classes changed to require the discarded computation to return punit. This is not a major problem, but there is some category theory in mathlib that uses applicative and monad and so the two barely-different versions would need to persist in mathlib4. I think backporting the change would be simple (here is a starting point: https://github.com/dselsam/lean3/commit/7e8ead2c0d371ddacef7db30e7dd68d52f4b768f) but Mario thinks it would be a change for the worse (https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/mathport/near/226098511) and wonders if the rationale for the change even still applies (https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/mathport/near/226098127).

dselsam commented 3 years ago

There is an open PR by Sebastian reverting the lean4 change: https://github.com/leanprover/lean4/pull/311 This should resolve the issue.

dselsam commented 3 years ago

leanprover/lean4#311 was merged and alignment went smoothly