Agda- A dependently typed functional programming language and proof assistant

Safe HaskellSafe-Infered





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.

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

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

Type-directed equality on argument lists

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

Equality on Types


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.