@@ -9,25 +9,26 @@
99 ||| The trivial constructor for `()`.
1010 MkUnit
1111
12−||| The non-dependent pair type, also known as conjunction.
13−||| @A the type of the left elements in the pair
14−||| @B the type of the left elements in the pair
15−%elim data Pair : (A : Type) -> (B : Type) -> Type where
16− ||| A pair of elements
17− ||| @a the left element of the pair
18− ||| @b the right element of the pair
19− MkPair : {A, B : Type} -> (a : A) -> (b : B) -> Pair A B
20−
21−||| Dependent pairs
22−|||
23−||| Dependent pairs represent existential quantification - they consist of a
24−||| witness for the existential claim and a proof that the property holds for
25−||| it. Another way to see dependent pairs is as just data - for instance, the
26−||| length of a vector paired with that vector.
27−|||
28−||| @ a the type of the witness @ P the type of the proof
29−data Sigma : (a : Type) -> (P : a -> Type) -> Type where
30− MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P
12+namespace Builtins
13+ ||| The non-dependent pair type, also known as conjunction.
14+ ||| @A the type of the left elements in the pair
15+ ||| @B the type of the left elements in the pair
16+ %elim data Pair : (A : Type) -> (B : Type) -> Type where
17+ ||| A pair of elements
18+ ||| @a the left element of the pair
19+ ||| @b the right element of the pair
20+ MkPair : {A, B : Type} -> (a : A) -> (b : B) -> Pair A B
21+
22+ ||| Dependent pairs
23+ |||
24+ ||| Dependent pairs represent existential quantification - they consist of a
25+ ||| witness for the existential claim and a proof that the property holds for
26+ ||| it. Another way to see dependent pairs is as just data - for instance, the
27+ ||| length of a vector paired with that vector.
28+ |||
29+ ||| @ a the type of the witness @ P the type of the proof
30+ data Sigma : (a : Type) -> (P : a -> Type) -> Type where
31+ MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P
3132
3233||| The empty type, also known as the trivially false proposition.
3334|||