Comment formatting tweak for Sigma
commit6c428f3be0bb85d29a9c223a76d90f9f883feec4
authorSteven Shaw <steven@steshaw.org>
dateMon 20 Apr 2015, 03:51 (12 years ago)
parent3ac0d5a
libs/prelude/Builtins.idr+2−1
@@ -36,7 +36,8 @@ namespace Builtins
3636 ||| it. Another way to see dependent pairs is as just data - for instance, the
3737 ||| length of a vector paired with that vector.
3838 |||
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
4041 data Sigma : (a : Type) -> (P : a -> Type) -> Type where
4142 MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P
4243