issues
search
uwplse
/
pumpkin-pi
An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
MIT License
49
stars
9
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Is it necessary to prove adjunction too?
#49
tlringer
closed
5 years ago
1
Generate proofs of coherence, section, and retraction (fixes #33)
#48
tlringer
closed
5 years ago
0
Move prints in frontend into msg_notice
#47
tlringer
closed
4 years ago
0
Integrate with the Coq CI
#46
tlringer
opened
5 years ago
0
Update to the latest Coq version
#45
tlringer
opened
5 years ago
0
Lifting large unpacked constants is very slow
#44
tlringer
opened
5 years ago
2
Case study numbers and text are out of sync
#43
tlringer
closed
5 years ago
21
Support lifting { a : A | indexer a = i_b } to B i_b directly
#42
tlringer
closed
4 years ago
0
Support lifting for refinements
#41
tlringer
opened
5 years ago
1
Tactic version of search for equivalences
#40
tlringer
opened
5 years ago
0
Methodology for user-friendly types without UIP on the index
#39
tlringer
opened
5 years ago
20
Improve error messaging
#38
tlringer
closed
4 years ago
0
Loosen the syntactic restrictions that search makes
#37
tlringer
closed
4 years ago
1
Allow users to supply their own functions when search fails
#36
tlringer
closed
4 years ago
1
Support other kinds of ornaments
#35
tlringer
opened
5 years ago
1
Partially automate the user-friendly indexing methodology
#34
tlringer
closed
4 years ago
0
Generate proofs that promote and forget form a equivalence
#33
tlringer
closed
5 years ago
0
Fix bugs from listTovect
#32
tlringer
opened
5 years ago
7
Lifting probably has a bug with dependent IB
#31
tlringer
opened
5 years ago
0
Plugin sometimes fails with Not_found in CoqIDE with asynchronous processing
#30
tlringer
closed
5 years ago
0
update proofs to use latest version of EFF
#29
tlringer
closed
5 years ago
0
Nate's unpacking automation (fixes #21)
#28
tlringer
closed
5 years ago
0
Whole-module ornamental lifting (low priority)
#27
nateyazdani
closed
4 years ago
0
Whole-module match/fixpoint-to-eliminator translation
#26
nateyazdani
closed
5 years ago
4
Support for weird fixed points in eliminator translation
#25
nateyazdani
closed
5 years ago
1
Ornamental lifting generates an ill-typed term (possibly related to ornamentally lifted inductive predicate)
#24
nateyazdani
closed
5 years ago
3
Support for translating fixed-points to eliminations (cf. Issue #18)
#23
nateyazdani
closed
5 years ago
2
Fix bugs in index identification and search
#22
tlringer
closed
5 years ago
0
Automate unwrapping of existential (sigma-packed) indices
#21
nateyazdani
closed
5 years ago
0
Auto-generate lifting-compatible eliminators for lifted inductive types (fixes #19)
#20
nateyazdani
closed
6 years ago
1
Eliminator of lifted inductive predicate is not lifting of eliminator of inductive predicate
#19
tlringer
closed
6 years ago
5
Convert fixed-point expressions to eliminator applications
#18
nateyazdani
closed
5 years ago
1
Automatically lift referenced inductive relations, using a default naming scheme
#17
nateyazdani
closed
5 years ago
1
Add function to translate match expressions to eliminator applications
#16
nateyazdani
closed
5 years ago
3
Fix implementation of lift-packed in the forward direction (fixes #14)
#15
tlringer
closed
6 years ago
0
Missing eta-expansions/contractions cause lifted terms to be ill-typed
#14
nateyazdani
closed
6 years ago
2
Support for lifting inductive relations
#13
nateyazdani
closed
6 years ago
5
Fix minor bug in term lifting
#12
nateyazdani
closed
6 years ago
3
Persistent caching of ornaments for improved interface
#11
tlringer
closed
6 years ago
0
Automate eval
#10
tlringer
closed
6 years ago
0
Case study: Qualify imports for UnivalentParametricity and delete dead code
#9
nateyazdani
closed
6 years ago
0
Simplified algorithm & cleanup
#8
tlringer
closed
6 years ago
0
Merge Nate's code with a few changes to make it more consistent with the paper
#7
tlringer
closed
6 years ago
0
Temporary reduction fixes
#6
tlringer
closed
6 years ago
0
Update to Coq 8.8
#5
tlringer
closed
6 years ago
0
Port ornamental promotions to use projT1/projT2
#4
tlringer
closed
6 years ago
0
Higher lifting
#3
tlringer
closed
6 years ago
0
Get reduction working for app_nil_r
#2
tlringer
closed
6 years ago
0
Use sigma types instead
#1
tlringer
closed
6 years ago
0
Previous