Agda.TypeChecking.SyntacticEquality

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.

Documentation

class SynEq a

Instantiate full as long as things are equal

Instances

SynEq LevelAtom

SynEq PlusLevel

SynEq Level

SynEq Sort

SynEq Type

Syntactic equality ignores sorts.

SynEq Term

Syntactic term equality ignores DontCare stuff.

SynEq a => SynEq [a]

SynEq c => SynEq (ArgInfo c)

(Subst a, SynEq a) => SynEq (Abs a)

SynEq a => SynEq (Elim' a)

(SynEq a, SynEq c) => SynEq (Dom c a)

(SynEq a, SynEq c) => SynEq (Arg c a)

checkSyntacticEquality :: SynEq a => a -> a -> TCM ((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.