diff options
| author | Josh Chen | 2020-05-25 19:36:30 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-05-25 19:36:30 +0200 |
| commit | c19533acfad3bbe603cd8a3d176e8b14f477573a (patch) | |
| tree | c0604b47ab8a4766d009fc762161f4314a915e48 | |
| parent | f97d71514a309c212d3b20e560ce6482df0dd7ea (diff) | |
notation
| -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" |