| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.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.
- class SynEq a
- checkSyntacticEquality :: SynEq a => a -> a -> TCM ((a, a), Bool)
Documentation
Instantiate full as long as things are equal
Minimal complete definition
synEq
Instances
| 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.