Safe Haskell	None
Language	Haskell2010

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

class SynEq a
checkSyntacticEquality :: (Instantiate a, SynEq a, MonadReduce m) => a -> a -> m ((a, a), Bool)

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 Methods synEq :: LevelAtom -> LevelAtom -> SynEqM (LevelAtom, LevelAtom) synEq' :: LevelAtom -> LevelAtom -> SynEqM (LevelAtom, LevelAtom)
SynEq PlusLevel Source #
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: PlusLevel -> PlusLevel -> SynEqM (PlusLevel, PlusLevel) synEq' :: PlusLevel -> PlusLevel -> SynEqM (PlusLevel, PlusLevel)
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.