Re: [isabelle] getting past ConstDefs.add_constdefs_i
> On Tue, 28 Feb 2006, Michael Norrish wrote:
> > What am I likely to be doing wrong in my invocation of add_constdefs_i?
> This is hard to guess from a distance.
Trying to step through the code, inasmuch as this is possible without
hitting hidden functions, I get to the point where
ProofContext.cert_term (ProofContext.init thy) tm
cterm_of thy tm
Having looked at the code, I'm now pretty sure the reason for this is
calls certify_typ on the types of its argument (using map_term_types),
does not. It would be nice if the two behaved a little more
consistently, but I can now deal with the issue. In particular, if
you pass Consts.certify a term that doesn't have its type
abbreviations expanded, then it will complain. The action of
certifying a type does this expansion (among other things, I'm sure).
> 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 'definition' element.
When implemented, please document the ML API for this new entry-point!
> Note that Constdefs.add_constdefs_i produces extra noise on the message
> channel -- this is a toplevel command after all.
Yes, this is what I want because I'm implementing a top-level command
This archive was generated by a fusion of
Pipermail (Mailman edition) and