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 -> TCM ((a, a), Bool)
Documentation
Instantiate full as long as things are equal
synEq
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 c => SynEq (ArgInfo c) Source | |
(Subst a, SynEq a) => SynEq (Abs a) Source | |
SynEq a => SynEq (Elim' a) Source | |
(SynEq a, SynEq c) => SynEq (Dom c a) Source | |
(SynEq a, SynEq c) => SynEq (Arg c a) Source |
checkSyntacticEquality :: SynEq a => a -> a -> TCM ((a, a), Bool) Source
Syntactic equality check for terms.
checkSyntacticEquality v v' = do
(v,v') <- instantiateFull (v,v')
return ((v,v'), v==v')
only that v,v'
are only fully instantiated to the depth
where they are equal.