The Coq mailing list

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

Hi Agnishom,

I'm rather puzzled - I assume you are saying that the syntax I gave, ie
{| c := ccc ; i := iii |}, is in fact a record.

But if so, why doesn't the split tactic work?

The following you gave:

Definition Person : Type := {
   name : String;
   age : int;
}.

I'm guessing you are saying that defines a record type in Coq.

However why I enter that I get the following error:

Definition Person : Type := {
  name : String;
  age : intCoq < Coq < Coq < }.
Toplevel input, characters 46-47:
>   name : String;
>                ^
Error:
Syntax error: '&' or '|' expected after [constr:operconstr level 200] 
(in [constr:operconstr]).

Cheers,

Jeremy


On 6/9/21 1:32 pm, Agnishom Chattopadhyay wrote:
> Records are like a product type, with desginated function for each 
> projection function. Informally, you can think of them as a class with 
> fields in some object oriented language.
>
> For example,
>
> class Person {
>    String name;
>    int age;
> }
>
> would be
>
> Definition Person : Type := {
>    name : String;
>    age : int;
> }.
>
> You can read the section titled "Records are Products" from 
> https://softwarefoundations.cis.upenn.edu/qc-current/Typeclasses.html 
> <https://softwarefoundations.cis.upenn.edu/qc-current/Typeclasses.html>
> (The rest of the page is not really relevant for this purpose.)
>
> Records are also a feature in OCaml or Haskell. You can google that.
>
>
>
> On Sun, Sep 5, 2021 at 10:20 PM Agnishom Chattopadhyay 
> <agnishom AT cmi.ac.in <mailto:agnishom AT cmi.ac.in>> 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