Stream: Coq users

Topic: ✔ What is this notation?


view this post on Zulip Tan Yee Jian (Dec 28 2022 at 13:57):

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

view this post on Zulip Tan Yee Jian (Dec 28 2022 at 13:59):

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

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

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

view this post on Zulip Tan Yee Jian (Dec 29 2022 at 06:36):

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

view this post on Zulip Notification Bot (Dec 29 2022 at 06:36):

Tan Yee Jian has marked this topic as resolved.


Last updated: Jul 25 2024 at 15:02 UTC