idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-20 01:41:44 +03:00
Code Issues Projects Releases Wiki Activity

add shunting test

Browse Source
This commit is contained in:
André Videla 2023-10-24 17:11:27 +01:00
parent 1adb780e3f
commit 02a6751796
1 changed files with 21 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
tests/idris2/operators/operators001/Test.idr
View File

@ -1,13 +1,19 @@
module Test
import Data.Vect import Data.Vect
typebind infixr 0 =@ typebind infixr 0 =@
infixr 0 -@ infixr 0 -@
typebind infix 1 =@@
0 (=@) : (a : Type) -> (a -> Type) -> Type 0 (=@) : (a : Type) -> (a -> Type) -> Type
(=@) a f = (1 x : a) -> f x (=@) 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 : Type) -> Type
(-@) a b = (1 _ : a) -> b (-@) 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) Mk2 : (x : ty) =@ (y : ty) =@ S (x, y)
Mk3 : (x : ty) =@ ty -@ S x Mk3 : (x : ty) =@ ty -@ S x
Mk4 : ty -@ (x : 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 *> typebind infixr 0 *>