@@ -33,19 +33,15 @@ namespace Builtins
3333 ||| @b the right element of the pair
3434 MkUPair : {A, B : AnyType} -> (a : A) -> (b : B) -> UPair A B
3535
36− -- Usage hints for erasure analysis
37− %used MkUPair a
38− %used MkUPair b
39−
40− ||| Dependent pairs
36+ ||| Dependent pairs aid in the construction of dependent types by
37+ ||| providing evidence that some value resides in the type.
4138 |||
42− ||| Dependent pairs represent existential quantification - they consist of a
43− ||| witness for the existential claim and a proof that the property holds for
44− ||| it. Another way to see dependent pairs is as just data - for instance, the
45− ||| length of a vector paired with that vector.
39+ ||| Formally, speaking, dependent pairs represent existential
40+ ||| quantification - they consist of a witness for the existential
41+ ||| claim and a proof that the property holds for it.
4642 |||
47− ||| @ a the type of the witness
48− ||| @ P the type of the proof
43+ ||| @ a the value to place in the type.
44+ ||| @ P the dependent type that requires the value.
4945 data Sigma : (a : Type) -> (P : a -> Type) -> Type where
5046 MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P
5147