yiyunliu/sp-eta-postpone
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
230 commits 12 branches 0 tags 3.6 MiB

Default branch

master

a367591e9a · Add extensional version of pair equality rules · Updated 2025-04-17 15:15:58 -04:00
 ZIP  TAR.GZ

Branches

ext-rep

0e04a7076b · Prove PairEta · Updated 2025-04-19 00:24:09 -04:00    yiyunliu

0
8
 ZIP  TAR.GZ
cleanup

f9d3a620f4 · Remove itauto dependency as it introduces weird axioms · Updated 2025-03-11 16:27:31 -04:00    yiyunliu

3
0
 Included
 ZIP  TAR.GZ
unscoped

437c97455e · Finish the soundness and completeness proof of the subtyping algorithm · Updated 2025-03-06 20:42:08 -05:00    yiyunliu

15
0
 Included
 ZIP  TAR.GZ
bove-capretta

3efca4160b · Add noconf check · Updated 2025-02-28 16:39:10 -05:00    yiyunliu

43
10
 ZIP  TAR.GZ
nat

4509a64bf5 · Finish the soundness and completeness proof with nat · Updated 2025-02-27 15:30:55 -05:00    yiyunliu

43
0
 Included
 ZIP  TAR.GZ
subtyping

0e0d9b20e5 · Try making the cases mutually recursive? · Updated 2025-02-19 18:03:32 -05:00    yiyunliu

81
0
 Included
 ZIP  TAR.GZ
logrelnew

c24cc7c9b0 · Finish ST Conv · Updated 2025-02-06 00:08:02 -05:00    yiyunliu

168
0
 #1 Merged
 ZIP  TAR.GZ
logrel

38a0416b2c · Add a constant to avoid kripke LR · Updated 2025-02-04 22:14:27 -05:00    yiyunliu

183
0
 Included
 ZIP  TAR.GZ
antirenaming

84cd0715c7 · Prove structural properties of DJoin · Updated 2025-02-03 14:55:31 -05:00    yiyunliu

187
0
 Included
 ZIP  TAR.GZ
nonessential

47473fd3cd · Minor · Updated 2025-01-31 16:30:06 -05:00    yiyunliu

205
0
 Included
 ZIP  TAR.GZ
tstar

a27c41c5d1 · Add lemmas that bad forms are impossible · Updated 2025-01-29 12:19:45 -05:00    yiyunliu

221
1
 ZIP  TAR.GZ