| 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 -> [(Int, (Term, Term))] -> 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 telViewPathBoundaryP'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 -> [(Int, (Term, Term))] -> 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
| IApplyVars p => IApplyVars (NamedArg p) Source # | |
Defined in Agda.TypeChecking.Telescope.Path Methods iApplyVars :: NamedArg p -> [Int] Source # | |
| DeBruijn a => IApplyVars (Pattern' a) Source # | |
Defined in Agda.TypeChecking.Telescope.Path Methods iApplyVars :: Pattern' a -> [Int] Source # | |
| IApplyVars p => IApplyVars [p] Source # | |
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.