The Coq mailing list

[Joachim Breitner <mail AT joachim-breitner.de>]

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.


-- 
Joachim Breitner
  
mail AT joachim-breitner.de
  http://www.joachim-breitner.de/

Attachment: signature.asc
Description: This is a digitally signed message part