sigT
for one variable looks like {x:A & P x}
, right?
How can we extend it to more than one variable (disregarding the fact that we got sigT2
. To find out how it can be extended to sigTn
)?
I was trying to have something like {a b | (fun a b => a < b)}
How would it look like?
Is it like
{a:nat &
{b:nat & (fun b => a < b)}
}
Is the following definition OK?
Definition X : {a:nat & {b: nat & {c: nat | a + b = c}}}.
now exists 3, 4, 7.
Defined.
Compute projT1 X.
Thanks!
So, for the a < b
example, we can do like
Definition X : {a:nat & {b: nat | a < b}}.
right?
You can also use {'(a,b) & a < b}
.
That worked as well. Thanks.
Can have multiple values like Definition X'' : {'(a,b,c) & (a<b<c)}.
as well.
Makes it concise and handy.
Julin S has marked this topic as resolved.
Last updated: Oct 05 2023 at 02:01 UTC