Merge branch 'master' of github.com:idris-lang/Idris-dev
commitc2580dc6e34aa84208ae9a45103c73ce1a71975c
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateMon 20 Apr 2015, 00:17 (12 years ago)
parent289c05f4307917
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