Re: [isabelle] making local definitions programmatically



Michael Norrish wrote:
> Florian Haftmann wrote:
>
>  > A further hint I want to add: LocalTheory.define etc. return the
>  > defined entity as a term.  Normally it is the best to use these
>  > directly to build up other definitions, lemmas etc.  This saves you
>  > from referring to suspected names of constants altogether.

> It seems I have have apply Context.map_proof_result for this to be
> useful.  If I omit this (as below), then the result includes a term
> that is a Free (not a Const), with no parameters.

It seems I was confused.  Context.map_proof_result is no use.
Whatever I do, LocalTheory.define doesn't return anything other than
an unadorned Free.

It seems that if I want to refer to other local constants, I should
construct a

  Const("local." ^ myconstname, dummyT)

and then Syntax.check it.

Is this best practice?

Michael.






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