From f46df86db9308dde29e0e5f97f54546ea1dc34bf Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 18 Jan 2021 23:49:13 +0000
Subject: Swapped notation for metas (now ?) and holes (now {}), other notation
 and name changes.

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

(limited to 'spartan/lib')

diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy
index 83e5149..1501221 100644
--- a/spartan/lib/List.thy
+++ b/spartan/lib/List.thy
@@ -64,10 +64,10 @@ Lemma list_cases [cases]:
 section \<open>Notation\<close>
 
 definition nil_i ("[]")
-  where [implicit]: "[] \<equiv> nil ?"
+  where [implicit]: "[] \<equiv> nil {}"
 
 definition cons_i (infixr "#" 120)
-  where [implicit]: "x # xs \<equiv> cons ? x xs"
+  where [implicit]: "x # xs \<equiv> cons {} x xs"
 
 translations
   "[]" \<leftharpoondown> "CONST List.nil A"
@@ -99,8 +99,8 @@ proof (cases xs)
   show "\<And>xs. xs: List A \<Longrightarrow> xs: List A" .
 qed
 
-definition head_i ("head") where [implicit]: "head xs \<equiv> List.head ? xs"
-definition tail_i ("tail") where [implicit]: "tail xs \<equiv> List.tail ? xs"
+definition head_i ("head") where [implicit]: "head xs \<equiv> List.head {} xs"
+definition tail_i ("tail") where [implicit]: "tail xs \<equiv> List.tail {} xs"
 
 translations
   "head" \<leftharpoondown> "CONST List.head A"
@@ -137,7 +137,7 @@ Definition app:
       proof - show "x # rec: List A" by typechk qed
   done
 
-definition app_i ("app") where [implicit]: "app xs ys \<equiv> List.app ? xs ys"
+definition app_i ("app") where [implicit]: "app xs ys \<equiv> List.app {} xs ys"
 
 translations "app" \<leftharpoondown> "CONST List.app A"
 
@@ -153,7 +153,7 @@ proof (elim xs)
   show "f x # ys: List B" by typechk
 qed
 
-definition map_i ("map") where [implicit]: "map \<equiv> List.map ? ?"
+definition map_i ("map") where [implicit]: "map \<equiv> List.map {} {}"
 
 translations "map" \<leftharpoondown> "CONST List.map A B"
 
@@ -173,7 +173,7 @@ Definition rev:
     \<^item> vars x _ rec proof - show "app rec [x]: List A" by typechk qed
   done
 
-definition rev_i ("rev") where [implicit]: "rev \<equiv> List.rev ?"
+definition rev_i ("rev") where [implicit]: "rev \<equiv> List.rev {}"
 
 translations "rev" \<leftharpoondown> "CONST List.rev A"
 
diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy
index da22a4e..e06a07b 100644
--- a/spartan/lib/Maybe.thy
+++ b/spartan/lib/Maybe.thy
@@ -64,8 +64,8 @@ lemmas
 
 abbreviation "MaybeRec A C \<equiv> MaybeInd A (K C)"
 
-definition none_i ("none") where [implicit]: "none \<equiv> Maybe.none ?"
-definition some_i ("some") where [implicit]: "some a \<equiv> Maybe.some ? a"
+definition none_i ("none") where [implicit]: "none \<equiv> Maybe.none {}"
+definition some_i ("some") where [implicit]: "some a \<equiv> Maybe.some {} a"
 
 translations
   "none" \<leftharpoondown> "CONST Maybe.none A"
diff --git a/spartan/lib/Prelude.thy b/spartan/lib/Prelude.thy
index c0abf31..0043c1e 100644
--- a/spartan/lib/Prelude.thy
+++ b/spartan/lib/Prelude.thy
@@ -139,7 +139,7 @@ lemmas
 subsection \<open>Notation\<close>
 
 definition ifelse_i ("if _ then _ else _")
-  where [implicit]: "if x then a else b \<equiv> ifelse ? x a b"
+  where [implicit]: "if x then a else b \<equiv> ifelse {} x a b"
 
 translations "if x then a else b" \<leftharpoondown> "CONST ifelse C x a b"
 
-- 
cgit v1.2.3