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 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'spartan/lib/List.thy')

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"
 
-- 
cgit v1.2.3