Yiyun Liu yiyunliu · he/him
0 followers · 0 following
Repositories
7
 Projects Packages Public activity Starred repositories
yiyunliu pushed to bove-capretta at yiyunliu/sp-eta-postpone 2025-02-28 15:56:45 -05:00
7b5e9f2562 view needs more information
yiyunliu pushed to bove-capretta at yiyunliu/sp-eta-postpone 2025-02-28 14:50:55 -05:00
816c73cb71 Switch to view pattern
yiyunliu pushed to bove-capretta at yiyunliu/sp-eta-postpone 2025-02-28 14:42:50 -05:00
ca73b5eac6 Add more cases to tm_to_eq
yiyunliu pushed to bove-capretta at yiyunliu/sp-eta-postpone 2025-02-28 14:05:32 -05:00
44ba3e6575 Add view
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