rudimentary support for Haskell
authorhaftmann
Tue, 25 Sep 2007 21:08:36 +0200
changeset 24717 56ba87ec8d31
parent 24716 483f0a64271f
child 24718 16b11ba36350
rudimentary support for Haskell
src/HOL/Library/ML_String.thy
--- a/src/HOL/Library/ML_String.thy	Tue Sep 25 21:08:35 2007 +0200
+++ b/src/HOL/Library/ML_String.thy	Tue Sep 25 21:08:36 2007 +0200
@@ -47,6 +47,7 @@
 
 code_type ml_string
   (SML "string")
+  (Haskell "String")
 
 setup {*
 let
@@ -65,9 +66,16 @@
 end
 *}
 
+code_const STR
+  (Haskell "_")
+
 code_reserved SML string
 
+code_instance ml_string :: eq
+  (Haskell -)
+
 code_const "op = \<Colon> ml_string \<Rightarrow> ml_string \<Rightarrow> bool"
   (SML "!((_ : string) = _)")
+  (Haskell infixl 4 "==")
 
 end