uwplse/pumpkin-pi

Issues

• Methodology for user-friendly types without UIP on the index

  #39 opened 5 years ago by tlringer
  20

• Combinatorial bijections?

  #98 opened 3 years ago by chadbrewbaker
  0

• Regression bug in simplifying projections of existentials

  #84 opened 4 years ago by tlringer
  0

• Adding constructors

  #86 opened 4 years ago by tlringer
  1

• Merge in decompiler from PUMPKIN PATCH to master as part of "Repair" command

  #85 opened 4 years ago by tlringer
  0

• Clean up code to match terminology in paper

  #92 opened 4 years ago by tlringer
  0

• Cancel out rewrites

  #91 opened 4 years ago by tlringer
  0

• Decompiler improvements meta

  #90 opened 4 years ago by tlringer
  0

• Weakening and strengthening logical predicates

  #89 opened 4 years ago by tlringer
  0

• Revisit the positive example

  #88 opened 4 years ago by tlringer
  0

• Adding hypotheses

  #87 opened 4 years ago by tlringer
  0

• Fix bugs from listTovect

  #32 opened 5 years ago by tlringer
  7

• Partially automate the user-friendly indexing methodology

  #34 opened 4 years ago by tlringer
  0

• Support other kinds of ornaments

  #35 opened 5 years ago by tlringer
  1

• Allow users to supply their own functions when search fails

  #36 opened 4 years ago by tlringer
  1

• Loosen the syntactic restrictions that search makes

  #37 opened 4 years ago by tlringer
  1

• Support lifting for refinements

  #41 opened 5 years ago by tlringer
  1

• Improve error messaging

  #38 opened 4 years ago by tlringer
  0

• Tactic version of search for equivalences

  #40 opened 5 years ago by tlringer
  0

• Integrate with the Coq CI

  #46 opened 5 years ago by tlringer
  0

• Update to the latest Coq version

  #45 opened 5 years ago by tlringer
  0

• Implement better handling of opaque terms

  #52 opened 4 years ago by tlringer
  0

• Support universe polymorphism

  #54 opened 5 years ago by tlringer
  0

• Use user_err instead of failwith

  #55 opened 4 years ago by tlringer
  0

• Support the kind of change Reviewer 2 was interested in

  #56 opened 5 years ago by tlringer
  1

• What kind of ornament relates unindexed to indexed Expr?

  #71 opened 5 years ago by tlringer
  1

• From adjunction and coherence, show user-friendly equivalence

  #62 opened 4 years ago by tlringer
  5

• For refactor, rename lifting to something more descriptive

  #66 opened 4 years ago by tlringer
  0

• Generate proofs of the correctness of configurations

  #70 opened 5 years ago by tlringer
  2

• Equations integration

  #72 opened 4 years ago by tlringer
  1

• Tactic version of lifting

  #73 opened 5 years ago by tlringer
  0

• Define adjunction with nicer type (cf., #68)

  #74 opened 5 years ago by nateyazdani
  1

• First-class lifts? First-class composition of lifts?

  #83 opened 4 years ago by Ptival
  1

• Syntax of commands feels awkward at times

  #82 opened 4 years ago by Ptival
  0

• Support lifting { a : A | indexer a = i_b } to B i_b directly

  #42 opened 4 years ago by tlringer
  0

• Move prints in frontend into msg_notice

  #47 opened 4 years ago by tlringer
  0

• File organization

  #67 opened 4 years ago by tlringer
  0

• Generate a proof of adjunction

  #57 opened 5 years ago by tlringer
  4

• Update docs after refactor

  #64 opened 5 years ago by tlringer
  0

• Use better evar hygiene

  #53 opened 5 years ago by tlringer
  0

• Refactor searching for ornaments (DEVOID)

  #63 opened 5 years ago by tlringer
  3

• Caching should be smarter

  #61 opened 5 years ago by tlringer
  0

• Bug in forgetting with letin

  #58 opened 5 years ago by tlringer
  0

• Is it necessary to prove adjunction too?

  #49 opened 5 years ago by tlringer
  1

• Case study numbers and text are out of sync

  #43 opened 5 years ago by tlringer
  21

• Lifting large unpacked constants is very slow

  #44 opened 5 years ago by tlringer
  2

• Improve automatically generated type for retraction

  #50 opened 5 years ago by tlringer
  0

• Generate proofs that promote and forget form a equivalence

  #33 opened 5 years ago by tlringer
  0

• Plugin sometimes fails with Not_found in CoqIDE with asynchronous processing

  #30 opened 5 years ago by tlringer
  0

• Lifting probably has a bug with dependent IB

  #31 opened 5 years ago by tlringer
  0