The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

Yes, I tried split, I get this

> split.
> ^^^^^^
Error: Not an inductive product.

As for exact, I need to have that result already as a hypothesis or 
proved theorem, don't I?

Cheers,

Jeremy

On 6/9/21 1:20 pm, Agnishom Chattopadhyay wrote:
> 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 
> <mailto: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