Commit 2022-10-25 00:59 2f2b44ae
View on Github →feat: Port Logic.Nonempty (#487)
- depends on: #484
- Deleted
nonempty_empty
sincestd4
now has that asnot_nonempty_empty
and as a simp lemma - Added an import to access
Zero
forZero.Nonempty
- Could not provide a
One.Nonempty
becauseOne
isn't defined yet - Used mathport's implicit type params, not sure what the style guidelines are
- Gave previously anonymous instances names:
Prod.Nonempty
,Pi.Nonempty