[isabelle] Creating the type required for DatatypePackage.add_datatype_i



How should I create the Term.typ values required by the function
DatatypePackage.add_datatype_i when I want to represent one of the
types being defined (thus, a recursive occurrence)?

If I call add_datatype I can do something like

  add_datatype true
               ["foo"]
               [([], "foo", NoSyn, (* no idea what 1st and 3rd elements
                                      do here *)
                 [("zero", [], NoSyn),
                  ("suc", ["foo"], NoSyn)])]
               thy

but if I want to do this with add_datatype_i, I need something like

   add_datatype_i true
                  true
                  ["foo"]
                  [([], "foo", NoSyn,
                    [("zero", [], NoSyn),
                     ("suc", [????], NoSyn)])]

and I don't know what to put in ????

Simply trying

   Type("foo", [])

doesn't seem to work.

Michael.






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