Re: [isabelle] Collections: problems with sets of sets

Hi all,

> The problem goes away when I remove the [code nbe] declaration that
> comes after the instance proof of equal in Dlist.thy
> (
> I don't know about the precise semantics of [code nbe] wrt. normal code
> equations, but it seems to override the previous code equation.

all [code …] declarations simply override any default equation.

Btw. the explicit declaration is currently tested for addition.




PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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