aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--spartan/data/List.thy4
1 files changed, 4 insertions, 0 deletions
diff --git a/spartan/data/List.thy b/spartan/data/List.thy
index 323ef7e..a6c41c6 100644
--- a/spartan/data/List.thy
+++ b/spartan/data/List.thy
@@ -71,6 +71,10 @@ definition tail_i ("tail")
definition map_i ("map")
where [implicit]: "map \<equiv> List.map ? ?"
+translations
+ "tail" \<leftharpoondown> "CONST List.tail A"
+ "map" \<leftharpoondown> "CONST List.map A B"
+
Lemma tail_type [typechk]:
assumes "A: U i" "xs: List A"
shows "tail xs: List A"