|
|
6d9ed23de9
|
Add the boolean extension without junk rules
|
2025-01-11 00:17:04 -05:00 |
|
|
|
53bef034ad
|
Add the "junk" rules for boolean
|
2025-01-10 22:28:53 -05:00 |
|
|
|
bec803949f
|
Finish Par and RPar lemmas
|
2025-01-10 20:51:59 -05:00 |
|
|
|
b750ea4095
|
Initial commit (still tweaking the rules)
|
2025-01-10 16:51:49 -05:00 |
|
|
|
0f1e85c853
|
Prove injectivity of Pair and Lambdas
|
2025-01-10 13:31:58 -05:00 |
|
|
|
fd8335a803
|
Add injectivity for pairs
|
2025-01-10 12:39:47 -05:00 |
|
|
|
34a0c2856e
|
Prove most of the confluence results for eta reduction
|
2025-01-09 20:21:38 -05:00 |
|
|
|
e75d7745fe
|
Finish normalization
|
2025-01-09 16:17:38 -05:00 |
|
|
|
0d3b751a33
|
.
|
2025-01-09 15:16:05 -05:00 |
|
|
|
7021497615
|
Finish adequacy
|
2025-01-09 15:15:11 -05:00 |
|
Yiyun Liu
|
bf2a369824
|
Generalize the model to talk about termination
|
2025-01-09 00:35:46 -05:00 |
|
Yiyun Liu
|
ec03826083
|
Add beta without the junk rules
|
2025-01-08 19:47:54 -05:00 |
|
|
|
9ab338c9e1
|
Add wn
|
2025-01-08 15:31:40 -05:00 |
|
|
|
602fe929bc
|
Add pars_var_inv
|
2025-01-05 00:21:19 -05:00 |
|
|
|
05d330254e
|
Fix ERed
|
2025-01-04 23:59:21 -05:00 |
|
|
|
a6fd48c009
|
Finish prov_extract
|
2025-01-04 23:38:44 -05:00 |
|
|
|
919f1513ce
|
Show that prov is preserved by beta red and eta exp
|
2025-01-04 23:02:12 -05:00 |
|
|
|
f0da5c97bb
|
Show that rpar preserves prov
|
2025-01-04 20:38:04 -05:00 |
|
|
|
ee7be7584c
|
Remove unnecessary usage of Equations
|
2025-01-04 16:56:21 -05:00 |
|
|
|
9a52ab334f
|
Finish all cases
|
2024-12-31 00:04:20 -05:00 |
|
|
|
a4682dedbe
|
Prove all except the proj2 case
|
2024-12-30 23:43:15 -05:00 |
|
|
|
708cac5d53
|
Finish all except the sigma case
|
2024-12-30 23:00:31 -05:00 |
|
|
|
2f68e6c87c
|
Finish structural rules
|
2024-12-30 22:07:35 -05:00 |
|
|
|
5347d573b5
|
Add semwt and its renaming lemmas
|
2024-12-30 21:43:41 -05:00 |
|
|
|
1a9cd6bda9
|
Start refactoring the logrel to include only closed terms
|
2024-12-30 20:46:43 -05:00 |
|
|
|
dd63ebf2e9
|
Prove that beta-eta equivalent types have the same meaning
|
2024-12-30 15:52:35 -05:00 |
|
|
|
86b8043215
|
Prove the pi case for interpext_join
|
2024-12-30 14:11:43 -05:00 |
|
|
|
d12de328b6
|
Generalize ProdSpace to BindSpace
|
2024-12-30 13:12:52 -05:00 |
|
Yiyun Liu
|
2fe0d33592
|
Minor
|
2024-12-29 22:36:15 -05:00 |
|
Yiyun Liu
|
6eba80ed70
|
Combine the different prov cases into one function
|
2024-12-29 22:33:37 -05:00 |
|
Yiyun Liu
|
8fc90f5935
|
Save
|
2024-12-27 14:32:41 -05:00 |
|
Yiyun Liu
|
1fd0ffe04d
|
Minor
|
2024-12-27 12:15:44 -05:00 |
|
Yiyun Liu
|
7f4c31b14e
|
Generalize Pi to TBind so we have both sigma and pi
|
2024-12-27 12:12:19 -05:00 |
|
Yiyun Liu
|
368c83dd8e
|
Add the statement that the logrel respects beta eta laws
|
2024-12-27 02:09:34 -05:00 |
|
Yiyun Liu
|
8e0f9a1e0a
|
Add the logical relation
|
2024-12-27 01:38:25 -05:00 |
|
Yiyun Liu
|
1bd6a8508e
|
Create README.md
|
2024-12-25 21:15:48 -05:00 |
|
Yiyun Liu
|
80d8b13e49
|
Prove join univ pi contra
|
2024-12-25 21:11:58 -05:00 |
|
Yiyun Liu
|
e2702ed277
|
Add join pi inj
|
2024-12-25 20:15:55 -05:00 |
|
Yiyun Liu
|
98a11fb7ac
|
Remove funext from Equations
|
2024-12-25 19:59:13 -05:00 |
|
Yiyun Liu
|
22c7eff954
|
No admits
|
2024-12-25 18:09:20 -05:00 |
|
Yiyun Liu
|
efc3662f31
|
Add erpars.picong
|
2024-12-25 18:05:49 -05:00 |
|
Yiyun Liu
|
a6f89ef7f7
|
Add abs and paircong
|
2024-12-25 17:55:47 -05:00 |
|
Yiyun Liu
|
ff0a54aaae
|
Add ERPars.AppCong
|
2024-12-25 17:48:37 -05:00 |
|
Yiyun Liu
|
2e49ff6667
|
Finish hindley rosen
|
2024-12-25 17:33:56 -05:00 |
|
Yiyun Liu
|
ce29464f08
|
Make progress on par epar
|
2024-12-25 13:49:45 -05:00 |
|
Yiyun Liu
|
a34afed3d5
|
Add ERPar
|
2024-12-25 13:40:51 -05:00 |
|
Yiyun Liu
|
2b26735fff
|
One admit left
|
2024-12-25 13:15:52 -05:00 |
|
Yiyun Liu
|
2d20d06fd2
|
Finish anti-renaming
|
2024-12-25 13:11:12 -05:00 |
|
Yiyun Liu
|
add8a62d85
|
Almost done!
|
2024-12-25 01:57:46 -05:00 |
|
Yiyun Liu
|
3de6dae199
|
Note: Changed the definition of extract!
|
2024-12-25 01:51:50 -05:00 |
|
