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 Bool

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq ArgInfo

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq LevelAtom

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq PlusLevel

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq Level

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq Sort

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

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

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

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 t 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 (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 (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)

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.