Yiyun Liu yiyunliu · he/him
0 followers · 0 following
Repositories
7
 Projects Packages Public activity Starred repositories
yiyunliu pushed to master at yiyunliu/eta-expand-confluence 2025-04-08 01:04:12 -04:00
00f581bcc7 Work on diamond
yiyunliu created branch master in yiyunliu/eta-expand-confluence 2025-04-07 23:37:01 -04:00
yiyunliu pushed to master at yiyunliu/eta-expand-confluence 2025-04-07 23:37:01 -04:00
5cf82dae12 Add syntax spec
yiyunliu created repository yiyunliu/eta-expand-confluence 2025-04-07 23:36:36 -04:00
yiyunliu pushed to syntactic at yiyunliu/pair-eta 2025-04-04 01:43:11 -04:00
71b08b83e3 Finish all cases of type unique except for pair formation
yiyunliu pushed to syntactic at yiyunliu/pair-eta 2025-04-03 23:20:45 -04:00
5eb1f9df0b Make progress on wt_unique
yiyunliu pushed to syntactic at yiyunliu/pair-eta 2025-04-03 21:50:50 -04:00
fbbce90304 Add typing and stub for typing properties
yiyunliu pushed to syntactic at yiyunliu/pair-eta 2025-04-03 21:18:22 -04:00
3b8fe388dc Make the internal language even smaller
yiyunliu created branch syntactic in yiyunliu/pair-eta 2025-04-03 16:21:19 -04:00
yiyunliu pushed to syntactic at yiyunliu/pair-eta 2025-04-03 16:21:19 -04:00
f402f4e528 Fix fp_red
yiyunliu pushed to main at yiyunliu/pair-eta 2025-04-01 23:21:40 -04:00
9c17ec5cac Start refactoring to unscoped syntax
yiyunliu pushed to main at yiyunliu/pair-eta 2025-04-01 21:59:40 -04:00
398a18d770 Finish renaming
255bd4acbf Rename the term constructors
1f7460fd11 Add new syntax for booleans
Compare 3 commits »
yiyunliu pushed to master at yiyunliu/info-page 2025-03-21 18:02:25 -04:00
d9742e6a94 Wrong branch
yiyunliu pushed to master at yiyunliu/info-page 2025-03-21 18:01:38 -04:00
b7820e6d9f Add woodpecker ci
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-03-11 16:34:52 -04:00
f9d3a620f4 Remove itauto dependency as it introduces weird axioms
8dbef3e29e Finish refactoring
96ad0a4740 Add stub for the new coqleq_complete'
181e06ae01 Finish the completeness proof for equality
9d68e5d6c9 Finish the conf case
Compare 12 commits »
yiyunliu pushed to cleanup at yiyunliu/sp-eta-postpone 2025-03-11 16:27:41 -04:00
f9d3a620f4 Remove itauto dependency as it introduces weird axioms
yiyunliu pushed to cleanup at yiyunliu/sp-eta-postpone 2025-03-11 16:25:04 -04:00
8dbef3e29e Finish refactoring
yiyunliu pushed to cleanup at yiyunliu/sp-eta-postpone 2025-03-11 00:14:53 -04:00
96ad0a4740 Add stub for the new coqleq_complete'
yiyunliu pushed to cleanup at yiyunliu/sp-eta-postpone 2025-03-10 23:47:17 -04:00
181e06ae01 Finish the completeness proof for equality
yiyunliu pushed to cleanup at yiyunliu/sp-eta-postpone 2025-03-10 23:22:17 -04:00
9d68e5d6c9 Finish the conf case