Hoogle Search
Within LTS Haskell 24.52 (ghc-9.10.3)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
PureConversionT :: ExceptT TCErr (StateT FreshThings m) a -> PureConversionT (m :: Type -> Type) aAgda Agda.TypeChecking.Conversion.Pure No documentation available.
-
Agda Agda.TypeChecking.DiscrimTree.Types Dependent function types. The domain will be represented accurately, for the case of a genuine dependent function type, the codomain will be a dummy.
module Agda.TypeChecking.Free.
Precompute Precompute free variables in a term (and store in ArgInfo).
-
Agda Agda.TypeChecking.Free.Precompute No documentation available.
ProjVar :: ProjectedVar -> InvertExceptAgda Agda.TypeChecking.MetaVars Try to eta-expand var to remove projs.
-
Agda Agda.TypeChecking.MetaVars.Occurs No documentation available.
PrunedEverything :: PruneResultAgda Agda.TypeChecking.MetaVars.Occurs all prescribed kills where performed
-
Agda Agda.TypeChecking.MetaVars.Occurs there is no possible kill (because of type dep.)
PrunedSomething :: PruneResultAgda Agda.TypeChecking.MetaVars.Occurs managed to kill some args in the list
PBoundVar :: Int -> PElims -> NLPatAgda Agda.TypeChecking.Monad.Base Matches x es where x is a lambda-bound variable