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/MLTT.thy | |
| parent | 1928649fd490d50d1e05fef6cbb22ca38d81cbe5 (diff) | |
1. Put universe level parameters first in automatic term definitions. 2. Add debugging to typechecker
Diffstat (limited to 'mltt/core/MLTT.thy')
| -rw-r--r-- | mltt/core/MLTT.thy | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/mltt/core/MLTT.thy b/mltt/core/MLTT.thy index cd8ae42..5888a90 100644 --- a/mltt/core/MLTT.thy +++ b/mltt/core/MLTT.thy @@ -137,9 +137,6 @@ translations "\<Sum>x: A. B" \<rightleftharpoons> "CONST Sig A (fn x. B)" abbreviation Prod (infixl "\<times>" 60) where "A \<times> B \<equiv> \<Sum>_: A. B" -abbreviation "and" (infixl "\<and>" 60) - where "A \<and> B \<equiv> A \<times> B" - axiomatization where SigF: "\<lbrakk>A: U i; \<And>x. x: A \<Longrightarrow> B x: U i\<rbrakk> \<Longrightarrow> \<Sum>x: A. B x: U i" and |