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

Safe HaskellNone

Agda.TypeChecking.Conversion

Contents

Synopsis

Documentation

sameVars :: Args -> Args -> BoolSource

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

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

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.

convError :: TypeError -> TCM ()Source

Ignore errors in irrelevant context.

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

Type directed equality on values.

unifyPointers :: t -> t1 -> t2 -> t3 -> t3Source

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

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 ()Source

Syntax directed equality on atomic values

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

Type-directed equality on eliminator spines

compareIrrelevant :: Type -> Term -> Term -> TCM ()Source

Compare two terms in irrelevant position. This always succeeds. However, we can dig for solutions of irrelevant metas in the terms we compare. (Certainly not the systematic solution, that'd be proof search...)

compareWithPol :: Polarity -> (Comparison -> a -> a -> TCM ()) -> a -> a -> TCM ()Source

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

Type-directed equality on argument lists

Types

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

Equality on Types

coerce :: Term -> Type -> Type -> TCM TermSource

coerce v a b coerces v : a to type b, returning a v' : b with maybe extra hidden applications or hidden abstractions.

In principle, this function can host coercive subtyping, but currently it only tries to fix problems with hidden function types.

Sorts

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

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

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

Check that the first sort equal to the second.