Yiyun Liu yiyunliu · he/him
0 followers · 0 following
Repositories
4
 Projects Packages Public activity Starred repositories
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
yiyunliu pushed to cleanup at yiyunliu/sp-eta-postpone 2025-03-10 22:44:51 -04:00
d1771adc48 Use hne and hf instead HRed.nf
yiyunliu pushed to cleanup at yiyunliu/sp-eta-postpone 2025-03-10 19:58:27 -04:00
30caf75002 Make progress on the refactored lemma
yiyunliu pushed to cleanup at yiyunliu/sp-eta-postpone 2025-03-10 19:03:00 -04:00
030dccb326 Finish the refactored executable_correct
yiyunliu pushed to cleanup at yiyunliu/sp-eta-postpone 2025-03-10 18:18:52 -04:00
4021d05d99 Update executable to use salgo_dom for subtyping