Hoogle Search
Within LTS Haskell 24.18 (ghc-9.10.3)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
getVarsToBind :: ScopeM LocalVarsAgda Agda.Syntax.Scope.Monad No documentation available.
intersectVars :: Elims -> Elims -> Maybe [Bool]Agda Agda.TypeChecking.Conversion 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.
-
Agda Agda.TypeChecking.Coverage.Match For each variable in the patterns of a split clause, we remember the de Bruijn-index and the literals excluded by previous matches.
SplitPatVar :: PatVarName -> Int -> [Literal] -> SplitPatVarAgda Agda.TypeChecking.Coverage.Match No documentation available.
splitPatVarIndex :: SplitPatVar -> IntAgda Agda.TypeChecking.Coverage.Match No documentation available.
splitPatVarName :: SplitPatVar -> PatVarNameAgda Agda.TypeChecking.Coverage.Match No documentation available.
allRelevantVars :: Free t => t -> VarSetAgda Agda.TypeChecking.Free Collect all relevant free variables, excluding the "unused" ones.
allRelevantVarsIgnoring :: Free t => IgnoreSorts -> t -> VarSetAgda Agda.TypeChecking.Free Collect all relevant free variables, possibly ignoring sorts.
SortOfSplitVarError :: Maybe Blocker -> Doc -> TypeErrorAgda Agda.TypeChecking.Monad.Base the meta is what we might be blocked on.
UnifyIndicesNotVars :: Telescope -> Type -> Term -> Term -> Args -> UnificationFailureAgda Agda.TypeChecking.Monad.Base Failed to apply injectivity to constructor of indexed datatype