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

Safe Haskell | None

Agda.TypeChecking.Conversion

Contents

- Types
- Sorts

Synopsis

- mlevel :: TCM (Maybe Term)
- sameVars :: Args -> Args -> Bool
- intersectVars :: Args -> Args -> Maybe [Bool]
- equalTerm :: Type -> Term -> Term -> TCM ()
- equalAtom :: Type -> Term -> Term -> TCM ()
- equalType :: Type -> Type -> TCM ()
- convError :: TypeError -> TCM ()
- compareTerm :: Comparison -> Type -> Term -> Term -> TCM ()
- unifyPointers :: t -> t1 -> t2 -> t3 -> t3
- compareTerm' :: Comparison -> Type -> Term -> Term -> TCM ()
- compareTel :: Type -> Type -> Comparison -> Telescope -> Telescope -> TCM ()
- compareAtom :: Comparison -> Type -> Term -> Term -> TCM ()
- compareRelevance :: Comparison -> Relevance -> Relevance -> Bool
- compareElims :: [Polarity] -> Type -> Term -> [Elim] -> [Elim] -> TCM ()
- compareIrrelevant :: Type -> Term -> Term -> TCM ()
- compareWithPol :: Polarity -> (Comparison -> a -> a -> TCM ()) -> a -> a -> TCM ()
- compareArgs :: [Polarity] -> Type -> Term -> Args -> Args -> TCM ()
- compareType :: Comparison -> Type -> Type -> TCM ()
- leqType :: Type -> Type -> TCM ()
- coerce :: Term -> Type -> Type -> TCM Term
- 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)

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

convError :: TypeError -> TCM ()

Ignore errors in irrelevant context.

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

Type directed equality on values.

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

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

compareRelevance :: Comparison -> Relevance -> Relevance -> Bool

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

Type-directed equality on eliminator spines

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

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

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

Type-directed equality on argument lists

# Types

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

Equality on Types

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

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

`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

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.