|
|
e1fc6b609d
|
Add the extensional representation of pair&abs equality rules
|
2025-04-17 15:22:45 -04:00 |
|
Yiyun Liu
|
b3bd75ad42
|
Fix the typing rules
|
2025-03-03 01:38:22 -05:00 |
|
Yiyun Liu
|
687d1be03f
|
Finish preservation
|
2025-02-25 22:35:59 -05:00 |
|
Yiyun Liu
|
96bc223b0a
|
Finish renaming and preservation
|
2025-02-25 20:18:40 -05:00 |
|
|
|
b2aec9c6ce
|
Add syntactic typing rules
|
2025-02-25 16:06:04 -05:00 |
|
|
|
4dd2cd7cd8
|
Finish indzero and indsuc rules
|
2025-02-25 15:46:22 -05:00 |
|
Yiyun Liu
|
ea1fba8ae9
|
Finish syntactic renaming
|
2025-02-09 20:41:27 -05:00 |
|
|
|
881b2e3825
|
Add missing premise
|
2025-02-09 17:05:43 -05:00 |
|
|
|
5b925e3fa1
|
Add beta and eta rules to syntactic typing
|
2025-02-09 16:33:43 -05:00 |
|
|
|
ab1bd8eef8
|
Add semantic rules for function beta and eta
|
2025-02-09 16:12:57 -05:00 |
|
Yiyun Liu
|
4396786701
|
Reformulate renaming
|
2025-02-08 22:56:45 -05:00 |
|
Yiyun Liu
|
0c83044d72
|
Update the typing rules with projections
|
2025-02-08 22:45:07 -05:00 |
|
|
|
0e5b82b162
|
Move projection axioms to the subtyping relation
|
2025-02-06 21:40:26 -05:00 |
|
|
|
2e2e41cbe6
|
Add missing Univ rule
|
2025-02-06 18:15:25 -05:00 |
|
|
|
6daa275ac8
|
Prove the fundamental theorem
|
2025-02-06 18:09:19 -05:00 |
|
|
|
399c97fa82
|
Add the semantic well-typedness rules to the hint db
|
2025-02-06 17:58:38 -05:00 |
|
|
|
8d92f19d74
|
Add all(?) typing rules
|
2025-02-06 17:47:34 -05:00 |
|
|
|
10f339c5b6
|
Add some syntactic typing rules
|
2025-02-06 17:00:04 -05:00 |
|
