Agda-2.4.2.1: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell98

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

Documentation

class SynEq a Source

Instantiate full as long as things are equal

Minimal complete definition

synEq

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) 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.