issues
search
sacerdot
/
Minimalist-Type-Theory-In-Lambda-Prolog
An implementation in Lambda-Prolog of the Minimalist Type Theory
4
stars
3
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Merging the extractor code with the rest of the codebase
#13
riccardocaprari
closed
6 years ago
0
Fix in propId and setSum
#12
riccardocaprari
closed
6 years ago
1
Fix richiesto al check dei kind sulle prop
#11
riccardocaprari
closed
6 years ago
0
Use constants to reduce the size of translated terms
#10
sacerdot
opened
6 years ago
0
Rename interp_isa as interp_tau
#9
fifofefe
opened
6 years ago
0
Added preliminary comments to main.elpi, moved some lines and deleted…
#8
Anfiarao
closed
6 years ago
0
syntax highlight on github
#7
gares
closed
6 years ago
1
tau_proof_eq for setPi does not consider the case of two non unifying functions
#6
fifofefe
opened
6 years ago
0
is it possible to implement tau_trasp in terms of tau (with maybe other non trivia modifications)?
#5
fifofefe
opened
6 years ago
0
Consider substituting dconv with conv
#4
fifofefe
opened
6 years ago
0
controllare che la correzione (locDef T M) |--> (locDef X T M) sia coerente
#3
fifofefe
opened
7 years ago
1
scrivere le "equ" come espansioni
#2
fifofefe
closed
6 years ago
1
aggiungere type signatures in elpi
#1
fifofefe
closed
6 years ago
0