diff tests/datatypeP.lac @ 191:aa54250f58ac

Parametrized datatypes through explify
author Adam Chlipala <adamc@hcoop.net>
date Fri, 08 Aug 2008 10:28:32 -0400
parents
children 8a70e2919e86
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/datatypeP.lac	Fri Aug 08 10:28:32 2008 -0400
@@ -0,0 +1,10 @@
+datatype option a = None | Some of a
+
+val none : option int = None
+val some_1 : option int = Some 1
+
+val f = fn t ::: Type => fn x : option t =>
+        case x of None => None | Some x => Some (Some x)
+
+val none_again = f none
+val some_1_again = f some_1