They are just are library type except that we also provide syntactic sugar for them (I think we should). Definition (depends on #2):
data Sigma (A: Type) (P: A -> Type): Type =
sigma (,A: Type) (,P: A -> Type)
(a: A) (proof: P a): Sigma A P
The syntactic sugar is not entirely clear but this is the current proposal:
(a: A ** P a) to crate.core.sigma.Sigma A (\a => P a)
(a ** p a) to crate.core.sigma.Sigma.sigma a (p a)
Note that we should not naïvely translate to the above path to the sigma type defined in core but intelligently to the actual resolved binding (and rise an error if core is not available (as a module or in the future as a crate #14)).
The most important blocker or at least the first to encounter is the question of precedence and associativity to be able to connect
it to the rest of the grammar.
They are just are library type except that we also provide syntactic sugar for them (I think we should). Definition (depends on #2):
The syntactic sugar is not entirely clear but this is the current proposal:
(a: A ** P a)tocrate.core.sigma.Sigma A (\a => P a)(a ** p a)tocrate.core.sigma.Sigma.sigma a (p a)Note that we should not naïvely translate to the above path to the sigma type defined in core but intelligently to the actual resolved binding (and rise an error if
coreis not available (as a module or in the future as a crate #14)).The most important blocker or at least the first to encounter is the question of precedence and associativity to be able to connect it to the rest of the grammar.