Safe Haskell | None |
---|---|
Language | Haskell98 |
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.
- class SynEq a
- checkSyntacticEquality :: SynEq a => a -> a -> ReduceM ((a, a), Bool)
Documentation
Instantiate full as long as things are equal
synEq
SynEq ArgInfo Source # | |
SynEq LevelAtom Source # | |
SynEq PlusLevel Source # | |
SynEq Level Source # | |
SynEq Sort Source # | |
SynEq Type Source # | Syntactic equality ignores sorts. |
SynEq Term Source # | Syntactic term equality ignores |
SynEq a => SynEq [a] Source # | |
SynEq a => SynEq (Dom a) Source # | |
SynEq a => SynEq (Arg a) Source # | |
(Subst t a, SynEq a) => SynEq (Abs a) Source # | |
SynEq a => SynEq (Elim' a) Source # | |