Re: [isabelle] Creating the type required for DatatypePackage.add_datatype_i
Michael Norrish wrote:
[(, "foo", NoSyn, (* no idea what 1st and 3rd elements
do here *)
the 1st element is the list of type parameters of the type constructor "foo",
and the 3rd element is used for specifying additional mixfix syntax for the
but if I want to do this with add_datatype_i, I need something like
[(, "foo", NoSyn,
[("zero", , NoSyn),
("suc", [????], NoSyn)])]
and I don't know what to put in ????
doesn't seem to work.
No, you have to give the full internal name of the type constructor, i.e.
"Foo.foo" instead of just "foo", where "Foo" is the name of the current theory.
You can compute the full name corresponding to a short name using the
function Sign.full_name. For example,
Sign.full_name my_theory "foo"
will return something like "Foo.foo".
By the way, the second boolean argument of add_datatype_i indicates whether
the constructors "zero" and "suc" of the datatype should be declared at the
"top level" of the theory, i.e. their internal names will be "Foo.zero" and
"Foo.suc", or whether the names of the constructors should be prefixed with
both the name of the theory and the name of the datatype, i.e. their internal
names will be "Foo.foo.zero" and "Foo.foo.suc". The latter enables you to
define several datatypes with constructors having the same name. In order
to get the default behaviour, you have to set the second argument of
add_datatype_i to false.
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