Stream: Coq users

Topic: ✔ Nested sigT

Julin S (Jun 16 2022 at 05:48):

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)}
 }

Pierre Castéran (Jun 16 2022 at 06:39):

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.

Julin S (Jun 16 2022 at 06:48):

Thanks!

Julin S (Jun 16 2022 at 06:48):

So, for the a < b example, we can do like

Definition X : {a:nat & {b: nat | a < b}}.

right?

Olivier Laurent (Jun 16 2022 at 06:51):

You can also use {'(a,b) & a < b}.

Julin S (Jun 16 2022 at 07:07):

That worked as well. Thanks.

Julin S (Jun 16 2022 at 07:09):

Can have multiple values like Definition X'' : {'(a,b,c) & (a<b<c)}. as well.
Makes it concise and handy.

Notification Bot (Jun 16 2022 at 07:18):

Julin S has marked this topic as resolved.

Last updated: Oct 05 2023 at 02:01 UTC