Leonardo de Moura
|
51e7f45af2
|
refactor: cases
remove dead `induction/cases` code
|
2021-03-07 12:37:02 -08:00 |
|
Leonardo de Moura
|
79a4aebf96
|
feat: add byCases tactic
|
2021-02-17 13:03:24 -08:00 |
|
Leonardo de Moura
|
7723953188
|
chore: use instance (priority := <prio>)
|
2020-12-21 10:17:54 -08:00 |
|
Leonardo de Moura
|
a4901f131b
|
feat: mark propDecidable as a scoped instance
|
2020-12-16 10:45:49 -08:00 |
|
Leonardo de Moura
|
f33473a39e
|
chore: use exists notation
|
2020-12-05 16:50:01 -08:00 |
|
Leonardo de Moura
|
b72a3c69b6
|
fix: ambiguity at induction/cases
See efc3a320fe
|
2020-11-24 14:59:12 -08:00 |
|
Leonardo de Moura
|
304c80d610
|
feat: use <|
|
2020-11-19 09:03:38 -08:00 |
|
Leonardo de Moura
|
c665d5e20a
|
chore: cleanup
|
2020-11-10 15:40:00 -08:00 |
|
Leonardo de Moura
|
7f364feeb5
|
chore: add Classical.lean, Equivalence, and cleanup
|
2020-11-10 14:55:34 -08:00 |
|