diff options
Diffstat (limited to '')
| -rw-r--r-- | test.thy | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/test.thy b/test.thy new file mode 100644 index 0000000..94ba900 --- /dev/null +++ b/test.thy @@ -0,0 +1,35 @@ +theory test +imports HoTT +begin + +lemma "Null : U" + by (rule Null_form) + +lemma "A \<equiv> B \<Longrightarrow> (\<^bold>\<lambda>x. x) : B\<rightarrow>A" +proof - + have "\<And>x. A \<equiv> B \<Longrightarrow> x : B \<Longrightarrow> x : A" by (rule equal_types) + thus "A \<equiv> B \<Longrightarrow> (\<^bold>\<lambda>x. x) : B\<rightarrow>A" by (rule Function_intro) +qed + +lemma "\<^bold>\<lambda>x. \<^bold>\<lambda>y. x : A\<rightarrow>B\<rightarrow>A" +proof - + have "\<And>x. x : A \<Longrightarrow> \<^bold>\<lambda>y. x : B \<rightarrow> A" by (rule Function_intro) + thus "\<^bold>\<lambda>x. \<^bold>\<lambda>y. x : A\<rightarrow>B\<rightarrow>A" by (rule Function_intro) +qed + +(* The previous proofs are nice, BUT I want to be able to do something like the following: +lemma "x : A \<Longrightarrow> \<^bold>\<lambda>x. x : B\<rightarrow>B" <Fail> +i.e. I want to be able to associate a type to variables, and have the type remembered by any +binding I define later. + +Do I need to give up using the \<open>binder\<close> syntax in order to do this? +*) + +lemma "succ(succ 0) : Nat" +proof - + have "(succ 0) : Nat" by (rule Nat_intro2) + from this have "succ(succ 0) : Nat" by (rule Nat_intro2) +qed + + +end
\ No newline at end of file |