diff --git a/tests/pos/eta_cons.fq b/tests/pos/eta_cons.fq new file mode 100644 index 000000000..38f633755 --- /dev/null +++ b/tests/pos/eta_cons.fq @@ -0,0 +1,24 @@ +fixpoint "--rewrite" +fixpoint "--allowho" +fixpoint "--etabeta" + +constant f : (func(0 , [int; int; int])) +define f (x : int, y: int) : int = {(x + y)} + +constant g : (func(0 , [int; int; int])) +define g (a : int, b: int) : int = {(b + a)} + + +data Ty 0 = [ + | Cons {mkCons : func(0 , [int; int; int])} +] + +constant Cons : (func(0 , [func(0 , [int; int; int]); Ty])) + +expand [1 : True; 2 : True] + +constraint: + env [] + lhs {VV1 : Tuple | true } + rhs {VV2 : Tuple | (Cons f = Cons g) } + id 2 tag [] \ No newline at end of file