diff --git a/tests/idris2/operators/operators001/Test.idr b/tests/idris2/operators/operators001/Test.idr index aa31184ae..e7dcfc9d4 100644 --- a/tests/idris2/operators/operators001/Test.idr +++ b/tests/idris2/operators/operators001/Test.idr @@ -1,13 +1,19 @@ +module Test import Data.Vect typebind infixr 0 =@ infixr 0 -@ +typebind infix 1 =@@ + 0 (=@) : (a : Type) -> (a -> Type) -> Type (=@) a f = (1 x : a) -> f x +0 (=@@) : (a : Type) -> (a -> Type) -> Type +(=@@) a f = (1 x : a) -> f x + (-@) : (a, b : Type) -> Type (-@) a b = (1 _ : a) -> b @@ -16,7 +22,21 @@ data S : {ty : Type} -> (x : ty) -> Type where Mk2 : (x : ty) =@ (y : ty) =@ S (x, y) Mk3 : (x : ty) =@ ty -@ S x Mk4 : ty -@ (x : ty) =@ S x - -- Chain : (x : ty =@ y : ty =@ S (x, y)) + +map : (x : a) =@@ b -@ (y : List a) =@ List b + +map2 : ((x : a) =@ b) -@ (y : List a) =@ List b + +map3 : (x : a) =@ b -@ (y : List a) =@ List b + +map4 : (x : a) =@ (b -@ (y : List a) =@ List b) + +test : Test.map === Test.map2 + +failing + test2 : Test.map === Test.map3 + +test3 : Test.map3 === Test.map4 typebind infixr 0 *>