diff options
author | Josh Chen | 2021-06-23 16:26:23 +0100 |
---|---|---|
committer | Josh Chen | 2021-06-23 16:26:23 +0100 |
commit | 0085798a86a35e2430a97289e894724f688db435 (patch) | |
tree | db1662a5805917c6627963578f074dc226b4b06a /mltt/core/goals.ML | |
parent | 1928649fd490d50d1e05fef6cbb22ca38d81cbe5 (diff) |
1. Put universe level parameters first in automatic term definitions. 2. Add debugging to typechecker
Diffstat (limited to '')
-rw-r--r-- | mltt/core/goals.ML | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/mltt/core/goals.ML b/mltt/core/goals.ML index 7d52495..d69c800 100644 --- a/mltt/core/goals.ML +++ b/mltt/core/goals.ML @@ -82,7 +82,7 @@ fun define_proof_term name (local_name, [th]) lthy = val concl_vars = Lib.collect_subterms is_Var (Lib.term_of_typing concl) - val params = inter Term.aconv concl_vars prems_vars + val params = sort (uncurry Lib.lvl_order) (inter Term.aconv concl_vars prems_vars) val prf_tm = fold_rev lambda params (Lib.term_of_typing concl) @@ -197,10 +197,11 @@ fun theorem spec descr = long descr NONE (K I) binding includes elems concl)) fun definition spec descr = - Outer_Syntax.local_theory_to_proof' spec "definition via proof" + Outer_Syntax.local_theory_to_proof' spec "definition with explicit type checking obligation" ((long_statement || short_statement) >> - (fn (long, binding, includes, elems, concl) => schematic_theorem_cmd - true long descr NONE (K I) binding includes elems concl)) + (fn (long, binding, includes, elems, concl) => + schematic_theorem_cmd + true long descr NONE (K I) binding includes elems concl)) in |