git.iko.soy/Idris-dev
on e35d643 help sign in
Idris-dev/test/basic023/sections.idr
34 lines 807 B history raw
1postInc : Nat -> Nat
2postInc = (`plus` 1)
4infixr 8 `cons`
5cons : Int -> List Int -> List Int
6cons = (::)
8namespace A
9 infixr 8 `nmul`
10 nmul : Nat -> Nat -> Nat
11 nmul = (*)
13namespace B
14 nmul : Nat -> Nat -> Nat
15 nmul _ y = y
17prefix 1 :/
18(:/) : Nat -> Nat
19(:/) = (1 `plus`)
21main : IO ()
22main = do
23 printLn $ (1 `cons`) [2] == [1,2]
24 printLn $ (1 ::) [2] == [1,2]
25 printLn $ (`cons` [2]) 1 == [1,2]
26 printLn $ (:: [2]) 1 == [1,2]
27 let x : Integer = 4
28 printLn $ (- x) == -4 -- prefix, not section
29 let io : IO Integer = pure 9
30 printLn $ (! io) == 9 -- prefix, not section
31 printLn $ (:/ 3) == 4 -- custom prefix operator (#2571)
32 printLn $ 1 `cons` 2 `cons` [3] == [1,2,3]
33 printLn $ 2 `A.nmul` 3 `B.nmul` 5 == 10
34 printLn $ 2 `B.nmul` 3 `A.nmul` 5 == 15