Stream: math-comp users

Topic: ✔ What is this notation

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.

Pierre Roux (Nov 06 2022 at 18:02):

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

Notification Bot (Nov 06 2022 at 18:15):

walker has marked this topic as resolved.

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.

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: Apr 20 2024 at 09:01 UTC