[isabelle] getting past ConstDefs.add_constdefs_i
I have a definitional term, of the form
Const ("==", ty) $ Free(name, ty') $ tm
such that it certifies with respect to a given theory, thy.
> cterm_of thy eqt;
val it =
TRY \<acute>j :== the (h_val \<acute>the_heap \<acute>i) CATCH SKIP END"
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",
What am I likely to be doing wrong in my invocation of
This archive was generated by a fusion of
Pipermail (Mailman edition) and