From 696796e1dcea137ee9b5c270b233892dd3267155 Mon Sep 17 00:00:00 2001
From: qadeer <qadeer@microsoft.com>
Date: Wed, 5 Oct 2011 19:11:23 -0700
Subject: implementing datatypes

---
 Test/datatypes/t1.bpl | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 Test/datatypes/t1.bpl

(limited to 'Test/datatypes')

diff --git a/Test/datatypes/t1.bpl b/Test/datatypes/t1.bpl
new file mode 100644
index 00000000..61409465
--- /dev/null
+++ b/Test/datatypes/t1.bpl
@@ -0,0 +1,20 @@
+type TT;
+type {:datatype} Tree;
+function {:constructor} leaf() : Tree;
+function {:constructor} node(value:TT, children:TreeList) : Tree;
+
+type {:datatype} TreeList;
+function {:constructor} cons(car:Tree, cdr:TreeList) : TreeList;
+function {:constructor} nil() : TreeList;
+
+procedure foo() 
+{
+  var a: Tree;
+  var b: TreeList;
+  var x: TT;
+
+  assert value#node(node(x, nil())) == x;
+  assert children#node(node(x, nil())) == nil();
+  
+  assert (cons(leaf(), nil()) == nil());
+}
\ No newline at end of file
-- 
cgit v1.2.3