Safe Haskell | None |
---|
- externals :: [External]
- verifyEqualityLeftToRightT :: MonadCatch m => CoreExpr -> CoreExpr -> Rewrite c m CoreExpr -> Translate c m a ()
- verifyEqualityCommonTargetT :: MonadCatch m => CoreExpr -> CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Translate c m a ()
- verifyIsomorphismT :: CoreExpr -> CoreExpr -> Rewrite c HermitM CoreExpr -> Rewrite c HermitM CoreExpr -> Translate c HermitM a ()
- verifyRetractionT :: CoreExpr -> CoreExpr -> Rewrite c HermitM CoreExpr -> Translate c HermitM a ()
- retractionBR :: forall c. Maybe (Rewrite c HermitM CoreExpr) -> CoreExpr -> CoreExpr -> BiRewrite c HermitM CoreExpr
Equational Reasoning
verifyEqualityLeftToRightT :: MonadCatch m => CoreExpr -> CoreExpr -> Rewrite c m CoreExpr -> Translate c m a ()Source
Given two expressions, and a rewrite from the former to the latter, verify that rewrite.
verifyEqualityCommonTargetT :: MonadCatch m => CoreExpr -> CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Translate c m a ()Source
Given two expressions, and a rewrite from the former to the latter, verify that rewrite.
verifyIsomorphismT :: CoreExpr -> CoreExpr -> Rewrite c HermitM CoreExpr -> Rewrite c HermitM CoreExpr -> Translate c HermitM a ()Source
Given f :: X -> Y and g :: Y -> X, verify that f (g y) ==> y and g (f x) ==> x.