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

Minimal complete definition

synEq

Instances

SynEq ArgInfo

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq Level

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq PlusLevel

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq Sort

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq Term

Syntactic term equality ignores DontCare stuff.

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq Type

Syntactic equality ignores sorts.

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq Bool

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq a => SynEq (Arg a)

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 a, SynEq a) => SynEq (Abs a)

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 (Dom a)

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)

SynEq a => SynEq (Elim' a)

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 [a]

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

(SynEq a, SynEq b) => SynEq (a, b)

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

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

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