issues
search
mzacho
/
refinement-types
A refinement type checker for simply typed lamda calculus with inductive data-types and well-founded recursive functions
MIT License
0
stars
1
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
substitute type can capture variables under refinement binder
#23
mzacho
opened
8 months ago
0
SUB-BASE can capture free variables with the binder
#22
mzacho
opened
9 months ago
2
Avoid using universal quantification
#21
mkarup
closed
9 months ago
0
demo
#20
mzacho
opened
9 months ago
0
WIP proving simple lemmas
#19
womeier
closed
9 months ago
0
Termination experimental
#18
womeier
closed
9 months ago
0
basic cli
#17
womeier
closed
9 months ago
0
parsing: precedence of negation wrt. conj/ disj is wrong
#16
mzacho
closed
9 months ago
0
Termination
#15
womeier
closed
9 months ago
0
sumT fails
#14
mzacho
closed
9 months ago
2
checking "append reflects len" fails
#13
mzacho
closed
9 months ago
6
lookup codomain of uninterpreted function in `metric_wf`
#12
mzacho
opened
9 months ago
0
enforce exhaustive switch alternatives
#11
womeier
closed
9 months ago
0
enforce that we don't add vars twice to env Gamma
#10
womeier
opened
9 months ago
3
append
#9
womeier
closed
9 months ago
2
WIP implementation of (simplified) inductive data types
#8
mkarup
closed
9 months ago
4
close formula properly
#7
womeier
closed
9 months ago
7
Simple recursion
#6
mkarup
closed
9 months ago
0
Bools and if-then-else
#5
womeier
closed
9 months ago
1
first lambda language
#4
mzacho
closed
9 months ago
1
extend predicates with some more bin ops.
#3
womeier
closed
9 months ago
3
Test naming and notation
#2
mkarup
closed
10 months ago
2
Basic logic and solver
#1
mkarup
closed
10 months ago
0