From c19533acfad3bbe603cd8a3d176e8b14f477573a Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 25 May 2020 19:36:30 +0200
Subject: notation

---
 spartan/data/List.thy | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'spartan')

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