Re: [isabelle] Nominal Isabelle and pair types



Robert Rothenberg wrote:
  nominal_datatype labelled_formula =
    "\<guillemotleft>simple_label\<guillemotright> * formula"

Hi Rob,

note that this command does not quite do what you want. The type expression
"\<guillemotleft>simple_label\<guillemotright> * formula" is not even well-formed,
since the type of a binder must have the form "\<guillemotleft>T\<guillemotright>U".
The reason why Isabelle does not complain about the ill-formed type is that it does
not define a datatype with a constructor having one argument of type
"\<guillemotleft>simple_label\<guillemotright> * formula". Instead, it defines a
datatype with a zero-argument constructor which is named
"\<guillemotleft>simple_label\<guillemotright> * formula".

Greetings,
Stefan

--
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.