Stream: Coq users

Topic: ✔ What is this notation?

Tan Yee Jian (Dec 28 2022 at 13:57):

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

Tan Yee Jian (Dec 28 2022 at 13:59):

I understand that × is the functor prod, but not sure about [] and &.

Pierre Roux (Dec 28 2022 at 14:16):

No idea but you can either Set Printing Notations (or simply Set Printing All) or Locate "x" to find out.

Karl Palmskog (Dec 28 2022 at 14:24):

isn't this just the usual MathComp style list notations applied to prod? For example,[:: x, y & l] = x :: y :: l

Tan Yee Jian (Dec 29 2022 at 06:36):

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

Notification Bot (Dec 29 2022 at 06:36):

Tan Yee Jian has marked this topic as resolved.

Last updated: Oct 04 2023 at 19:01 UTC