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