@@ -12,7 +12,7 @@
12namespace Builtins
12namespace Builtins
13 ||| The non-dependent pair type, also known as conjunction.
13 ||| The non-dependent pair type, also known as conjunction.
14 ||| @A the type of the left elements in the pair
14 ||| @A the type of the left elements in the pair
15− ||| @B the type of the left elements in the pair
15+ ||| @B the type of the right elements in the pair
16 %elim data Pair : (A : Type) -> (B : Type) -> Type where
16 %elim data Pair : (A : Type) -> (B : Type) -> Type where
17 ||| A pair of elements
17 ||| A pair of elements
18 ||| @a the left element of the pair
18 ||| @a the left element of the pair
@@ -26,7 +26,7 @@ namespace Builtins
26 ||| The non-dependent pair type, also known as conjunction, usable with
26 ||| The non-dependent pair type, also known as conjunction, usable with
27 ||| UniqueTypes.
27 ||| UniqueTypes.
28 ||| @A the type of the left elements in the pair
28 ||| @A the type of the left elements in the pair
29− ||| @B the type of the left elements in the pair
29+ ||| @B the type of the right elements in the pair
30 data UPair : (A : AnyType) -> (B : AnyType) -> AnyType where
30 data UPair : (A : AnyType) -> (B : AnyType) -> AnyType where
31 ||| A pair of elements
31 ||| A pair of elements
32 ||| @a the left element of the pair
32 ||| @a the left element of the pair
@@ -74,7 +74,6 @@ void : Void -> a
74||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
74||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
75data Symbol_ : String -> Type where
75data Symbol_ : String -> Type where
78infix 5 ~=~
77infix 5 ~=~
80||| Explicit heterogeneous ("John Major") equality. Use this when Idris
79||| Explicit heterogeneous ("John Major") equality. Use this when Idris