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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Telescope.Path

Synopsis

- telePiPath :: (Abs Type -> Abs Type) -> ([Arg ArgName] -> Term -> Term) -> Telescope -> Type -> Boundary -> TCM Type
- telePiPath_ :: Telescope -> Type -> Boundary -> TCM Type
- arityPiPath :: Type -> TCM Int
- class IApplyVars p where
  - iApplyVars :: p -> [Int]
- isInterval :: (MonadTCM m, MonadReduce m) => Type -> m Bool

# Documentation

telePiPath :: (Abs Type -> Abs Type) -> ([Arg ArgName] -> Term -> Term) -> Telescope -> Type -> Boundary -> TCM Type Source #

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

telePiPath_ :: Telescope -> Type -> Boundary -> TCM Type Source #

`telePiPath_ Δ t [(i,u)]` Δ ⊢ t i ∈ Δ Δ ⊢ u_b : t for b ∈ {0,1}

arityPiPath :: Type -> TCM Int Source #

arity of the type, including both Pi and Path. Does not reduce the type.

class IApplyVars p where Source #

Collect the interval copattern variables as list of de Bruijn indices.

Methods

iApplyVars :: p -> [Int] Source #

#### Instances

Instances details

IApplyVars p => IApplyVars (NamedArg p) Source # |
Instance details Defined in Agda.TypeChecking.Telescope.Path Methods iApplyVars :: NamedArg p -> [Int] Source #
DeBruijn a => IApplyVars (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Telescope.Path Methods iApplyVars :: Pattern' a -> [Int] Source #
IApplyVars p => IApplyVars [p] Source # |
Instance details Defined in Agda.TypeChecking.Telescope.Path Methods iApplyVars :: [p] -> [Int] Source #

isInterval :: (MonadTCM m, MonadReduce m) => Type -> m Bool Source #

Check whether a type is the built-in interval type.