mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-17 16:21:46 +03:00
13 lines
381 B
Idris
13 lines
381 B
Idris
|
-- Things like ( , ) ( ** ) () are special in that they denote more than
|
||
|
|
-- one thing at once. () can mean Unit or MkUnit, (,) can mean Pair or MkPair
|
||
|
|
-- Idiom brackets need to be able to work despite that, which is tested here
|
||
|
|
|
||
|
|
fez : IO Int
|
||
|
|
fez = pure 1
|
||
|
|
|
||
|
|
fez1 : IO (Int, ())
|
||
|
|
fez1 = [| MkPair fez (pure ()) |]
|
||
|
|
|
||
|
|
fez2 : IO (Int, Maybe Int)
|
||
|
|
fez2 = [| ( fez , (pure Nothing) ) |]
|