Stream: math-comp users

Topic: ✔ What is this notation


view this post on Zulip walker (Nov 06 2022 at 17:55):

I came along an expression that looks like this:

 {in map_to_list m2, forall x : prod_eqType K V, m1 !! x.1 != None}

I got it from move/hasPn:

I cannot figure out what is being said here,

I tried Locate "{ in _ , forall _ : _ , _}". and various of other variants (mostly truncating stuff from the right) but couldn't find anything.

view this post on Zulip Pierre Roux (Nov 06 2022 at 18:02):

You can always Set Printing All (or Set Printing Notation) in those cases.

view this post on Zulip Notification Bot (Nov 06 2022 at 18:15):

walker has marked this topic as resolved.

view this post on Zulip Ana de Almeida Borges (Nov 06 2022 at 19:32):

Note that while using Locate " stuff ", the _ need to be enclosed by spaces. Ie, "... _}" won't work, you need "... _ }" instead.

view this post on Zulip Pierre Roux (Nov 07 2022 at 08:27):

And you can also use Locate on single tokens, for instance Locate "in" would have worked here (of course it displays a bit more than what you are looking for).


Last updated: Jan 29 2023 at 18:03 UTC