@@ -12,7 +12,7 @@
12||| The non-dependent pair type, also known as conjunction.
12||| The non-dependent pair type, also known as conjunction.
13||| @A the type of the left elements in the pair
13||| @A the type of the left elements in the pair
14||| @B the type of the left elements in the pair
14||| @B the type of the left elements in the pair
15−data Pair : (A : Type) -> (B : Type) -> Type where
15+%elim data Pair : (A : Type) -> (B : Type) -> Type where
16 ||| A pair of elements
16 ||| A pair of elements
17 ||| @a the left element of the pair
17 ||| @a the left element of the pair
18 ||| @b the right element of the pair
18 ||| @b the right element of the pair