Re: [isabelle] State of the State Monad
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?
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
Andreas: Would you be also interested in consolidating Tree_Relabeling
with the fresh monad I've implemented on top of state?
This archive was generated by a fusion of
Pipermail (Mailman edition) and