On 7 August 2010 18:14, dan portin
So my question, finally, is: what would be the general structure of the implementation of the state monad for a tableau-style theorem prover look like, schematically.
Hi Dan One would need a detailed knowledge of tableau-style theorem provers to answer that... In the code above Tableau is the same type after rewriting. If that's the case, maybe you don't need a state monad solution. However, if you are labelling something with /w/ which looks like an integer from your explanation, then first you want to make a variation of the Tableau datatype that holds the label, thus rewrite would be a type changing function: rewrite :: Tableau -> Tableau' Where Tableau' is an alternative definition of Tableau that includes a field for /w/ (possibly in the auxiliary types Status or Expr, which would likewise need an alternative definition). If this is what you want to do, you should be able to thread "number supply" through the rewrite and rule functions fairly simply with a state monad. rewrite :: Tableau -> State Int Tableau' Best wishes Stephen