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
Const("local." ^ myconstname, dummyT)
and then Syntax.check it.
Is this best practice?
This archive was generated by a fusion of
Pipermail (Mailman edition) and