yiyunliu/sp-eta-postpone
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Compare commits

base: yiyunliu:tstar
Branches Tags
yiyunliu:master
yiyunliu:nonessential
yiyunliu:tstar
..
compare: yiyunliu:master
Branches Tags
yiyunliu:master
yiyunliu:nonessential
yiyunliu:tstar

19 commits
tstar ... master

Author SHA1 Message Date
Yiyun Liu
5a7f46a8a1 Finish the enhanced eta postponement 2025-01-30 23:29:25 -05:00
Yiyun Liu
51ac5ffbd6 Finish eta postponement 2025-01-30 23:10:11 -05:00
Yiyun Liu
9134cfec8a Finish a few cases of eta postponement 2025-01-30 22:18:58 -05:00
Yiyun Liu
d925a8bcaa Minor cleanup 2025-01-30 20:23:57 -05:00
Yiyun Liu
fc666956e2 Finish off the SN proof 2025-01-30 20:23:25 -05:00
Yiyun Liu
64e558f09e Finish sn unsubst 2025-01-30 20:17:00 -05:00
Yiyun Liu
c83be03230 Finish antirenaming 2025-01-30 16:14:56 -05:00
Yiyun Liu
e4c2bd39db Finish the eta split proof without any admits 2025-01-29 23:41:38 -05:00
Yiyun Liu
20eef78014 Finish one example case of violate sn 2025-01-29 22:59:57 -05:00
Yiyun Liu
aa2c2ca151 Add lemmas that bad forms are impossible 2025-01-29 22:25:14 -05:00
Yiyun Liu
a47d69f427 More no forbid 2025-01-29 22:19:36 -05:00
Yiyun Liu
99b5e87ea3 Finish red sn preservation 2025-01-29 22:09:08 -05:00
Yiyun Liu
369bd55932 Add red sn preservation 2025-01-29 21:27:49 -05:00
Yiyun Liu
5f619c0980 Finish the split lemma up to strong normalization 2025-01-29 15:52:05 -05:00
Yiyun Liu
710b59fd8f Prove all application cases 2025-01-29 14:01:35 -05:00
Yiyun Liu
08b9395acb Push some important cases of the split lemma 2025-01-29 13:37:54 -05:00
Yiyun Liu
3f3703990d Save progress 2025-01-28 16:37:23 -05:00
Yiyun Liu
24693b8928 Add "beta-free" eta contraction 2025-01-28 16:07:52 -05:00
Yiyun Liu
61e743ee74 Add ne ered 2025-01-28 15:14:33 -05:00
1 changed files with 730 additions and 344 deletions
Show stats Expand all files Collapse all files

1074
theories/fp_red.v
View file

File diff suppressed because it is too large Load diff