HORIZON HASKELLDocslts/ghc-9.14.x3e2d5682026-10-11Search names, modules, packages, or :: a typeCtrl K

GHC 9.14.1 · lts/ghc-9.14.x · 3e2d568 · 2026-10-11

ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Substitute

This module contains the definition of hereditary substitution and application operating on internal syntax which is in β-normal form (β including projection reductions).

Further, it contains auxiliary functions which rely on substitution but not on reduction.

  • 5 types
  • 1 class
  • 56 values
  • PackageAgda-2.8.0.2
  • Exports64
  • LanguageHaskell2010
  • LicenceMIT
  • SourceSubstitute.hs
valuecompiledClauseBody :: Clause -> Maybe Term
#

In compiled clauses, the variables in the clause body are relative to the pattern variables (including dot patterns) instead of the clause telescope.

valuedefApp :: QName -> Elims -> Elims -> Term
#

defApp f us vs applies Def f us to further arguments vs, eliminating top projection redexes. If us is not empty, we cannot have a projection redex, since the record argument is the first one.

valuefunSort' :: Sort -> Sort -> Either Blocker Sort
#

Compute the sort of a function type from the sorts of its domain and codomain.

This function should only be called on reduced sorts, since the LevelUniv rules should only apply when the sort does not reduce to Set.

valuepiApply :: Type -> Args -> Type
#
(x:A)->B(x) piApply [u] = B(u)

Precondition: The type must contain the right number of pis without having to perform any reduction.

piApply is potentially unsafe, the monadic piApplyM is preferable.

valuepiSort' :: Dom Term -> Sort -> Abs Sort -> Either Blocker Sort
#

Compute the sort of a pi type from the sorts of its domain and codomain. This function should only be called on reduced sorts, since the LevelUniv rules should only apply when the sort doesn't reduce to Set

valuetelView' :: Type -> TelView
#

Takes off all exposed function domains from the given type. This means that it does not reduce to expose Pi-types.

valuetelView'UpTo :: Int -> Type -> TelView
#

telView'UpTo n t takes off the first n exposed function types of t. Takes off all (exposed ones) if n < 0.

valuetelePiVisible :: Telescope -> Type -> Type
#

Only abstract the visible components of the telescope, and all that bind variables. Everything will be an Abs! Caution: quadratic time!

valueunivSort' :: Sort -> Either Blocker Sort
#

univSort' univInf s gets the next higher sort of s, if it is known (i.e. it is not just UnivSort s).

Precondition: s is reduced

module Agda.TypeChecking.Substitute.Class

module Agda.TypeChecking.Substitute.DeBruijn

datadata Substitution' a
#

Substitutions.

Constructors

  • IdS

    Identity substitution. Γ ⊢ IdS : Γ

  • EmptyS Impossible

    Empty substitution, lifts from the empty context. First argument is IMPOSSIBLE. Apply this to closed terms you want to use in a non-empty context. Γ ⊢ EmptyS : ()

  • a :# Substitution' ainfixr 4

    Substitution extension, `cons'. Γ ⊢ u : Aρ Γ ⊢ ρ : Δ ---------------------- Γ ⊢ u :# ρ : Δ, A

  • Strengthen Impossible !Int (Substitution' a)

    Strengthening substitution. First argument is IMPOSSIBLE. In 'Strengthen err n ρ the number n must be non-negative. This substitution should only be applied to values t for which none of the variables 0 up to n - 1 are free in t[ρ], and in that case n is subtracted from all free de Bruijn indices in t[ρ]. Γ ⊢ ρ : Δ |Θ| = n --------------------------- Γ ⊢ Strengthen n ρ : Δ, Θ @

  • Wk !Int (Substitution' a)

    Weakening substitution, lifts to an extended context. Γ ⊢ ρ : Δ ------------------- Γ, Ψ ⊢ Wk |Ψ| ρ : Δ

  • Lift !Int (Substitution' a)

    Lifting substitution. Use this to go under a binder. Lift 1 ρ == var 0 :# Wk 1 ρ. Γ ⊢ ρ : Δ ------------------------- Γ, Ψρ ⊢ Lift |Ψ| ρ : Δ, Ψ

Instances19Eq, Functor, Ord, Foldable, Traversable, KillRange, …

Orphan instances

130 instances