1 files changed, 20 insertions, 0 deletions
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