Documentation

data ProofResult e Source #

data Proof r e p Source #

verifyProof :: (Monad m, Ord p, Show r, Show p) => (p -> m (Proof r e p)) -> (r -> [ProofResult e] -> ProofResult e -> ExceptT String m ()) -> p -> StateT (Map p (ProofResult e)) (ExceptT String m) (ProofResult e) Source #

renderProof :: (Monad m, Ord p, Show r) => (forall tp. e tp -> ShowS) -> (p -> m (Proof r e p)) -> p -> m ShowS Source #

renderProof' :: (Monad m, Ord p, Show r) => (forall tp. e tp -> ShowS) -> (p -> m (Proof r e p)) -> p -> StateT (Map p Int) (WriterT (Endo String) m) Int Source #

renderProofResult :: (forall tp. e tp -> ShowS) -> ProofResult e -> ShowS Source #

mapProof :: (forall tp. e tp -> e' tp) -> Proof r e p -> Proof r e' p Source #