# HG changeset patch
# User wenzelm
# Date 1582806469 -3600
# Node ID 3488c0eb4cc857d41f88f9ae3215d986b0e7e81f
# Parent  e8da4a8d364acf28ba091cddadee39934918d6ac
more complete signature;

diff -r e8da4a8d364a -r 3488c0eb4cc8 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Thu Feb 27 12:58:03 2020 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Thu Feb 27 13:27:49 2020 +0100
@@ -879,7 +879,7 @@
 
   int_atom, bool_atom, unit_atom,
 
-  tree, properties, string, int, bool, unit, pair, triple, list, variant
+  tree, properties, string, int, bool, unit, pair, triple, list, option, variant
 )
 where
 
@@ -947,6 +947,10 @@
 list :: T a -> T [a]
 list f xs = map (node . f) xs
 
+option :: T a -> T (Maybe a)
+option _ Nothing = []
+option f (Just x) = [node (f x)]
+
 variant :: [V a] -> T a
 variant fs x = [tagged (the (get_index (\f -> f x) fs))]
 \<close>
@@ -966,7 +970,7 @@
 
   int_atom, bool_atom, unit_atom,
 
-  tree, properties, string, int, bool, unit, pair, triple, list, variant
+  tree, properties, string, int, bool, unit, pair, triple, list, option, variant
 )
 where