Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone



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 Source

Instantiate full as long as things are equal

Minimal complete definition



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 DontCare stuff.

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.