diff options
| -rw-r--r-- | spartan/data/List.thy | 4 |
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" |