Safe Haskell | None |
---|
- class Apply t where
- piApply :: Type -> Args -> Type
- class Abstract t where
- telVars :: Telescope -> [Arg Pattern]
- abstractArgs :: Abstract a => Args -> a -> a
- data Substitution
- = IdS
- | EmptyS
- | Wk !Int Substitution
- | Term :# Substitution
- | Lift !Int Substitution
- idS :: Substitution
- wkS :: Int -> Substitution -> Substitution
- raiseS :: Int -> Substitution
- singletonS :: Term -> Substitution
- liftS :: Int -> Substitution -> Substitution
- dropS :: Int -> Substitution -> Substitution
- composeS :: Substitution -> Substitution -> Substitution
- splitS :: Int -> Substitution -> (Substitution, Substitution)
- (++#) :: [Term] -> Substitution -> Substitution
- parallelS :: [Term] -> Substitution
- lookupS :: Substitution -> Nat -> Term
- class Subst t where
- applySubst :: Substitution -> t -> t
- raise :: Subst t => Nat -> t -> t
- raiseFrom :: Subst t => Nat -> Nat -> t -> t
- subst :: Subst t => Term -> t -> t
- substUnder :: Subst t => Nat -> Term -> t -> t
- data TelV a = TelV (Tele (Dom a)) a
- type TelView = TelV Type
- telFromList :: [Dom (String, Type)] -> Telescope
- telToList :: Telescope -> [Dom (String, Type)]
- telView' :: Type -> TelView
- mkPi :: Dom (String, Type) -> Type -> Type
- 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 :: Subst t => Abs t -> t
- mkAbs :: (Subst a, Free a) => String -> a -> Abs a
- reAbs :: (Subst a, Free a) => Abs a -> Abs a
- underAbs :: Subst a => (a -> b -> b) -> a -> Abs b -> Abs b
- underLambdas :: Subst a => Int -> (a -> Term -> Term) -> a -> Term -> Term
- sLub :: Sort -> Sort -> Sort
- lvlView :: Term -> Level
- levelMax :: [PlusLevel] -> Level
- sortTm :: Sort -> Term
- levelSort :: Level -> Sort
- levelTm :: Level -> Term
- unLevelAtom :: LevelAtom -> Term
Documentation
Apply something to a bunch of arguments. Preserves blocking tags (application can never resolve blocking).
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 [Occurrence] | |
Apply [Polarity] | |
Apply t => Apply (Maybe t) | |
Apply a => Apply (Ptr a) | |
Apply t => Apply (Blocked t) | |
Subst a => Apply (Tele a) | |
Apply a => Apply (Case a) | |
Apply a => Apply (WithArity 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]
.
Abstract Permutation | |
Abstract ClauseBody | |
Abstract Clause | |
Abstract Sort | |
Abstract Telescope | |
Abstract Type | |
Abstract Term | |
Abstract CompiledClauses | |
Abstract FunctionInverse | |
Abstract PrimFun | |
Abstract Defn | |
Abstract Definition | |
Abstract t => Abstract [t] | |
Abstract [Occurrence] | |
Abstract [Polarity] | |
Abstract t => Abstract (Maybe t) | |
Abstract a => Abstract (Case a) | |
Abstract a => Abstract (WithArity a) | |
Abstract v => Abstract (Map k v) |
abstractArgs :: Abstract a => Args -> a -> aSource
data Substitution Source
Substitutions.
wkS :: Int -> Substitution -> SubstitutionSource
raiseS :: Int -> SubstitutionSource
singletonS :: Term -> SubstitutionSource
liftS :: Int -> Substitution -> SubstitutionSource
dropS :: Int -> Substitution -> SubstitutionSource
composeS :: Substitution -> Substitution -> SubstitutionSource
applySubst (ρ composeS
σ) v == applySubst ρ (applySubst σ v)
splitS :: Int -> Substitution -> (Substitution, Substitution)Source
(++#) :: [Term] -> Substitution -> SubstitutionSource
parallelS :: [Term] -> SubstitutionSource
lookupS :: Substitution -> Nat -> TermSource
Apply a substitution.
applySubst :: Substitution -> t -> tSource
Subst () | |
Subst Pattern | |
Subst ClauseBody | |
Subst LevelAtom | |
Subst PlusLevel | |
Subst Level | |
Subst Sort | |
Subst Type | |
Subst Elim | |
Subst Term | |
Subst DisplayTerm | |
Subst DisplayForm | |
Subst Constraint | |
Subst Substitution | |
Subst AsBinding | |
Subst DotPatternInst | |
Subst ProblemRest | |
Subst Equality | |
Subst a => Subst [a] | |
Subst a => Subst (Maybe a) | |
Subst a => Subst (Ptr a) | |
Subst a => Subst (Arg a) | |
Subst a => Subst (Dom a) | |
Subst t => Subst (Blocked t) | |
Subst a => Subst (Tele a) | |
Subst a => Subst (Abs a) | |
Subst (Problem' p) | |
Subst a => Subst (HomHet a) | |
(Subst a, Subst b) => Subst (a, b) |
substUnder :: Subst t => Nat -> Term -> t -> tSource
dLub :: Sort -> Abs Sort -> SortSource
Dependent least upper bound, to assign a level to expressions
like forall i -> Set i
.
dLub s1 i.s2 = omega
if i
appears in the rigid variables of s2
.
underAbs :: Subst a => (a -> b -> b) -> a -> Abs b -> Abs bSource
underAbs k a b
applies k
to a
and the content of
abstraction b
and puts the abstraction back.
a
is raised if abstraction was proper such that
at point of application of k
and the content of b
are at the same context.
Precondition: a
and b
are at the same context at call time.
unLevelAtom :: LevelAtom -> TermSource