Stream: Coq users

Topic: ✔ Nested sigT


view this post on Zulip 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)}
 }

view this post on Zulip 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.

view this post on Zulip Julin S (Jun 16 2022 at 06:48):

Thanks!

view this post on Zulip 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?

view this post on Zulip Olivier Laurent (Jun 16 2022 at 06:51):

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

view this post on Zulip Julin S (Jun 16 2022 at 07:07):

That worked as well. Thanks.

view this post on Zulip 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.

view this post on Zulip Notification Bot (Jun 16 2022 at 07:18):

Julin S has marked this topic as resolved.


Last updated: Jun 18 2024 at 08:01 UTC