|
|
226b196d15
|
Refactor half of fp_red
|
2025-03-02 17:35:51 -05:00 |
|
|
|
657c1325c9
|
Add unscoped syntax
|
2025-03-02 16:40:39 -05:00 |
|
Yiyun Liu
|
133bcd55c2
|
Need to fix gamma eq
|
2025-02-25 12:48:42 -05:00 |
|
|
|
fd0b48073d
|
Add nat type definition
|
2025-02-21 13:23:38 -05:00 |
|
|
|
38a0416b2c
|
Add a constant to avoid kripke LR
|
2025-02-04 22:14:27 -05:00 |
|
|
|
d9b5ef1267
|
Refactor the impossible case proof
|
2025-02-04 15:06:17 -05:00 |
|
|
|
6cc3a65163
|
Discharge one case of antirenaming using injective renaming
|
2025-02-02 19:42:42 -05:00 |
|
|
|
9f80013df6
|
Add tstar to preserve eta normal forms
|
2025-01-27 16:44:48 -05:00 |
|
Yiyun Liu
|
2f04bcc75c
|
Add a mostly finished eta postponement proof
|
2025-01-25 16:08:21 -07:00 |
|
