Examples:

- A value of a Σ type must have a proof inside:
`exist Odd 1 …`

. How can I put a proof there without giving it a name? - An instance of [
`Countable`

] is a record that contains two functions and a proof that one retracts the other. How do I write that proof in?

I know that I can write the proof separately and assign it to a name with a `Theorem`

or a `Lemma`

. But it would be cumbersome. Is there a way to do it inline?

[`Countable`

]: https://plv.mpi-sws.org/coqdoc/stdpp/stdpp.base.html#lab9

I also know that I can use `ltac:(…)`

to put some Ltac inline, but it is awkward. Is it the only way?

Awkward because I cannot see the context and without seeing the context I find it hard to build a suitable Ltac snippet.

ltac just builds terms

you can `Print`

your definition or theorem to see what ltac produced

eg

```
Lemma foo_countable : Countable foo.
Proof. some ltac. Qed.
Print foo_countable.
```

the print will say something like `(* foo_countable = {| encode := ...; decode := ...; decode_encode := ... |} *)`

if you do `Definition foo_countable_alt := {| encode := ...; decode := ...; decode_encode := ... |}`

it will work too

What do these fancy "{| … |}" braces do?

it's record syntax

if you `Set Printing All`

to disable the sugared printing it will be something like `@Build_Countable foo ... ... ...`

instead

Oh, I see. I was lost between the notation for defining record types and record values.

Last updated: Jun 17 2024 at 22:01 UTC