Safe Haskell | Safe-Infered |
---|
- 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
nextPolarity :: [Polarity] -> (Polarity, [Polarity])Source
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.
compareTerm :: Comparison -> Type -> Term -> Term -> TCM ()Source
Type directed equality on values.
compareTerm' :: Comparison -> Type -> Term -> Term -> TCM ()Source
compareTel :: Type -> Type -> Comparison -> Telescope -> Telescope -> TCM ()Source
compareTel t1 t2 cmp tel1 tel1
checks whether pointwise tel1
and complains that cmp
tel2t2
failed if not.
cmp
t1
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
compareArgs :: [Polarity] -> Type -> Term -> Args -> Args -> TCM ()Source
Type-directed equality on argument lists
compareType :: Comparison -> Type -> Type -> TCM ()Source
Equality on Types
Sorts
compareSort :: Comparison -> Sort -> Sort -> TCM ()Source