1 files changed, 8 insertions, 0 deletions
diff --git a/Test/test0/Types0.bpl b/Test/test0/Types0.bpl
new file mode 100644
index 00000000..7bb1dcef
--- /dev/null
+++ b/Test/test0/Types0.bpl
@@ -0,0 +1,8 @@
+type T, U;
+type V;
+
+function f([U,V]T, int) returns (U);
+function g(x: [U,V]T, y: int) returns (z: U);
+function h([U,V]T: int, y: int) returns (z: U);  // parse error
+function k(T: int, y: int) returns (U: [any]int);
+function l(x) returns (int);  // resolve error