Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Telescope.Path

Synopsis

- telePiPath :: (Abs Type -> Abs Type) -> Telescope -> Type -> Boundary -> TCM Type
- iApplyVars :: DeBruijn a => [NamedArg (Pattern' a)] -> [Int]

# Documentation

telePiPath :: (Abs Type -> Abs Type) -> Telescope -> Type -> Boundary -> TCM Type Source #

In an ambient context Γ, `telePiPath f Δ t bs` builds a type that can be `telViewPathBoundaryP'ed` into (TelV Δ t, bs'). Γ.Δ ⊢ t bs = [(i,u_i)] Δ = Δ0,(i : I),Δ1 ∀ b ∈ {0,1}. Γ.Δ0 | u_i .b : (telePiPath f Δ1 t bs)(i = b) Γ ⊢ telePiPath f Δ t bs

iApplyVars :: DeBruijn a => [NamedArg (Pattern' a)] -> [Int] Source #