I received advice here to use this type instead of vectors:

```
Definition tuple A n := { xs : list A | length xs = n }.
```

Which I ignored until today because vectors turned out to be hard to work with. I mistook this type for a record but it is not.. I tried finding exactly what is this but I failed to do so, I am struggling with the pipe symbol. and I just don't know how construct elements of this type, so I tried seing how coq cosntructs them and I tried little trick

```
Theorem x: tuple nat 0.
Proof.
unfold tuple.
assert(H: length (@nil nat) = 0 ). {auto. }
econstructor.
eauto.
Qed.
Print x.
```

and what I got is

```
x =
(let H : length [] = 0 := eq_refl in [] ↾ H) : tuple nat 0
: tuple nat 0
``` Which is even worse ... I cannot figure out what this flag symbol and I cannot figure out what that pipe symbol is in that specific context.
```

This is a sigma type which goes by the name `sig`

.

Doing `Locate sig.`

gives:

```
Inductive
sig (A : Type) (P : A -> Prop) : Type :=
exist : forall x : A, P x -> {x : A | P x}.
Arguments sig [A]%type_scope P%type_scope
Arguments exist [A]%type_scope
P%function_scope x _
```

So the constructor is called exist

In ltac you can even use the special `exists x.`

tactic to fill in the first field.

Unset Printing Notations is also your friend

That might not work in CoqIDE for example however, so you will have to go to the View options. (Which is a terrible usability feature imo)

yeah that doesn't work in vscoq either :(

In VsCoq if you do Ctrl+p

In vscoq or whatever you can do `Locate "{"`

also.

and then type >

And then type Coq

you should see options to display stuff

wow! thanks a lot!

wow I spent an hour searching for the bar thing in coq syntax manual trying to figure out what it is and now I have the general technique to deal with those issues.

Also `Locate`

is quite smart: `Locate "{ x | P }".`

will give:

```
Notation "{ x | P }" := (sig (fun x => P))
: type_scope (default interpretation)
```

Last updated: Jun 15 2024 at 08:01 UTC