uwplse/pumpkin-pi
An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
CoqMIT
Issues
- 20
- 0
Combinatorial bijections?
#98 opened by chadbrewbaker - 0
- 1
Adding constructors
#86 opened by tlringer - 0
- 0
Clean up code to match terminology in paper
#92 opened by tlringer - 0
Cancel out rewrites
#91 opened by tlringer - 0
Decompiler improvements meta
#90 opened by tlringer - 0
Weakening and strengthening logical predicates
#89 opened by tlringer - 0
Revisit the positive example
#88 opened by tlringer - 0
Adding hypotheses
#87 opened by tlringer - 7
Fix bugs from listTovect
#32 opened by tlringer - 0
- 1
Support other kinds of ornaments
#35 opened by tlringer - 1
- 1
- 1
Support lifting for refinements
#41 opened by tlringer - 0
Improve error messaging
#38 opened by tlringer - 0
Tactic version of search for equivalences
#40 opened by tlringer - 0
Integrate with the Coq CI
#46 opened by tlringer - 0
Update to the latest Coq version
#45 opened by tlringer - 0
Implement better handling of opaque terms
#52 opened by tlringer - 0
Support universe polymorphism
#54 opened by tlringer - 0
Use user_err instead of failwith
#55 opened by tlringer - 1
- 1
- 5
- 0
- 2
- 1
Equations integration
#72 opened by tlringer - 0
Tactic version of lifting
#73 opened by tlringer - 1
Define adjunction with nicer type (cf., #68)
#74 opened by nateyazdani - 1
- 0
Syntax of commands feels awkward at times
#82 opened by Ptival - 0
- 0
Move prints in frontend into msg_notice
#47 opened by tlringer - 0
File organization
#67 opened by tlringer - 4
Generate a proof of adjunction
#57 opened by tlringer - 0
Update docs after refactor
#64 opened by tlringer - 0
Use better evar hygiene
#53 opened by tlringer - 3
Refactor searching for ornaments (DEVOID)
#63 opened by tlringer - 0
Caching should be smarter
#61 opened by tlringer - 0
Bug in forgetting with letin
#58 opened by tlringer - 1
Is it necessary to prove adjunction too?
#49 opened by tlringer - 21
Case study numbers and text are out of sync
#43 opened by tlringer - 2
Lifting large unpacked constants is very slow
#44 opened by tlringer - 0
- 0
- 0
- 0
Lifting probably has a bug with dependent IB
#31 opened by tlringer