## Stream: Coq users

### Topic: What does any value inside `{| ... |}` mean?

#### kumar (Apr 08 2022 at 15:13):

for example I have a proof that I need to resolve and it has a specific function

``````  (fun
_ : {|
COMPARABLE.compare :=
fun id1 id2 : Bond_id_repr.t =>
let
'(t0, y) := (id1, id2) in
let
'Bond_id_repr.Tx_rollup_bond_id id3 := t0 in
let
'Bond_id_repr.Tx_rollup_bond_id id4 := y in
Tx_rollup_repr.compare id3 id4
|}.(COMPARABLE.t) => True)
``````

what do things in `{| .. |}` mean?

#### Ali Caglayan (Apr 08 2022 at 15:25):

That is a constructor of a record. So if you have:

``````Record A := {
b : B ;
c : C ;
}.
``````

and you had `x : B`, `y : C` you could have

``````{| b := x ; c := y |} : A
``````

#### Ali Caglayan (Apr 08 2022 at 15:26):

If you do `Print` or `About` on `COMPARABLE.compare` you should get more info on the record.

#### kumar (Apr 08 2022 at 15:46):

oh so multiline assigments in coq are just syntactic sugar over records?

I did do a `Print COMPARABLE.compare` and I get this

``````COMPARABLE.compare =
fun (t : Set) (s : COMPARABLE.signature) => s.(COMPARABLE.compare)
: forall t : Set, COMPARABLE.signature -> t -> t -> int
``````

so this means it returns a `Prop` Type `COMPARABLE.signature -> t -> t -> int`

#### kumar (Apr 08 2022 at 15:53):

but this would be the type of the function input since it's `(fun _ : <...>)`

#### Ali Caglayan (Apr 08 2022 at 16:06):

I think if you do `Print COMPARABLE.signature` you will see the record.

#### Ali Caglayan (Apr 08 2022 at 16:07):

If this is from CoqOfOcaml then this record probably has two fields COMPARABLE.t and COMPARABLE.compare

#### Ali Caglayan (Apr 08 2022 at 16:07):

Note that whatever you wrote first is actually a projection of a record `{| ... |}.(COMPARABLE.t)`

#### Ali Caglayan (Apr 08 2022 at 16:09):

so this means take the `COMPARABLE.signature` which has field `COMPARABLE.compare` as specified and take the `COMPARABLE.t` projection. Since `COMPARABLE.compare` takes in a `COMPARABLE.t` I can deduce that it must be `(fun _ : Bond_id_repr.t => True)` or something

#### Ali Caglayan (Apr 08 2022 at 16:10):

If you do `unfold COMPARABLE.Build_signature` or `unfold COMPARABLE.t` in your proof that should unfold some things and simplify the goal.

#### Gaëtan Gilbert (Apr 08 2022 at 16:10):

you can also `Unset Printing Records`

Last updated: Sep 23 2023 at 08:01 UTC