@@ -12,7 +12,7 @@
1212namespace Builtins
1313 ||| The non-dependent pair type, also known as conjunction.
1414 ||| @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
1616 %elim data Pair : (A : Type) -> (B : Type) -> Type where
1717 ||| A pair of elements
1818 ||| @a the left element of the pair
@@ -26,7 +26,7 @@ namespace Builtins
2626 ||| The non-dependent pair type, also known as conjunction, usable with
2727 ||| UniqueTypes.
2828 ||| @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
3030 data UPair : (A : AnyType) -> (B : AnyType) -> AnyType where
3131 ||| A pair of elements
3232 ||| @a the left element of the pair
@@ -74,7 +74,6 @@ void : Void -> a
7474||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
7575data Symbol_ : String -> Type where
7676
77−
7877infix 5 ~=~
7978
8079||| Explicit heterogeneous ("John Major") equality. Use this when Idris