Russoul/Nova

Issues

• Extensional TT as formulated is not suitable for automated unification

  #34 opened a year ago by Russoul
  0

• Design and implement a set of conditions to check before running a tactic

  #7 opened a year ago by Russoul
  0

• Include `Ω` into the design of the core

  #6 opened a year ago by Russoul
  0

• Reference the material that has influenced and has been used to build Nova

  #33 opened a year ago by Russoul
  0

• Collect all reasons why unification problem is stuck

  #31 opened a year ago by Russoul
  0

• Get rid of nameful meta-context in favour of a nameless one.

  #29 opened a year ago by Russoul
  0

• Design and implement a system for testing Nova

  #28 opened a year ago by Russoul
  0

• Split Elaboration.idr into multiple files for better performance

  #22 opened a year ago by Russoul
  0

• Figure out why `Elem` elaboration is slow and fix the issue

  #26 opened a year ago by Russoul
  0

• Design and implement Coquand-Russell externally indexed universe hierarchy.

  #25 opened a year ago by Russoul
  0

• Note about universes

  #24 opened a year ago by Russoul
  0

• Allow defining (large) types at surface-level

  #20 opened a year ago by Russoul
  0

• Think of implementing quotient indexed W-type as it's equivalent to strictly positive quotient inductive schemas in our TT

  #16 opened a year ago by Russoul
  0

• Check surface path syntax for correctness before running a tactic on it

  #19 opened a year ago by Russoul
  0

• Try integrating frex into the tactics language to discharge equations

  #18 opened a year ago by Russoul
  0

• Design and implement a form of co-inductive types

  #17 opened a year ago by Russoul
  0

• Make rewrite work with implicit applications

  #10 opened a year ago by Russoul
  1

• Implement "dot patterns" in rewrite

  #11 opened a year ago by Russoul
  0

• Make contexts contain type-families to support higher-order arguments

  #15 opened a year ago by Russoul
  0

• Make reduce tactic identify shorter paths

  #9 opened a year ago by Russoul
  0

• Fix ambiguous surface path syntax

  #2 opened a year ago by Russoul
  0

• Make an alternative indentation-significant syntax for `tac` that doesn't require `;`

  #12 opened a year ago by Russoul
  0

• Add ability to solve unification constraints separately of elaboration of surface syntax

  #8 opened a year ago by Russoul
  0

• Design and implement an externally indexed Tarski universe hierarchy

  #5 opened a year ago by Russoul
  0

• Design and implement indexed quotient inductive types

  #4 opened a year ago by Russoul
  0

• Rework eliminators if possible

  #3 opened a year ago by Russoul
  1