aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2020-05-25 19:36:30 +0200
committerJosh Chen2020-05-25 19:36:30 +0200
commitc19533acfad3bbe603cd8a3d176e8b14f477573a (patch)
treec0604b47ab8a4766d009fc762161f4314a915e48
parentf97d71514a309c212d3b20e560ce6482df0dd7ea (diff)
notation
Diffstat (limited to '')
-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"