Yiyun Liu yiyunliu · he/him
0 followers · 0 following
Repositories
4
 Projects Packages Public activity Starred repositories
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-03 23:46:55 -05:00
87f6dcd870 Prove the soundness of the computable equality
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-03 21:16:59 -05:00
36d1f95d65 Move HRed to the common .v file
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-03 21:09:25 -05:00
5ac3b21331 Refactor the correctness proof of coquand's algorithm
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-03 16:01:31 -05:00
3a17548a7d Minor
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-03 15:50:18 -05:00
3e8ad2c5bc Work on the refactoring proof
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-03 15:30:04 -05:00
fe418c2a78 Fix preservation and broken cases in logrel
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-03 15:23:11 -05:00
d68adf85f4 Finish refactoring substitution lemmas
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-03 01:40:15 -05:00
896d22ac9b minor
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-03 01:38:28 -05:00
b3bd75ad42 Fix the typing rules
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-03 01:15:32 -05:00
47e21df801 Finish refactoring logical relations
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-02 22:41:22 -05:00
7f38544a1e Finish refactoring fp_red
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-02 20:19:20 -05:00
551dd5c17c Fix the fv proof
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-02 17:35:59 -05:00
226b196d15 Refactor half of fp_red
yiyunliu pushed to unscoped at yiyunliu/sp-eta-postpone 2025-03-02 16:40:55 -05:00
657c1325c9 Add unscoped syntax
yiyunliu created branch unscoped in yiyunliu/sp-eta-postpone 2025-03-02 16:40:54 -05:00
yiyunliu pushed to bove-capretta at yiyunliu/sp-eta-postpone 2025-02-28 16:39:24 -05:00
3efca4160b Add noconf check
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