```
Definition a := [× nat, nat & nat].
```

I understand that `×`

is the functor `prod`

, but not sure about `[]`

and `&`

.

No idea but you can either `Set Printing Notations`

(or simply `Set Printing All`

) or `Locate "x"`

to find out.

isn't this just the usual MathComp style list notations applied to `prod`

? For example,`[:: x, y & l] = x :: y :: l`

Thanks! The printing worked, and @Karl Palmskog was right. :happy:

Tan Yee Jian has marked this topic as resolved.

Last updated: Oct 04 2023 at 19:01 UTC