From f988d541364841cd208f4fd21ff8e5e2935fc7aa Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 24 Jun 2021 22:40:05 +0100
Subject: Bad practice huge commit: 1. Rudimentary prototype definitional
 package 2. Started univalence 3. Various compatibility fixes and new theory
 stubs 4. Updated ROOT file

---
 mltt/lib/List.thy    | 10 +++++-----
 mltt/lib/Maybe.thy   |  2 +-
 mltt/lib/Prelude.thy |  2 +-
 3 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'mltt/lib')

diff --git a/mltt/lib/List.thy b/mltt/lib/List.thy
index 4beb9b6..0cd43c8 100644
--- a/mltt/lib/List.thy
+++ b/mltt/lib/List.thy
@@ -83,7 +83,7 @@ section \<open>Standard functions\<close>
 
 subsection \<open>Head and tail\<close>
 
-Definition head:
+Lemma (def) head:
   assumes "A: U i" "xs: List A"
   shows "Maybe A"
 proof (cases xs)
@@ -91,7 +91,7 @@ proof (cases xs)
   show "\<And>x. x: A \<Longrightarrow> some x: Maybe A" by intro
 qed
 
-Definition tail:
+Lemma (def) tail:
   assumes "A: U i" "xs: List A"
   shows "List A"
 proof (cases xs)
@@ -128,7 +128,7 @@ Lemma tail_of_cons [comp]:
 
 subsection \<open>Append\<close>
 
-Definition app:
+Lemma (def) app:
   assumes "A: U i" "xs: List A" "ys: List A"
   shows "List A"
   apply (elim xs)
@@ -143,7 +143,7 @@ translations "app" \<leftharpoondown> "CONST List.app A"
 
 subsection \<open>Map\<close>
 
-Definition map:
+Lemma (def) map:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "xs: List A"
   shows "List B"
 proof (elim xs)
@@ -165,7 +165,7 @@ Lemma map_type [type]:
 
 subsection \<open>Reverse\<close>
 
-Definition rev:
+Lemma (def) rev:
   assumes "A: U i" "xs: List A"
   shows "List A"
   apply (elim xs)
diff --git a/mltt/lib/Maybe.thy b/mltt/lib/Maybe.thy
index 452acc2..257bc8f 100644
--- a/mltt/lib/Maybe.thy
+++ b/mltt/lib/Maybe.thy
@@ -17,7 +17,7 @@ lemma
   Maybe_some: "a: A \<Longrightarrow> some A a: Maybe A"
   unfolding Maybe_def none_def some_def by typechk+
 
-Definition MaybeInd:
+Lemma (def) MaybeInd:
   assumes
     "A: U i"
     "\<And>m. m: Maybe A \<Longrightarrow> C m: U i"
diff --git a/mltt/lib/Prelude.thy b/mltt/lib/Prelude.thy
index 0393968..86165cd 100644
--- a/mltt/lib/Prelude.thy
+++ b/mltt/lib/Prelude.thy
@@ -100,7 +100,7 @@ Lemma
   unfolding Bool_def true_def false_def by typechk+
 
 \<comment> \<open>Definitions like these should be handled by a future function package\<close>
-Definition ifelse [rotated 1]:
+Lemma (def) ifelse [rotated 1]:
   assumes *[unfolded Bool_def true_def false_def]:
     "\<And>x. x: Bool \<Longrightarrow> C x: U i"
     "x: Bool"
-- 
cgit v1.2.3