owo-lang/minitt-rs

Issues

• Try apply `id` to `id`

  #26 opened 5 years ago by xieyuheng
  2

• Type universe and (possibly) universal subtyping

  #7 opened 5 years ago by ice1000
  9

• Try the `elimBool` of the paper.

  #25 opened 5 years ago by xieyuheng
  6

• Generalized algebraic data types (indexed inductive families)

  #11 opened 6 years ago by ice1000
  22

• Support "otherwise" in split

  #2 opened 6 years ago by ice1000
  0

• Universe polymorphism

  #20 opened 6 years ago by ice1000
  1

• Termination check (structural induction)

  #9 opened 6 years ago by ice1000
  2

• Create `minitt-util`

  #24 opened 5 years ago by ice1000
  1

• Use KaTeX in rustdoc

  #23 opened 6 years ago by ice1000
  1

• Entering empty expressions in REPL mode should not trigger parsing

  #22 opened 6 years ago by anqurvanillapy
  0

• Merge two sums

  #15 opened 6 years ago by ice1000
  1

• Sum/Pi/Sigma with levels?

  #13 opened 6 years ago by ice1000
  0

• Improve `split` pretty printer

  #16 opened 6 years ago by ice1000
  0

• Sum's each branch should have its own telescope

  #17 opened 6 years ago by ice1000
  0

• Backend framework

  #10 opened 6 years ago by ice1000
  0

• The ability to attach builtin definitions (like Agda BUILTIN pragma

  #12 opened 6 years ago by ice1000
  0

• Positivity check for sum types

  #8 opened 6 years ago by ice1000
  0

• Subtyping check on sum types

  #6 opened 6 years ago by ice1000
  0

• Infer type of constructor call as a "minimum sum"

  #3 opened 6 years ago by ice1000
  0

• Default placeholder for constructor parameter/pattern

  #5 opened 6 years ago by ice1000
  0

• `const` parser

  #4 opened 6 years ago by ice1000
  0

• Support big lambdas

  #1 opened 6 years ago by ice1000
  2