diff options
| author | Josh Chen | 2020-07-11 15:13:20 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-07-11 15:13:20 +0200 |
| commit | 79659cb0edf1eea026a93955403a33a1f38f6123 (patch) | |
| tree | cc2e5f96a48a450b5b178304232509bedfdb49b9 | |
| parent | 7d59cf17b60d196c2a8bb93e5b1927748599107e (diff) | |
Defined annotated terms to be used in future typechecking improvements
| -rw-r--r-- | spartan/core/Spartan.thy | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index 1ca027f..8fa6cfe 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -42,10 +42,13 @@ typedecl o judgment has_type :: \<open>o \<Rightarrow> o \<Rightarrow> prop\<close> ("(2_:/ _)" 999) +text \<open>Type annotations:\<close> -section \<open>Type annotations\<close> +definition anno :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close> ("'(_ : _')") + where "(a : A) \<equiv> a" if "a: A" -consts anno :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close> ("'(_: _')") +lemma anno: "a: A \<Longrightarrow> (a : A): A" + by (unfold anno_def) section \<open>Universes\<close> @@ -95,7 +98,7 @@ translations "\<lambda>x: A. b" \<rightleftharpoons> "CONST lam A (fn x. b)" abbreviation Fn (infixr "\<rightarrow>" 40) where "A \<rightarrow> B \<equiv> \<Prod>_: A. B" -term "\<lambda>x: A. b x" + axiomatization where PiF: "\<lbrakk>\<And>x. x: A \<Longrightarrow> B x: U i; A: U i\<rbrakk> \<Longrightarrow> \<Prod>x: A. B x: U i" and @@ -166,7 +169,7 @@ axiomatization where section \<open>Infrastructure\<close> ML_file \<open>lib.ML\<close> -ML_file \<open>types.ML\<close> +ML_file \<open>typechecking.ML\<close> subsection \<open>Proof commands\<close> |