Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

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

Instances details
SynEq Bool Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Bool -> Bool -> SynEqM (Bool, Bool)

synEq' :: Bool -> Bool -> SynEqM (Bool, Bool)

SynEq ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: ArgInfo -> ArgInfo -> SynEqM (ArgInfo, ArgInfo)

synEq' :: ArgInfo -> ArgInfo -> SynEqM (ArgInfo, ArgInfo)

SynEq LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

SynEq PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

SynEq Level Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Level -> Level -> SynEqM (Level, Level)

synEq' :: Level -> Level -> SynEqM (Level, Level)

SynEq Sort Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Sort -> Sort -> SynEqM (Sort, Sort)

synEq' :: Sort -> Sort -> SynEqM (Sort, Sort)

SynEq Type Source #

Syntactic equality ignores sorts.

Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Type -> Type -> SynEqM (Type, Type)

synEq' :: Type -> Type -> SynEqM (Type, Type)

SynEq Term Source #

Syntactic term equality ignores DontCare stuff.

Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Term -> Term -> SynEqM (Term, Term)

synEq' :: Term -> Term -> SynEqM (Term, Term)

SynEq a => SynEq [a] Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: [a] -> [a] -> SynEqM ([a], [a])

synEq' :: [a] -> [a] -> SynEqM ([a], [a])

SynEq a => SynEq (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Arg a -> Arg a -> SynEqM (Arg a, Arg a)

synEq' :: Arg a -> Arg a -> SynEqM (Arg a, Arg a)

(Subst t a, SynEq a) => SynEq (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Abs a -> Abs a -> SynEqM (Abs a, Abs a)

synEq' :: Abs a -> Abs a -> SynEqM (Abs a, Abs a)

SynEq a => SynEq (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Elim' a -> Elim' a -> SynEqM (Elim' a, Elim' a)

synEq' :: Elim' a -> Elim' a -> SynEqM (Elim' a, Elim' a)

SynEq a => SynEq (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Dom a -> Dom a -> SynEqM (Dom a, Dom a)

synEq' :: Dom a -> Dom a -> SynEqM (Dom a, Dom a)

checkSyntacticEquality :: (Instantiate a, SynEq a, MonadReduce m) => a -> a -> m ((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.

This means in particular that the returned v,v' cannot be MetaVs that are instantiated.