hazelgrove/agda-popl17

Issues

• look up table for rule numbers

  #37 opened 8 years ago by ivoysey
  0

• final pass to remove cruft, document

  #35 opened 8 years ago by ivoysey
  0

• idempotency of minimzer

  #34 opened 8 years ago by ivoysey
  6

• final pass to propagate to sums, curate diff

  #36 opened 8 years ago by ivoysey
  0

• add ifz

  #4 opened 8 years ago by ivoysey
  2

• add let

  #5 opened 8 years ago by ivoysey
  2

• derived actions

  #17 opened 8 years ago by ivoysey
  2

• reflection

  #18 opened 8 years ago by ivoysey
  1

• finish normal / role of non-empty holes in constructability

  #21 opened 8 years ago by ivoysey
  2

• implement semantics using agda functions

  #25 opened 8 years ago by cyrus-
  1

• not-outside-in checksum

  #33 opened 8 years ago by ivoysey
  2

• operators and arities

  #2 opened 8 years ago by ivoysey
  5

• structural properties

  #22 opened 8 years ago by ivoysey
  0

• complete dynamics, progress and preservation

  #11 opened 8 years ago by ivoysey
  7

• add example code for all figures

  #32 opened 8 years ago by ivoysey
  0

• declarative system

  #12 opened 8 years ago by ivoysey
  0

• curate diff between sum and master

  #29 opened 8 years ago by ivoysey
  2

• clean up moveerase.agda

  #27 opened 8 years ago by ivoysey
  2

• add rules for constructing a case in a synthetic context

  #31 opened 8 years ago by ivoysey
  0

• extra assumptions in case zippers

  #30 opened 8 years ago by ivoysey
  0

• reformulate movement

  #6 opened 8 years ago by ivoysey
  0

• extend determinism to sums

  #28 opened 8 years ago by ivoysey
  0

• restore determinism of action semantics

  #16 opened 8 years ago by ivoysey
  4

• theorem names

  #26 opened 8 years ago by ivoysey
  1

• fix the action subsumption rule

  #13 opened 8 years ago by ivoysey
  1

• coherence between heads of the two branches

  #24 opened 8 years ago by ivoysey
  1

• sums

  #1 opened 8 years ago by ivoysey
  0

• abstract rules for repeated ideas in constructors

  #14 opened 8 years ago by ivoysey
  1

• update the readme

  #23 opened 8 years ago by ivoysey
  0

• make comments and notation consistent with paper

  #19 opened 8 years ago by cyrus-
  5

• add comments for fancy unicode

  #20 opened 8 years ago by cyrus-
  2

• deletability

  #7 opened 8 years ago by ivoysey
  9

• finishability

  #8 opened 8 years ago by ivoysey
  1

• understand and unify congruence lemmas

  #15 opened 8 years ago by ivoysey
  1

• erasure

  #3 opened 8 years ago by ivoysey
  2

• constructability

  #9 opened 8 years ago by ivoysey
  2

• finish reachability

  #10 opened 8 years ago by ivoysey
  0