Agda-2.2.6: A dependently typed functional programming language and proof assistant Source code Contents Index

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 -> Bool Source

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 Constraints Source

equalAtom :: MonadTCM tcm => Type -> Term -> Term -> tcm Constraints Source

equalArgs :: MonadTCM tcm => Type -> Args -> Args -> tcm Constraints Source

equalType :: MonadTCM tcm => Type -> Type -> tcm Constraints Source

compareTerm :: MonadTCM tcm => Comparison -> Type -> Term -> Term -> tcm Constraints Source

Type directed equality on values.

compareTel :: MonadTCM tcm => Comparison -> Telescope -> Telescope -> tcm Constraints Source

compareAtom :: MonadTCM tcm => Comparison -> Type -> Term -> Term -> tcm Constraints Source

Syntax directed equality on atomic values

compareArgs :: MonadTCM tcm => [Polarity] -> Type -> Args -> Args -> tcm Constraints Source

Type-directed equality on argument lists

compareType :: MonadTCM tcm => Comparison -> Type -> Type -> tcm Constraints Source

Equality on Types

leqType :: MonadTCM tcm => Type -> Type -> tcm Constraints Source

Sorts

compareSort :: MonadTCM tcm => Comparison -> Sort -> Sort -> tcm Constraints Source

leqSort :: MonadTCM tcm => Sort -> Sort -> tcm Constraints Source

Check that the first sort is less or equal to the second.

leqLevel :: MonadTCM tcm => Term -> Term -> tcm Constraints Source

equalLevel :: MonadTCM tcm => Term -> Term -> tcm Constraints Source

equalSort :: MonadTCM tcm => Sort -> Sort -> tcm Constraints Source

Check that the first sort equal to the second.

Produced by Haddock version 2.6.0