The Coq mailing list

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

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

(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> 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> 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