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

Safe Haskell | Safe-Infered

Agda.TypeChecking.Conversion

Contents

- Sorts

Synopsis

- mlevel :: TCM (Maybe Term)
- nextPolarity :: [Polarity] -> (Polarity, [Polarity])
- sameVars :: Args -> Args -> Bool
- intersectVars :: Args -> Args -> Maybe [Bool]
- equalTerm :: Type -> Term -> Term -> TCM ()
- equalAtom :: Type -> Term -> Term -> TCM ()
- equalType :: Type -> Type -> TCM ()
- compareTerm :: Comparison -> Type -> Term -> Term -> TCM ()
- compareTerm' :: Comparison -> Type -> Term -> Term -> TCM ()
- compareTel :: Type -> Type -> Comparison -> Telescope -> Telescope -> TCM ()
- compareAtom :: Comparison -> Type -> Term -> Term -> TCM ()
- compareElims :: [Polarity] -> Type -> Term -> [Elim] -> [Elim] -> TCM ()
- compareArgs :: [Polarity] -> Type -> Term -> Args -> Args -> TCM ()
- compareType :: Comparison -> Type -> Type -> TCM ()
- leqType :: Type -> Type -> TCM ()
- compareSort :: Comparison -> Sort -> Sort -> TCM ()
- leqSort :: Sort -> Sort -> TCM ()
- leqLevel :: Level -> Level -> TCM ()
- equalLevel :: Level -> Level -> TCM ()
- equalSort :: Sort -> Sort -> TCM ()

# Documentation

mlevel :: TCM (Maybe Term)

nextPolarity :: [Polarity] -> (Polarity, [Polarity])

sameVars :: Args -> Args -> Bool

Check if to lists of arguments are the same (and all variables). Precondition: the lists have the same length.

intersectVars :: Args -> Args -> Maybe [Bool]

`intersectVars us vs` checks whether all relevant elements in `us` and `vs` are variables, and if yes, returns a prune list which says `True` for arguments which are different and can be pruned.

equalTerm :: Type -> Term -> Term -> TCM ()

equalAtom :: Type -> Term -> Term -> TCM ()

equalType :: Type -> Type -> TCM ()

compareTerm :: Comparison -> Type -> Term -> Term -> TCM ()

Type directed equality on values.

compareTerm' :: Comparison -> Type -> Term -> Term -> TCM ()

compareTel :: Type -> Type -> Comparison -> Telescope -> Telescope -> TCM ()

`compareTel t1 t2 cmp tel1 tel1` checks whether pointwise `tel1 `cmp` tel2` and complains that `t2 `cmp` t1` failed if not.

compareAtom :: Comparison -> Type -> Term -> Term -> TCM ()

Syntax directed equality on atomic values

compareElims :: [Polarity] -> Type -> Term -> [Elim] -> [Elim] -> TCM ()

Type-directed equality on eliminator spines

compareArgs :: [Polarity] -> Type -> Term -> Args -> Args -> TCM ()

Type-directed equality on argument lists

compareType :: Comparison -> Type -> Type -> TCM ()

Equality on Types

leqType :: Type -> Type -> TCM ()

# Sorts

compareSort :: Comparison -> Sort -> Sort -> TCM ()

leqSort :: Sort -> Sort -> TCM ()

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

leqLevel :: Level -> Level -> TCM ()

equalLevel :: Level -> Level -> TCM ()

equalSort :: Sort -> Sort -> TCM ()

Check that the first sort equal to the second.