Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.Conversion
Contents
Sorts
Synopsis
sameVars :: Args -> Args -> Bool
equalTerm :: MonadTCM tcm => Type -> Term -> Term -> tcm Constraints
equalAtom :: MonadTCM tcm => Type -> Term -> Term -> tcm Constraints
equalArgs :: MonadTCM tcm => Type -> Args -> Args -> tcm Constraints
equalType :: MonadTCM tcm => Type -> Type -> tcm Constraints
compareTerm :: MonadTCM tcm => Comparison -> Type -> Term -> Term -> tcm Constraints
compareTel :: MonadTCM tcm => Comparison -> Telescope -> Telescope -> tcm Constraints
compareAtom :: MonadTCM tcm => Comparison -> Type -> Term -> Term -> tcm Constraints
compareArgs :: MonadTCM tcm => [Polarity] -> Type -> Args -> Args -> tcm Constraints
compareType :: MonadTCM tcm => Comparison -> Type -> Type -> tcm Constraints
leqType :: MonadTCM tcm => Type -> Type -> tcm Constraints
compareSort :: MonadTCM tcm => Comparison -> Sort -> Sort -> tcm Constraints
leqSort :: MonadTCM tcm => Sort -> Sort -> tcm Constraints
leqLevel :: MonadTCM tcm => Term -> Term -> tcm Constraints
equalLevel :: MonadTCM tcm => Term -> Term -> tcm Constraints
equalSort :: MonadTCM tcm => Sort -> Sort -> tcm Constraints
Documentation
sameVars :: Args -> Args -> BoolSource
Check if to lists of arguments are the same (and all variables). Precondition: the lists have the same length.
equalTerm :: MonadTCM tcm => Type -> Term -> Term -> tcm ConstraintsSource
equalAtom :: MonadTCM tcm => Type -> Term -> Term -> tcm ConstraintsSource
equalArgs :: MonadTCM tcm => Type -> Args -> Args -> tcm ConstraintsSource
equalType :: MonadTCM tcm => Type -> Type -> tcm ConstraintsSource
compareTerm :: MonadTCM tcm => Comparison -> Type -> Term -> Term -> tcm ConstraintsSource
Type directed equality on values.
compareTel :: MonadTCM tcm => Comparison -> Telescope -> Telescope -> tcm ConstraintsSource
compareAtom :: MonadTCM tcm => Comparison -> Type -> Term -> Term -> tcm ConstraintsSource
Syntax directed equality on atomic values
compareArgs :: MonadTCM tcm => [Polarity] -> Type -> Args -> Args -> tcm ConstraintsSource
Type-directed equality on argument lists
compareType :: MonadTCM tcm => Comparison -> Type -> Type -> tcm ConstraintsSource
Equality on Types
leqType :: MonadTCM tcm => Type -> Type -> tcm ConstraintsSource
Sorts
compareSort :: MonadTCM tcm => Comparison -> Sort -> Sort -> tcm ConstraintsSource
leqSort :: MonadTCM tcm => Sort -> Sort -> tcm ConstraintsSource
Check that the first sort is less or equal to the second.
leqLevel :: MonadTCM tcm => Term -> Term -> tcm ConstraintsSource
equalLevel :: MonadTCM tcm => Term -> Term -> tcm ConstraintsSource
equalSort :: MonadTCM tcm => Sort -> Sort -> tcm ConstraintsSource
Check that the first sort equal to the second.
Produced by Haddock version 2.4.2