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

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 :: (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

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

checkSyntacticEquality :: (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.