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,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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