Agda.TypeChecking.Substitute
- class Apply t where
- piApply :: Type -> Args -> Type
- class Abstract t where
- abstractArgs :: Abstract a => Args -> a -> a
- type Substitution = [Term]
- class Subst t where
- substs :: Substitution -> t -> t
- substUnder :: Nat -> Term -> t -> t
- idSub :: Telescope -> Substitution
- subst :: Subst t => Term -> t -> t
- class Raise t where
- raise :: Raise t => Nat -> t -> t
- rename :: Raise t => (Nat -> Nat) -> t -> t
- data TelV a = TelV (Tele (Arg a)) a
- type TelView = TelV Type
- telFromList :: [Arg (String, Type)] -> Telescope
- telToList :: Telescope -> [Arg (String, Type)]
- telView' :: Type -> TelView
- telePi :: Telescope -> Type -> Type
- telePi_ :: Telescope -> Type -> Type
- teleLam :: Telescope -> Term -> Term
- dLub :: Sort -> Abs Sort -> Sort
- absApp :: Subst t => Abs t -> Term -> t
- absBody :: Raise t => Abs t -> t
- mkAbs :: (Raise a, Free a) => String -> a -> Abs a
- reAbs :: (Raise a, Free a) => Abs a -> Abs a
- sLub :: Sort -> Sort -> Sort
- lvlView :: Term -> Level
- levelMax :: [PlusLevel] -> Level
- sortTm :: Sort -> Term
- levelSort :: Level -> Sort
- levelTm :: Level -> Term
Documentation
Apply something to a bunch of arguments. Preserves blocking tags (application can never resolve blocking).
Instances
| Apply Permutation | |
| Apply ClauseBody | |
| Apply Clause | |
| Apply Sort | |
| Apply Type | |
| Apply Term | |
| Apply CompiledClauses | |
| Apply FunctionInverse | |
| Apply PrimFun | |
| Apply Defn | |
| Apply Definition | |
| Apply DisplayTerm | |
| Apply t => Apply [t] | |
| Apply t => Apply (Maybe t) | |
| Subst a => Apply (Tele a) | |
| Apply t => Apply (Blocked t) | |
| Apply a => Apply (Case a) | |
| (Apply a, Apply b) => Apply (a, b) | |
| Apply v => Apply (Map k v) | |
| (Apply a, Apply b, Apply c) => Apply (a, b, c) |
piApply :: Type -> Args -> TypeSource
The type must contain the right number of pis without have to perform any reduction.
(abstract args v) args --> v[args].
Instances
| Abstract Permutation | |
| Abstract ClauseBody | |
| Abstract Clause | |
| Abstract Telescope | |
| Abstract Sort | |
| Abstract Type | |
| Abstract Term | |
| Abstract CompiledClauses | |
| Abstract FunctionInverse | |
| Abstract PrimFun | |
| Abstract Defn | |
| Abstract Definition | |
| Abstract t => Abstract [t] | |
| Abstract t => Abstract (Maybe t) | |
| Abstract a => Abstract (Case a) | |
| Abstract v => Abstract (Map k v) |
abstractArgs :: Abstract a => Args -> a -> aSource
type Substitution = [Term]Source
Substitutions.
Substitute a term for the nth free variable.
Instances
| Subst Pattern | |
| Subst ClauseBody | |
| Subst LevelAtom | |
| Subst PlusLevel | |
| Subst Level | |
| Subst Sort | |
| Subst Type | |
| Subst Term | |
| Subst DisplayTerm | |
| Subst Equality | |
| Subst AsBinding | |
| Subst DotPatternInst | |
| Subst a => Subst [a] | |
| Subst a => Subst (Maybe a) | |
| Subst a => Subst (Arg a) | |
| Subst a => Subst (Abs a) | |
| Subst a => Subst (Tele a) | |
| Subst t => Subst (Blocked t) | |
| Subst a => Subst (HomHet a) | |
| (Subst a, Subst b) => Subst (a, b) |
idSub :: Telescope -> SubstitutionSource
Add k to index of each open variable in x.
Instances
| Raise () | |
| Raise Pattern | |
| Raise ClauseBody | |
| Raise LevelAtom | |
| Raise PlusLevel | |
| Raise Level | |
| Raise Sort | |
| Raise Elim | |
| Raise Type | |
| Raise Term | |
| Raise DisplayTerm | |
| Raise DisplayForm | |
| Raise Constraint | |
| Raise AsBinding | |
| Raise t => Raise [t] | |
| Raise t => Raise (Maybe t) | |
| Raise t => Raise (Arg t) | |
| Raise t => Raise (Abs t) | |
| Raise a => Raise (Tele a) | |
| Raise t => Raise (Blocked t) | |
| Raise (Problem' p) | |
| Raise a => Raise (HomHet a) | |
| (Raise a, Raise b) => Raise (a, b) | |
| Raise v => Raise (Map k v) |