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?

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

If you do `Print`

or `About`

on `COMPARABLE.compare`

you should get more info on the record.

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`

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

I think if you do `Print COMPARABLE.signature`

you will see the record.

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

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

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

If you do `unfold COMPARABLE.Build_signature`

or `unfold COMPARABLE.t`

in your proof that should unfold some things and simplify the goal.

you can also `Unset Printing Records`

Last updated: Jun 25 2024 at 15:02 UTC