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

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

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

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

Type directed equality on values.

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

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

Syntax directed equality on atomic values

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

Type-directed equality on argument lists

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

Equality on Types

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

# Sorts

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

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

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

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

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

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

Check that the first sort equal to the second.