The Coq mailing list

[Agnishom Chattopadhyay <agnishom AT cmi.ac.in>]

Locate locates notation that is defined by the programmer. I believe that "{|" is syntax which is part of Gallina.

As for the next step, have you tried split? You can also try solving this with exact.

--agnishom

On Sun, Sep 5, 2021, 21:25 Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> wrote:

Hi,

I have a hypothesis (got by playing around with someone else's code) of
the form {| c := ccc ; i := iii |}

The command Locate "{|". produces no results.

I found in the documentation a syntax definition

term_record::={| field_def*; ;? |}

but I can't find anything about what that means or what you can do with it.

Does it mean I have a thing of type ccc and another thing of type iii?

If so how do I actually get hold of those things?

Then, when I have a goal of the form {| c := ccc ; i := iii |}
what does that mean and what is the next step to solving it?

Thanks

Jeremy