Safe Haskell | None |
---|
Agda.TypeChecking.Conversion
- 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
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.
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
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 ()
equalLevel :: Level -> Level -> TCM ()