diff options
author | Josh Chen | 2018-07-12 01:46:30 +0200 |
---|---|---|
committer | Josh Chen | 2018-07-12 01:46:30 +0200 |
commit | 1be12499f63119d9455e2baa917659806732ca7d (patch) | |
tree | b65f13beb0231c6fbac99eac5e980155477c8074 /Sum.thy | |
parent | 9723fc3ffc55b22a2a8ec09cbba80f14c40d7991 (diff) |
Unit and Null types. Methods.
Diffstat (limited to '')
-rw-r--r-- | Sum.thy | 13 |
1 files changed, 13 insertions, 0 deletions
@@ -60,4 +60,17 @@ abbreviation Pair :: "[Term, Term] \<Rightarrow> Term" (infixr "\<times>" 50) where "A \<times> B \<equiv> \<Sum>_:A. B" +section \<open>Null type\<close> + +axiomatization + Null :: Term ("\<zero>") and + indNull :: "[Typefam, Term] \<Rightarrow> Term" +where + Null_form: "\<zero> : U(0)" +and + Null_elim: "\<And>i C z. \<lbrakk>C: \<zero> \<longrightarrow> U(i); z : \<zero>\<rbrakk> \<Longrightarrow> indNull C z : C z" + +lemmas Null_rules [intro] = Null_form Null_elim + + end
\ No newline at end of file |