Denis Buzdalov
|
a3542ad0cd
|
[ cleanup ] Make existing equality proofs a bit cleaner
|
2022-05-20 11:50:46 +01:00 |
|
André Videla
|
10b9685e4b
|
Injective interface and its implementations (#2114)
Co-authored-by: Nick Drozd <nicholasdrozd@gmail.com>
|
2021-11-26 10:55:17 +00:00 |
|
Denis Buzdalov
|
927c358bef
|
[ base ] Some lacking implementations for Uninhabited were added
|
2021-06-15 15:07:54 +03:00 |
|
Stiopa Koltsov
|
7264d40c56
|
Make isElem, DecEq public, not just export
... so they could be used in proof search.
Follow-up to #942
|
2021-01-18 10:37:57 +00:00 |
|
Stiopa Koltsov
|
b76c9d91e0
|
Remove trailing whitespaces and add trailing newlines
|
2021-01-16 10:00:03 +00:00 |
|
Alex Gryzlov
|
69612bf6bf
|
Add list lemmas (#491)
|
2020-07-29 10:51:07 +01:00 |
|
Nick Drozd
|
6519b5608d
|
Further simplify List
|
2020-07-12 21:00:33 -05:00 |
|
Edwin Brady
|
dec7dff622
|
Add libraries
|
2020-05-18 14:00:08 +01:00 |
|