Yiyun Liu yiyunliu · he/him
0 followers · 0 following
Repositories
7
 Projects Packages Public activity Starred repositories
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-22 01:29:31 -05:00
2ab47ac883 Finish eta postponement
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-22 01:20:48 -05:00
f44c8ef425 Only the indsucc case remaining for postponement
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-22 00:10:27 -05:00
d9d0e9cdd4 One remaining case for eta postponement
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-21 23:43:51 -05:00
29d05befe9 Seemingly redundant nonelim cases
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-21 22:23:46 -05:00
9f3b04d041 Finish sn red preservation
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-21 17:30:07 -05:00
fc0e096c04 Add two cases for red sn preservation
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-21 15:11:22 -05:00
2af49373e3 Repair epar sn preservation
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-21 14:35:38 -05:00
396bddc8b3 Finish unmorphing
yiyunliu created branch nat in yiyunliu/sp-eta-postpone 2025-02-21 13:23:44 -05:00
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-21 13:23:44 -05:00
fd0b48073d Add nat type definition
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-19 18:03:44 -05:00
0e0d9b20e5 Try making the cases mutually recursive?
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-19 17:41:26 -05:00
fe5c16361a Add definition for algorithmic domain
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-19 16:04:19 -05:00
df0b955e4e Add the stub for Equations but might give up later
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-17 23:31:39 -05:00
d48d9db1b7 Finish the conversion proof completely
9c5eb31edf Finish all cases of subtyping
735c7f2046 Prove some simple soundness cases of subtyping
067ae89b1d Finish soundness for subtyping
Compare 4 commits »
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-17 23:31:22 -05:00
d48d9db1b7 Finish the conversion proof completely
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-17 22:50:40 -05:00
9c5eb31edf Finish all cases of subtyping
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-17 21:43:31 -05:00
735c7f2046 Prove some simple soundness cases of subtyping
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-17 18:35:06 -05:00
067ae89b1d Finish soundness for subtyping
yiyunliu pushed to subtyping at yiyunliu/sp-eta-postpone 2025-02-17 18:05:50 -05:00
ef3de3af3d Add the specification for algorithmic subtyping
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-16 23:53:24 -05:00
ef3de3af3d Add the specification for algorithmic subtyping