Re: [isabelle] getting past ConstDefs.add_constdefs_i
On Tue, 28 Feb 2006, Michael Norrish wrote:
> > cterm_of thy eqt;
> val it =
> "foo_body ==
> TRY \<acute>j :== the (h_val \<acute>the_heap \<acute>i) CATCH SKIP END"
> : Thm.cterm
> But, if I try to use this as the basis for a definition, I get an
> error from the constant certification part of the code:
> > thy |> Constdefs.add_constdefs_i (, [(NONE, (("", ), eqt))]);
> ("Illegal type for constant \"mytest.globals.the_heap\" :: globals => addr => word8",
> ) raised
> What am I likely to be doing wrong in my invocation of add_constdefs_i?
This is hard to guess from a distance.
Generally speaking, add_constdefs_i is just the internal version of a
user-level command -- it is common practice to provide both external and
internal version just to make sure that ML packages can always invoke each
other. For basic definitions the primitive add_consts/add_defs are
usually easier to use in ML. Even more, constdefs is about to become a
legacy feature pretty soon, being superceded by a more general
Anyway, add_constdefs_i actually does work for me as follows:
val eq = Logic.mk_equals (Free ("x", HOLogic.boolT), Const ("True", HOLogic.boolT));
val thy =
Theory.begin_theory "Test" [Main.thy]
|> Constdefs.add_constdefs_i (, [(NONE, (("", ), eq))]);
Note that Constdefs.add_constdefs_i produces extra noise on the message
channel -- this is a toplevel command after all.
This archive was generated by a fusion of
Pipermail (Mailman edition) and