AndrasKovacs/elaboration-zoo

Issues

• What does `A[spine]` mean?

  #35 opened a year ago by hirrolot
  2

• Why do we ignore the type while checking a hole?

  #38 opened a year ago by hirrolot
  4

• Documentation of `PartialRenaming`

  #34 opened a year ago by hirrolot
  11

• Is the implementation of `invert` correct?

  #32 opened a year ago by BjoernLoetters
  3

• How to add boolean elimination in the domain

  #21 opened 5 years ago by atennapel
  14

• Why do we generate a fresh identifier in `quote`?

  #31 opened 2 years ago by hirrolot
  2

• General Recursion

  #30 opened 3 years ago by onepunchtech
  4

• Predicative type hierarchy

  #27 opened 3 years ago by atennapel
  1

• Stick to strict pattern unification

  #18 opened 4 years ago by AndrasKovacs
  5

• What is the need for InsertedMeta?

  #28 opened 4 years ago by atennapel
  7

• Get rid of all String names, only use de Bruijn

  #19 opened 4 years ago by AndrasKovacs
  7

• Unification of decoding functions

  #26 opened 4 years ago by atennapel
  6

• Adding primitives

  #23 opened 4 years ago by atennapel
  15

• Zoo zone for introducing inductive data types?

  #25 opened 4 years ago by anqurvanillapy
  8

• Should types be unified when unifying lambdas?

  #24 opened 4 years ago by atennapel
  2

• Making lambda the only binder

  #22 opened 5 years ago by atennapel
  2

• Axiom for induction for church encoding

  #20 opened 5 years ago by atennapel
  1

• Some hints regarding deBruijn implementation of meta solving

  #5 opened 5 years ago by atennapel
  6

• Inferring annotated lambdas

  #14 opened 5 years ago by atennapel
  3

• Implicit lambda insertion with deBruijn

  #17 opened 5 years ago by atennapel
  3

• How to evaluate primitive induction principles?

  #15 opened 5 years ago by atennapel
  0

• Eta reduction in evaluation

  #13 opened 5 years ago by atennapel
  1

• Displaying types without reducing globally defined variables

  #12 opened 5 years ago by atennapel
  1

• Anything new?

  #7 opened 5 years ago by ice1000
  45

• Elaboration seems to not handle shadows names correctly

  #11 opened 5 years ago by atennapel
  0

• What is the unification algorithm lacking in order to handle application of a meta?

  #10 opened 5 years ago by atennapel
  6

• Metas with reference cells

  #8 opened 5 years ago by atennapel
  9

• checkSolution, should meta solution be checked?

  #9 opened 5 years ago by atennapel
  2

• Unification should check for spine length equality?

  #6 opened 5 years ago by atennapel
  2

• Can you translate let-expressions to lambda abstractions?

  #4 opened 5 years ago by atennapel
  2

• Shouldn't the elaborated lambda abstractions be annotated with their parameter type?

  #3 opened 5 years ago by atennapel
  2

• Why this term fails to typecheck?

  #2 opened 8 years ago by VictorTaelin
  4