The Coq mailing list

[Guillaume Allais <guillaume.allais AT ens-lyon.org>]

Hi Joachim,

One way of achieving this is to define a record for `Pair`'s
arguments and to declare `Pair` as an implicit coercion from
that record type to the `OptPair` type. In other words:

============================================================
Record OptPairRecord a b := { fst : a; snd : b }.

Inductive OptPair a b :=
  | Pair : OptPairRecord a b -> OptPair a b
  | NoPair.

Coercion Pair : OptPairRecord >-> OptPair.

Definition c : OptPair nat nat := {| fst := 5; snd := 3 |}.
============================================================

Cheers,
--
gallais

On 21/11/17 18:22, Joachim Breitner wrote:
> Dear all,
>
>
> if I read the reference manual correctly, then
>
>     Definition b := {| x := 5; y := 3 |}.
>
> is just syntactic sugar for
>
>     Definition b := Build_point 5 3.
>
> This makes me wonder: Can I register, for a type t that is not defined
> using Record, a “build” function and “field names” so that the user can
> use record syntax?
>
> For example given
>
>     Inductive OptPair a b := pair a b | no_pair.
>
> can I somehow make
>
>     Definition c := {| fst := 5; snd := 3 |}.
>
> accepted notation for 
>
>     Definition c := pair 5 3
>
>
> Thanks,
> Joachim
>
> BTW, the next question will be if that desugaring then works with the 
>
>     Instance ... := { … }.
>
> notation.
>
>