Re: [isabelle] Generic Contexts and Generic Data

Hi Christian,

> The reason why I'm asking is that I recently found out that my "add"
> function is actually called 3 times every time "add'" is called and the
> morphism applied to "value" seems to be different the last time (i.e.,
> constants, generated via "BNF_LFP_Rec_Sugar.add_primrec" that are
> "Const"s as expected the first 2 times, are "Free"s the 3rd time).

this is quire regular: usually a declaration in a local theory has
effect on three levels:

1. the background theory
2. the target context itself
3. the hypothetical surface context (hence the »Free«s)

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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