| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Mikan.TypeChecking.SyntacticEquality
Description
A syntactic equality check that takes meta instantiations into account, but does not reduce. It replaces
(v, v') <- instantiateFull (v, v') v == v'
by a more efficient routine which only traverses and instantiates the terms as long as they are equal.
Synopsis
- checkSyntacticEquality :: (SynEq a, MonadReduce m) => a -> a -> (a -> a -> m b) -> (a -> a -> m b) -> m b
- class SynEq a
Documentation
checkSyntacticEquality Source #
Arguments
| :: (SynEq a, MonadReduce m) | |
| => a | |
| -> a | |
| -> (a -> a -> m b) | Continuation used upon success. |
| -> (a -> a -> m b) | Continuation used upon failure. |
| -> m b |
Syntactic equality check for terms.
Morally, checkSyntacticEquality behaves as if it were
implemented as:
checkSyntacticEquality v v' s f = do (v, v') <- instantiateFull (v, v') if v == v' then s v v' else f v v'
with the follow caveat:
- Both
vandv'are only guaranteed to fully instantiated to the depth at which they are syntactically equal.
A type is SynEq if it can be checked for syntactic equality.
Minimal complete definition
synEq