Re: [isabelle] State of the State Monad



Hi Lars,

Replacing the existing state monad in Applicative_Lifting with yours shouldn't be hard. Except that if your theories become an AFP entry of their own, then we have a circular dependency between the entries.

So it might be easier to put your theory without the AFP entry integration into HOL/Library and do the integration in the respective AFP entries. What do you think?

Best,
Andreas

On 10/07/17 11:42, Lars Hupel wrote:
I've spent a few hours polishing my representation. See attachment.

Given the integration with the "Optics" and "Applicative" entries I'd
consider this worthy of inclusion in the AFP.

The existing "State_Monad" can be folded into its only use site
("~~/src/HOL/Proofs/Extraction/Higman_Extraction").

Andreas: Would you be also interested in consolidating Tree_Relabeling
with the fresh monad I've implemented on top of state?

Cheers
Lars





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