owo-lang minitt-rs issues

owo-lang / minitt-rs

Dependently-typed lambda calculus, Mini-TT, extended and implemented in Rust

Apache License 2.0

113 stars 2 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Try apply `id` to `id`

#26 xieyuheng closed 4 years ago
2
Try the `elimBool` of the paper.

#25 xieyuheng closed 4 years ago
6
Create `minitt-util`

#24 ice1000 closed 4 years ago
1
Use KaTeX in rustdoc

#23 ice1000 closed 5 years ago
1
Entering empty expressions in REPL mode should not trigger parsing

#22 anqurvanillapy closed 5 years ago
0
level

#21 oraluben closed 5 years ago
1
Universe polymorphism

#20 ice1000 opened 5 years ago
1
[ #13 ] Level for Sigma/Pi/Sum

#19 oraluben closed 5 years ago
3
merge level with new Merge feature

#18 oraluben closed 5 years ago
0
Sum's each branch should have its own telescope

#17 ice1000 closed 5 years ago
0
Improve `split` pretty printer

#16 ice1000 closed 5 years ago
0
Merge two sums

#15 ice1000 closed 5 years ago
1
Sigma/Pi/Sum with level

#14 oraluben closed 5 years ago
1
Sum/Pi/Sigma with levels?

#13 ice1000 closed 5 years ago
0
The ability to attach builtin definitions (like Agda BUILTIN pragma

#12 ice1000 opened 5 years ago
0
Generalized algebraic data types (indexed inductive families)

#11 ice1000 opened 5 years ago
22
Backend framework

#10 ice1000 opened 5 years ago
0
Termination check (structural induction)

#9 ice1000 opened 5 years ago
2
Positivity check for sum types

#8 ice1000 opened 5 years ago
0
Type universe and (possibly) universal subtyping

#7 ice1000 closed 4 years ago
9
Subtyping check on sum types

#6 ice1000 closed 5 years ago
0
Default placeholder for constructor parameter/pattern

#5 ice1000 closed 5 years ago
0
`const` parser

#4 ice1000 closed 5 years ago
0
Infer type of constructor call as a "minimum sum"

#3 ice1000 closed 5 years ago
0
Support "otherwise" in split

#2 ice1000 opened 5 years ago
0
Support big lambdas

#1 ice1000 closed 5 years ago
2