Yiyun Liu yiyunliu · he/him
0 followers · 0 following
Repositories
4
 Projects Packages Public activity Starred repositories
yiyunliu pushed to bove-capretta at yiyunliu/sp-eta-postpone 2025-02-28 00:30:24 -05:00
11bfed2d17 Finish defining the algorithm
yiyunliu pushed to bove-capretta at yiyunliu/sp-eta-postpone 2025-02-27 22:27:22 -05:00
757f050d92 The definition is semi-working
yiyunliu pushed to bove-capretta at yiyunliu/sp-eta-postpone 2025-02-27 21:34:08 -05:00
7503dea251 Seems to work but takes a million years to type check
yiyunliu created branch bove-capretta in yiyunliu/sp-eta-postpone 2025-02-27 20:56:12 -05:00
yiyunliu pushed to bove-capretta at yiyunliu/sp-eta-postpone 2025-02-27 20:56:12 -05:00
6c11f5560d Need noconfusion?
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-27 20:40:19 -05:00
875db75955 Add equations for check_equal
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-27 15:31:29 -05:00
4509a64bf5 Finish the soundness and completeness proof with nat
e663a1a596 Finish most of the completeness proof
aaec928902 Make progress on the completeness proof
af0cac15e6 Prove some simple impossible cases
f8943e3a9c Finish some cases of the soundness proof
Compare 41 commits »
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-27 15:31:06 -05:00
4509a64bf5 Finish the soundness and completeness proof with nat
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-27 15:09:30 -05:00
e663a1a596 Finish most of the completeness proof
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-27 00:08:13 -05:00
aaec928902 Make progress on the completeness proof
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-26 19:46:10 -05:00
af0cac15e6 Prove some simple impossible cases
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-26 16:49:11 -05:00
f8943e3a9c Finish some cases of the soundness proof
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-26 15:45:47 -05:00
49bb2cca13 Finish the completeness proof
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-26 00:48:26 -05:00
2a492a67de Add algorithmic rules for nat
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-25 22:36:08 -05:00
687d1be03f Finish preservation
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-25 21:04:39 -05:00
bb39f157ba Finish regularity
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-25 20:18:49 -05:00
96bc223b0a Finish renaming and preservation
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-25 16:50:19 -05:00
cc0e9219c4 Finish two cases of renaming
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-25 16:12:53 -05:00
291d821d94 Add some admits to work on later
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-25 16:06:11 -05:00
b2aec9c6ce Add syntactic typing rules