Re: [isabelle] State of the State Monad

Hi Lars,

I've ported the tree relabelling (AFP/6a4641399c0a). I had to prove a bunch of lemmas about how the state monad operations interact. They are at the top of Tree_Relabelling.thy, but you might want to move them to State_Monad in HOL/Library.


On 12/07/17 06:03, Lars Hupel wrote:
Good point. If nobody objects I'll do that later this week. I was
planning to clean up some stuff in the vicinity ("Finite_Map") anyway.

See now Isabelle/d157195a468a and AFP/9f41cb6d9cfa.

I'll leave the porting of the tree relabeling to you, Andreas :-)


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