aboutsummaryrefslogtreecommitdiff
path: root/mltt/core/elimination.ML
diff options
context:
space:
mode:
authorJosh Chen2021-06-23 16:26:23 +0100
committerJosh Chen2021-06-23 16:26:23 +0100
commit0085798a86a35e2430a97289e894724f688db435 (patch)
treedb1662a5805917c6627963578f074dc226b4b06a /mltt/core/elimination.ML
parent1928649fd490d50d1e05fef6cbb22ca38d81cbe5 (diff)
1. Put universe level parameters first in automatic term definitions. 2. Add debugging to typechecker
Diffstat (limited to 'mltt/core/elimination.ML')
0 files changed, 0 insertions, 0 deletions