Re: [isabelle] getting past ConstDefs.add_constdefs_i

Makarius writes:
> 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

fails, but 

  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 MHonArc.