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.
module Agda.TypeChecking.
Pretty No documentation available.
-
Agda Agda.TypeChecking.Pretty No documentation available.
PrettyContext :: Context -> PrettyContextAgda Agda.TypeChecking.Pretty No documentation available.
-
Agda Agda.TypeChecking.Pretty No documentation available.
-
Agda Agda.TypeChecking.Pretty Pretty-print something paired with a (printable) node. | This intermediate typeclass exists to avoid UndecidableInstances.
module Agda.TypeChecking.
Primitive Primitive functions, such as addition on builtin integers.
-
Agda Agda.TypeChecking.Primitive No documentation available.
class PrimType a =>
PrimTerm aAgda Agda.TypeChecking.Primitive No documentation available.
-
Agda Agda.TypeChecking.Primitive No documentation available.
module Agda.TypeChecking.
ProjectionLike Dropping initial arguments (`parameters') from a function which can be easily reconstructed from its principal argument. A function which has such parameters is called ``projection-like''. The motivation for this optimization comes from the use of nested records. First, let us look why proper projections need not store the parameters: The type of a projection f is of the form f : Γ → R Γ → C where R is the record type and C is the type of the field f. Given a projection application p pars u we know that the type of the principal argument u is u : R pars thus, the parameters pars are redundant in the projection application if we can always infer the type of u. For projections, this is case, because the principal argument u must be neutral; otherwise, if it was a record value, we would have a redex, yet Agda maintains a β-normal form. The situation for projections can be generalized to ``projection-like'' functions f. Conditions:
- The type of f is of the form f : Γ → D Γ → ... for some type constructor D which can never reduce.
- For every reduced welltyped application f pars u ..., the type of u is inferable.
- This analysis could be dualized to ``constructor-like'' functions whose parameters are reconstructable from the target type. But such functions would need to be fully applied.
- A more general analysis of which arguments are reconstructible can be found inJason C. Reed, Redundancy elimination for LF LFTMP 2004.