Add %elim to tuples.
commit3d9115af85279eaf600943c12f3fa11995169b6c
authorJuliusz Chroboczek <jch@pps.univ-paris-diderot.fr>
dateThu 13 Nov 2014, 19:39 (12 years ago)
parentefd6f8a
libs/prelude/Builtins.idr+1−1
@@ -12,7 +12,7 @@
1212||| The non-dependent pair type, also known as conjunction.
1313||| @A the type of the left elements in the pair
1414||| @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
1616 ||| A pair of elements
1717 ||| @a the left element of the pair
1818 ||| @b the right element of the pair