@@ -36,7 +36,8 @@ namespace Builtins
36 ||| it. Another way to see dependent pairs is as just data - for instance, the
36 ||| it. Another way to see dependent pairs is as just data - for instance, the
37 ||| length of a vector paired with that vector.
37 ||| length of a vector paired with that vector.
39− ||| @ a the type of the witness @ P the type of the proof
39+ ||| @ a the type of the witness
40+ ||| @ P the type of the proof
40 data Sigma : (a : Type) -> (P : a -> Type) -> Type where
41 data Sigma : (a : Type) -> (P : a -> Type) -> Type where
41 MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P
42 MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P