Agda.TypeChecking.Conversion

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.