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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Substitute

Contents

- Orphan instances

Description

This module contains the definition of hereditary substitution and application operating on internal syntax which is in β-normal form (β including projection reductions).

Further, it contains auxiliary functions which rely on substitution but not on reduction.

Synopsis

- class TeleNoAbs a where
  - teleNoAbs :: a -> Term -> Term
- data TelV a = TelV {
  - theTel :: Tele (Dom a)
  - theCore :: a
  }
- type TelView = TelV Type
- canProject :: QName -> Term -> Maybe (Arg Term)
- conApp :: ConHead -> ConInfo -> Elims -> Elims -> Term
- defApp :: QName -> Elims -> Elims -> Term
- argToDontCare :: Arg Term -> Term
- relToDontCare :: LensRelevance a => a -> Term -> Term
- piApply :: Type -> Args -> Type
- telVars :: Int -> Telescope -> [Arg DeBruijnPattern]
- namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern]
- abstractArgs :: Abstract a => Args -> a -> a
- renaming :: forall a. DeBruijn a => Empty -> Permutation -> Substitution' a
- renamingR :: DeBruijn a => Permutation -> Substitution' a
- renameP :: Subst t a => Empty -> Permutation -> a -> a
- applyNLPatSubst :: Subst Term a => Substitution' NLPat -> a -> a
- fromPatternSubstitution :: PatternSubstitution -> Substitution
- applyPatSubst :: Subst Term a => PatternSubstitution -> a -> a
- usePatOrigin :: PatOrigin -> Pattern' a -> Pattern' a
- projDropParsApply :: Projection -> ProjOrigin -> Args -> Term
- telView' :: Type -> TelView
- telView'UpTo :: Int -> Type -> TelView
- bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a
- bindsToTel :: [Name] -> Dom Type -> ListTel
- namedBindsToTel :: [NamedArg Name] -> Type -> Telescope
- domFromNamedArgName :: NamedArg Name -> Dom ()
- mkPi :: Dom (ArgName, Type) -> Type -> Type
- mkLam :: Arg ArgName -> Term -> Term
- telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type
- telePi :: Telescope -> Type -> Type
- telePi_ :: Telescope -> Type -> Type
- teleLam :: Telescope -> Term -> Term
- typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type]
- compiledClauseBody :: Clause -> Maybe Term
- univSort' :: Maybe Sort -> Sort -> Maybe Sort
- univSort :: Maybe Sort -> Sort -> Sort
- univInf :: HasOptions m => m (Maybe Sort)
- funSort' :: Sort -> Sort -> Maybe Sort
- funSort :: Sort -> Sort -> Sort
- piSort' :: Sort -> Abs Sort -> Maybe Sort
- piSort :: Sort -> Abs Sort -> Sort
- levelMax :: [PlusLevel] -> Level
- levelTm :: Level -> Term
- unLevelAtom :: LevelAtom -> Term
- levelSucView :: Level -> Maybe Level
- module Agda.TypeChecking.Substitute.Class
- module Agda.TypeChecking.Substitute.DeBruijn
- data Substitution' a
  - = IdS
  - | EmptyS Empty
  - | a :# (Substitution' a)
  - | Strengthen Empty (Substitution' a)
  - | Wk !Int (Substitution' a)
  - | Lift !Int (Substitution' a)
- type Substitution = Substitution' Term

# Documentation

class TeleNoAbs a where Source #

Performs void (`noAbs`) abstraction over telescope.

Methods

teleNoAbs :: a -> Term -> Term Source #

Instances

TeleNoAbs ListTel Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods teleNoAbs :: ListTel -> Term -> Term Source #
TeleNoAbs Telescope Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods teleNoAbs :: Telescope -> Term -> Term Source #

data TelV a Source #

Constructors

TelV |

Fields

- theTel :: Tele (Dom a)
- theCore :: a

Instances

Functor TelV Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods fmap :: (a -> b) -> TelV a -> TelV b Source # (<$) :: a -> TelV b -> TelV a Source #
(Subst t a, Eq a) => Eq (TelV a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: TelV a -> TelV a -> Bool Source # (/=) :: TelV a -> TelV a -> Bool Source #
(Subst t a, Ord a) => Ord (TelV a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: TelV a -> TelV a -> Ordering Source # (<) :: TelV a -> TelV a -> Bool Source # (<=) :: TelV a -> TelV a -> Bool Source # (>) :: TelV a -> TelV a -> Bool Source # (>=) :: TelV a -> TelV a -> Bool Source # max :: TelV a -> TelV a -> TelV a Source # min :: TelV a -> TelV a -> TelV a Source #
Show a => Show (TelV a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods showsPrec :: Int -> TelV a -> ShowS Source # show :: TelV a -> String Source # showList :: [TelV a] -> ShowS Source #

type TelView = TelV Type Source #

canProject :: QName -> Term -> Maybe (Arg Term) Source #

If $v$ is a record value, `canProject f v` returns its field `f`.

conApp :: ConHead -> ConInfo -> Elims -> Elims -> Term Source #

Eliminate a constructed term.

defApp :: QName -> Elims -> Elims -> Term Source #

`defApp f us vs` applies `Def f us` to further arguments `vs`, eliminating top projection redexes. If `us` is not empty, we cannot have a projection redex, since the record argument is the first one.

argToDontCare :: Arg Term -> Term Source #

relToDontCare :: LensRelevance a => a -> Term -> Term Source #

piApply :: Type -> Args -> Type Source #

    (x:A)->B(x) piApply [u] = B(u)

Precondition: The type must contain the right number of pis without having to perform any reduction.

`piApply` is potentially unsafe, the monadic `piApplyM` is preferable.

telVars :: Int -> Telescope -> [Arg DeBruijnPattern] Source #

namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern] Source #

abstractArgs :: Abstract a => Args -> a -> a Source #

renaming :: forall a. DeBruijn a => Empty -> Permutation -> Substitution' a Source #

If `permute π : [a]Γ -> [a]Δ`, then `applySubst (renaming _ π) : Term Γ -> Term Δ`

renamingR :: DeBruijn a => Permutation -> Substitution' a Source #

If `permute π : [a]Γ -> [a]Δ`, then `applySubst (renamingR π) : Term Δ -> Term Γ`

renameP :: Subst t a => Empty -> Permutation -> a -> a Source #

The permutation should permute the corresponding context. (right-to-left list)

applyNLPatSubst :: Subst Term a => Substitution' NLPat -> a -> a Source #

fromPatternSubstitution :: PatternSubstitution -> Substitution Source #

applyPatSubst :: Subst Term a => PatternSubstitution -> a -> a Source #

usePatOrigin :: PatOrigin -> Pattern' a -> Pattern' a Source #

projDropParsApply :: Projection -> ProjOrigin -> Args -> Term Source #

    projDropParsApply proj o args = projDropPars proj o `apply' args

This function is an optimization, saving us from construction lambdas we immediately remove through application.

telView' :: Type -> TelView Source #

Takes off all exposed function domains from the given type. This means that it does not reduce to expose `Pi`-types.

telView'UpTo :: Int -> Type -> TelView Source #

`telView'UpTo n t` takes off the first `n` exposed function types of `t`. Takes off all (exposed ones) if `n < 0`.

bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a Source #

Turn a typed binding `(x1 .. xn : A)` into a telescope.

bindsToTel :: [Name] -> Dom Type -> ListTel Source #

namedBindsToTel :: [NamedArg Name] -> Type -> Telescope Source #

Turn a typed binding `(x1 .. xn : A)` into a telescope.

domFromNamedArgName :: NamedArg Name -> Dom () Source #

mkPi :: Dom (ArgName, Type) -> Type -> Type Source #

    mkPi dom t = telePi (telFromList [dom]) t

mkLam :: Arg ArgName -> Term -> Term Source #

telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type Source #

telePi :: Telescope -> Type -> Type Source #

Uses free variable analysis to introduce `NoAbs` bindings.

telePi_ :: Telescope -> Type -> Type Source #

Everything will be an `Abs`.

teleLam :: Telescope -> Term -> Term Source #

Abstract over a telescope in a term, producing lambdas. Dumb abstraction: Always produces `Abs`, never `NoAbs`.

The implementation is sound because `Telescope` does not use `NoAbs`.

typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type] Source #

Given arguments `vs : tel` (vector typing), extract their individual types. Returns `Nothing` is `tel` is not long enough.

compiledClauseBody :: Clause -> Maybe Term Source #

In compiled clauses, the variables in the clause body are relative to the pattern variables (including dot patterns) instead of the clause telescope.

univSort' :: Maybe Sort -> Sort -> Maybe Sort Source #

Get the next higher sort.

univSort :: Maybe Sort -> Sort -> Sort Source #

univInf :: HasOptions m => m (Maybe Sort) Source #

funSort' :: Sort -> Sort -> Maybe Sort Source #

Compute the sort of a function type from the sorts of its domain and codomain.

funSort :: Sort -> Sort -> Sort Source #

piSort' :: Sort -> Abs Sort -> Maybe Sort Source #

Compute the sort of a pi type from the sorts of its domain and codomain.

piSort :: Sort -> Abs Sort -> Sort Source #

levelMax :: [PlusLevel] -> Level Source #

levelTm :: Level -> Term Source #

unLevelAtom :: LevelAtom -> Term Source #

levelSucView :: Level -> Maybe Level Source #

module Agda.TypeChecking.Substitute.Class

module Agda.TypeChecking.Substitute.DeBruijn

data Substitution' a Source #

Substitutions.

Constructors

IdS | Identity substitution. `Γ ⊢ IdS : Γ`
EmptyS Empty | Empty substitution, lifts from the empty context. First argument is `(throwImpossible (Impossible "srcfullAgdaSyntaxInternal.hs" 614))`. Apply this to closed terms you want to use in a non-empty context. `Γ ⊢ EmptyS : ()`
a :# (Substitution' a) infixr 4 | Substitution extension, ``cons'`. `Γ ⊢ u : Aρ Γ ⊢ ρ : Δ ---------------------- Γ ⊢ u :# ρ : Δ, A`
Strengthen Empty (Substitution' a) | Strengthening substitution. First argument is `(throwImpossible (Impossible "srcfullAgdaSyntaxInternal.hs" 627))`. Apply this to a term which does not contain variable 0 to lower all de Bruijn indices by one. `Γ ⊢ ρ : Δ --------------------------- Γ ⊢ Strengthen ρ : Δ, A`
Wk !Int (Substitution' a) | Weakning substitution, lifts to an extended context. `Γ ⊢ ρ : Δ ------------------- Γ, Ψ ⊢ Wk |Ψ| ρ : Δ`
Lift !Int (Substitution' a) | Lifting substitution. Use this to go under a binder. `Lift 1 ρ == var 0 :# Wk 1 ρ`. `Γ ⊢ ρ : Δ ------------------------- Γ, Ψρ ⊢ Lift |Ψ| ρ : Δ, Ψ`

Instances

Functor Substitution' Source # |
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Substitution' a -> Substitution' b Source # (<$) :: a -> Substitution' b -> Substitution' a Source #
Foldable Substitution' Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => Substitution' m -> m Source #

foldMap :: Monoid m => (a -> m) -> Substitution' a -> m Source #

foldr :: (a -> b -> b) -> b -> Substitution' a -> b Source #

foldr' :: (a -> b -> b) -> b -> Substitution' a -> b Source #

foldl :: (b -> a -> b) -> b -> Substitution' a -> b Source #

foldl' :: (b -> a -> b) -> b -> Substitution' a -> b Source #

foldr1 :: (a -> a -> a) -> Substitution' a -> a Source #

foldl1 :: (a -> a -> a) -> Substitution' a -> a Source #

toList :: Substitution' a -> [a] Source #

null :: Substitution' a -> Bool Source #

length :: Substitution' a -> Int Source #

elem :: Eq a => a -> Substitution' a -> Bool Source #

maximum :: Ord a => Substitution' a -> a Source #

minimum :: Ord a => Substitution' a -> a Source #

sum :: Num a => Substitution' a -> a Source #

product :: Num a => Substitution' a -> a Source #

Traversable Substitution' Source # |
Instance details Defined in Agda.Syntax.Internal Methods traverse :: Applicative f => (a -> f b) -> Substitution' a -> f (Substitution' b) Source # sequenceA :: Applicative f => Substitution' (f a) -> f (Substitution' a) Source # mapM :: Monad m => (a -> m b) -> Substitution' a -> m (Substitution' b) Source # sequence :: Monad m => Substitution' (m a) -> m (Substitution' a) Source #
KillRange Substitution Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Substitution Source #
InstantiateFull Substitution Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Substitution -> ReduceM Substitution Source #
Subst a a => Subst a (Substitution' a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' a -> Substitution' a -> Substitution' a Source #
Eq (Substitution' Term) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Substitution' Term -> Substitution' Term -> Bool Source # (/=) :: Substitution' Term -> Substitution' Term -> Bool Source #
Data a => Data (Substitution' a) Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Substitution' a -> c (Substitution' a) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Substitution' a) Source #

toConstr :: Substitution' a -> Constr Source #

dataTypeOf :: Substitution' a -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Substitution' a)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Substitution' a)) Source #

gmapT :: (forall b. Data b => b -> b) -> Substitution' a -> Substitution' a Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Substitution' a -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Substitution' a -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Substitution' a -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Substitution' a -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Substitution' a -> m (Substitution' a) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Substitution' a -> m (Substitution' a) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Substitution' a -> m (Substitution' a) Source #

Ord (Substitution' Term) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Methods

compare :: Substitution' Term -> Substitution' Term -> Ordering Source #

(<) :: Substitution' Term -> Substitution' Term -> Bool Source #

(<=) :: Substitution' Term -> Substitution' Term -> Bool Source #

(>) :: Substitution' Term -> Substitution' Term -> Bool Source #

(>=) :: Substitution' Term -> Substitution' Term -> Bool Source #

max :: Substitution' Term -> Substitution' Term -> Substitution' Term Source #

min :: Substitution' Term -> Substitution' Term -> Substitution' Term Source #

Show a => Show (Substitution' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Substitution' a -> ShowS Source # show :: Substitution' a -> String Source # showList :: [Substitution' a] -> ShowS Source #
Null (Substitution' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods empty :: Substitution' a Source # null :: Substitution' a -> Bool Source #
Pretty a => Pretty (Substitution' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Substitution' a -> Doc Source # prettyPrec :: Int -> Substitution' a -> Doc Source # prettyList :: [Substitution' a] -> Doc Source #
TermSize a => TermSize (Substitution' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Substitution' a -> Int Source # tsize :: Substitution' a -> Sum Int Source #
EmbPrj a => EmbPrj (Substitution' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Substitution' a -> S Int32 Source # icod_ :: Substitution' a -> S Int32 Source # value :: Int32 -> R (Substitution' a) Source #
(Pretty a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Substitution' a -> TCM Doc Source #

type Substitution = Substitution' Term Source #

# Orphan instances

Eq NotBlocked Source # |
Instance details Methods (==) :: NotBlocked -> NotBlocked -> Bool Source # (/=) :: NotBlocked -> NotBlocked -> Bool Source #
Eq LevelAtom Source # |
Instance details Methods (==) :: LevelAtom -> LevelAtom -> Bool Source # (/=) :: LevelAtom -> LevelAtom -> Bool Source #
Eq PlusLevel Source # |
Instance details Methods (==) :: PlusLevel -> PlusLevel -> Bool Source # (/=) :: PlusLevel -> PlusLevel -> Bool Source #
Eq Level Source # |
Instance details Methods (==) :: Level -> Level -> Bool Source # (/=) :: Level -> Level -> Bool Source #
Eq Sort Source # |
Instance details Methods (==) :: Sort -> Sort -> Bool Source # (/=) :: Sort -> Sort -> Bool Source #
Eq Term Source # | Syntactic `Term` equality, ignores stuff below `DontCare` and sharing.
Instance details Methods (==) :: Term -> Term -> Bool Source # (/=) :: Term -> Term -> Bool Source #
Eq Candidate Source # |
Instance details Methods (==) :: Candidate -> Candidate -> Bool Source # (/=) :: Candidate -> Candidate -> Bool Source #
Eq Section Source # |
Instance details Methods (==) :: Section -> Section -> Bool Source # (/=) :: Section -> Section -> Bool Source #
Eq Constraint Source # |
Instance details Methods (==) :: Constraint -> Constraint -> Bool Source # (/=) :: Constraint -> Constraint -> Bool Source #
Ord LevelAtom Source # |
Instance details Methods compare :: LevelAtom -> LevelAtom -> Ordering Source # (<) :: LevelAtom -> LevelAtom -> Bool Source # (<=) :: LevelAtom -> LevelAtom -> Bool Source # (>) :: LevelAtom -> LevelAtom -> Bool Source # (>=) :: LevelAtom -> LevelAtom -> Bool Source # max :: LevelAtom -> LevelAtom -> LevelAtom Source # min :: LevelAtom -> LevelAtom -> LevelAtom Source #
Ord PlusLevel Source # |
Instance details Methods compare :: PlusLevel -> PlusLevel -> Ordering Source # (<) :: PlusLevel -> PlusLevel -> Bool Source # (<=) :: PlusLevel -> PlusLevel -> Bool Source # (>) :: PlusLevel -> PlusLevel -> Bool Source # (>=) :: PlusLevel -> PlusLevel -> Bool Source # max :: PlusLevel -> PlusLevel -> PlusLevel Source # min :: PlusLevel -> PlusLevel -> PlusLevel Source #
Ord Level Source # |
Instance details Methods compare :: Level -> Level -> Ordering Source # (<) :: Level -> Level -> Bool Source # (<=) :: Level -> Level -> Bool Source # (>) :: Level -> Level -> Bool Source # (>=) :: Level -> Level -> Bool Source # max :: Level -> Level -> Level Source # min :: Level -> Level -> Level Source #
Ord Sort Source # |
Instance details Methods compare :: Sort -> Sort -> Ordering Source # (<) :: Sort -> Sort -> Bool Source # (<=) :: Sort -> Sort -> Bool Source # (>) :: Sort -> Sort -> Bool Source # (>=) :: Sort -> Sort -> Bool Source # max :: Sort -> Sort -> Sort Source # min :: Sort -> Sort -> Sort Source #
Ord Term Source # |
Instance details Methods compare :: Term -> Term -> Ordering Source # (<) :: Term -> Term -> Bool Source # (<=) :: Term -> Term -> Bool Source # (>) :: Term -> Term -> Bool Source # (>=) :: Term -> Term -> Bool Source # max :: Term -> Term -> Term Source # min :: Term -> Term -> Term Source #
DeBruijn DeBruijnPattern Source # |
Instance details Methods deBruijnVar :: Int -> DeBruijnPattern Source # debruijnNamedVar :: String -> Int -> DeBruijnPattern Source # deBruijnView :: DeBruijnPattern -> Maybe Int Source #
DeBruijn NLPat Source # |
Instance details Methods deBruijnVar :: Int -> NLPat Source # debruijnNamedVar :: String -> Int -> NLPat Source # deBruijnView :: NLPat -> Maybe Int Source #
Abstract Permutation Source # |
Instance details Methods abstract :: Telescope -> Permutation -> Permutation Source #
Abstract Clause Source # |
Instance details Methods abstract :: Telescope -> Clause -> Clause Source #
Abstract Sort Source # |
Instance details Methods abstract :: Telescope -> Sort -> Sort Source #
Abstract Telescope Source # |
Instance details Methods abstract :: Telescope -> Telescope -> Telescope Source #
Abstract Type Source # |
Instance details Methods abstract :: Telescope -> Type -> Type Source #
Abstract Term Source # |
Instance details Methods abstract :: Telescope -> Term -> Term Source #
Abstract CompiledClauses Source # |
Instance details Methods abstract :: Telescope -> CompiledClauses -> CompiledClauses Source #
Abstract FunctionInverse Source # |
Instance details Methods abstract :: Telescope -> FunctionInverse -> FunctionInverse Source #
Abstract PrimFun Source # |
Instance details Methods abstract :: Telescope -> PrimFun -> PrimFun Source #
Abstract Defn Source # |
Instance details Methods abstract :: Telescope -> Defn -> Defn Source #
Abstract ProjLams Source # |
Instance details Methods abstract :: Telescope -> ProjLams -> ProjLams Source #
Abstract Projection Source # |
Instance details Methods abstract :: Telescope -> Projection -> Projection Source #
Abstract System Source # |
Instance details Methods abstract :: Telescope -> System -> System Source #
Abstract NumGeneralizableArgs Source # |
Instance details Methods abstract :: Telescope -> NumGeneralizableArgs -> NumGeneralizableArgs Source #
Abstract Definition Source # |
Instance details Methods abstract :: Telescope -> Definition -> Definition Source #
Abstract RewriteRule Source # | `tel ⊢ (Γ ⊢ lhs ↦ rhs : t)` becomes `tel, Γ ⊢ lhs ↦ rhs : t)` we do not need to change lhs, rhs, and t since they live in Γ. See 'Abstract Clause'.
Instance details Methods abstract :: Telescope -> RewriteRule -> RewriteRule Source #
Apply Permutation Source # |
Instance details Methods apply :: Permutation -> Args -> Permutation Source # applyE :: Permutation -> Elims -> Permutation Source #
Apply Clause Source # |
Instance details Methods apply :: Clause -> Args -> Clause Source # applyE :: Clause -> Elims -> Clause Source #
Apply Sort Source # |
Instance details Methods apply :: Sort -> Args -> Sort Source # applyE :: Sort -> Elims -> Sort Source #
Apply Term Source # |
Instance details Methods apply :: Term -> Args -> Term Source # applyE :: Term -> Elims -> Term Source #
Apply CompiledClauses Source # |
Instance details Methods apply :: CompiledClauses -> Args -> CompiledClauses Source # applyE :: CompiledClauses -> Elims -> CompiledClauses Source #
Apply FunctionInverse Source # |
Instance details Methods apply :: FunctionInverse -> Args -> FunctionInverse Source # applyE :: FunctionInverse -> Elims -> FunctionInverse Source #
Apply PrimFun Source # |
Instance details Methods apply :: PrimFun -> Args -> PrimFun Source # applyE :: PrimFun -> Elims -> PrimFun Source #
Apply Defn Source # |
Instance details Methods apply :: Defn -> Args -> Defn Source # applyE :: Defn -> Elims -> Defn Source #
Apply ProjLams Source # |
Instance details Methods apply :: ProjLams -> Args -> ProjLams Source # applyE :: ProjLams -> Elims -> ProjLams Source #
Apply Projection Source # |
Instance details Methods apply :: Projection -> Args -> Projection Source # applyE :: Projection -> Elims -> Projection Source #
Apply ExtLamInfo Source # |
Instance details Methods apply :: ExtLamInfo -> Args -> ExtLamInfo Source # applyE :: ExtLamInfo -> Elims -> ExtLamInfo Source #
Apply System Source # |
Instance details Methods apply :: System -> Args -> System Source # applyE :: System -> Elims -> System Source #
Apply NumGeneralizableArgs Source # |
Instance details Methods apply :: NumGeneralizableArgs -> Args -> NumGeneralizableArgs Source # applyE :: NumGeneralizableArgs -> Elims -> NumGeneralizableArgs Source #
Apply Definition Source # |
Instance details Methods apply :: Definition -> Args -> Definition Source # applyE :: Definition -> Elims -> Definition Source #
Apply RewriteRule Source # |
Instance details Methods apply :: RewriteRule -> Args -> RewriteRule Source # applyE :: RewriteRule -> Elims -> RewriteRule Source #
Apply DisplayTerm Source # |
Instance details Methods apply :: DisplayTerm -> Args -> DisplayTerm Source # applyE :: DisplayTerm -> Elims -> DisplayTerm Source #
Subst DeBruijnPattern DeBruijnPattern Source # |
Instance details Methods applySubst :: Substitution' DeBruijnPattern -> DeBruijnPattern -> DeBruijnPattern Source #
Subst Term () Source # |
Instance details Methods applySubst :: Substitution' Term -> () -> () Source #
Subst Term String Source # |
Instance details Methods applySubst :: Substitution' Term -> String -> String Source #
Subst Term Range Source # |
Instance details Methods applySubst :: Substitution' Term -> Range -> Range Source #
Subst Term Name Source # |
Instance details Methods applySubst :: Substitution' Term -> Name -> Name Source #
Subst Term EqualityView Source # |
Instance details Methods applySubst :: Substitution' Term -> EqualityView -> EqualityView Source #
Subst Term ConPatternInfo Source # |
Instance details Methods applySubst :: Substitution' Term -> ConPatternInfo -> ConPatternInfo Source #
Subst Term Pattern Source # |
Instance details Methods applySubst :: Substitution' Term -> Pattern -> Pattern Source #
Subst Term LevelAtom Source # |
Instance details Methods applySubst :: Substitution' Term -> LevelAtom -> LevelAtom Source #
Subst Term PlusLevel Source # |
Instance details Methods applySubst :: Substitution' Term -> PlusLevel -> PlusLevel Source #
Subst Term Level Source # |
Instance details Methods applySubst :: Substitution' Term -> Level -> Level Source #
Subst Term Sort Source # |
Instance details Methods applySubst :: Substitution' Term -> Sort -> Sort Source #
Subst Term Term Source # |
Instance details Methods applySubst :: Substitution' Term -> Term -> Term Source #
Subst Term ProblemEq Source # |
Instance details Methods applySubst :: Substitution' Term -> ProblemEq -> ProblemEq Source #
Subst Term Candidate Source # |
Instance details Methods applySubst :: Substitution' Term -> Candidate -> Candidate Source #
Subst Term DisplayTerm Source # |
Instance details Methods applySubst :: Substitution' Term -> DisplayTerm -> DisplayTerm Source #
Subst Term DisplayForm Source # |
Instance details Methods applySubst :: Substitution' Term -> DisplayForm -> DisplayForm Source #
Subst Term Constraint Source # |
Instance details Methods applySubst :: Substitution' Term -> Constraint -> Constraint Source #
Subst NLPat RewriteRule Source # |
Instance details Methods applySubst :: Substitution' NLPat -> RewriteRule -> RewriteRule Source #
Subst NLPat NLPType Source # |
Instance details Methods applySubst :: Substitution' NLPat -> NLPType -> NLPType Source #
Subst NLPat NLPat Source # |
Instance details Methods applySubst :: Substitution' NLPat -> NLPat -> NLPat Source #
Subst t a => Subst t [a] Source # |
Instance details Methods applySubst :: Substitution' t -> [a] -> [a] Source #
Subst t a => Subst t (Maybe a) Source # |
Instance details Methods applySubst :: Substitution' t -> Maybe a -> Maybe a Source #
Subst t a => Subst t (Dom a) Source # |
Instance details Methods applySubst :: Substitution' t -> Dom a -> Dom a Source #
Subst t a => Subst t (Arg a) Source # |
Instance details Methods applySubst :: Substitution' t -> Arg a -> Arg a Source #
Subst t a => Subst t (Abs a) Source # |
Instance details Methods applySubst :: Substitution' t -> Abs a -> Abs a Source #
Subst t a => Subst t (Elim' a) Source # |
Instance details Methods applySubst :: Substitution' t -> Elim' a -> Elim' a Source #
Subst t a => Subst t (Tele a) Source # |
Instance details Methods applySubst :: Substitution' t -> Tele a -> Tele a Source #
Subst t a => Subst t (Blocked a) Source # |
Instance details Methods applySubst :: Substitution' t -> Blocked a -> Blocked a Source #
Subst a a => Subst a (Substitution' a) Source # |
Instance details Methods applySubst :: Substitution' a -> Substitution' a -> Substitution' a Source #
Subst Term a => Subst Term (Type' a) Source # |
Instance details Methods applySubst :: Substitution' Term -> Type' a -> Type' a Source #
(Subst t a, Subst t b) => Subst t (a, b) Source # |
Instance details Methods applySubst :: Substitution' t -> (a, b) -> (a, b) Source #
(Ord k, Subst t a) => Subst t (Map k a) Source # |
Instance details Methods applySubst :: Substitution' t -> Map k a -> Map k a Source #
Subst t a => Subst t (Named name a) Source # |
Instance details Methods applySubst :: Substitution' t -> Named name a -> Named name a Source #
(Subst t a, Subst t b, Subst t c) => Subst t (a, b, c) Source # |
Instance details Methods applySubst :: Substitution' t -> (a, b, c) -> (a, b, c) Source #
(Subst t a, Subst t b, Subst t c, Subst t d) => Subst t (a, b, c, d) Source # |
Instance details Methods applySubst :: Substitution' t -> (a, b, c, d) -> (a, b, c, d) Source #
Eq (Substitution' Term) Source # |
Instance details Methods (==) :: Substitution' Term -> Substitution' Term -> Bool Source # (/=) :: Substitution' Term -> Substitution' Term -> Bool Source #
Eq a => Eq (Pattern' a) Source # |
Instance details Methods (==) :: Pattern' a -> Pattern' a -> Bool Source # (/=) :: Pattern' a -> Pattern' a -> Bool Source #
Eq t => Eq (Blocked t) Source # |
Instance details Methods (==) :: Blocked t -> Blocked t -> Bool Source # (/=) :: Blocked t -> Blocked t -> Bool Source #
(Subst t a, Eq a) => Eq (Tele a) Source # |
Instance details Methods (==) :: Tele a -> Tele a -> Bool Source # (/=) :: Tele a -> Tele a -> Bool Source #
Eq a => Eq (Type' a) Source # | Syntactic `Type` equality, ignores sort annotations.
Instance details Methods (==) :: Type' a -> Type' a -> Bool Source # (/=) :: Type' a -> Type' a -> Bool Source #
(Subst t a, Eq a) => Eq (Abs a) Source # | Equality of binders relies on weakening which is a special case of renaming which is a special case of substitution.
Instance details Methods (==) :: Abs a -> Abs a -> Bool Source # (/=) :: Abs a -> Abs a -> Bool Source #
(Subst t a, Eq a) => Eq (Elim' a) Source # |
Instance details Methods (==) :: Elim' a -> Elim' a -> Bool Source # (/=) :: Elim' a -> Elim' a -> Bool Source #
Ord (Substitution' Term) Source # |

Instance details

Methods

compare :: Substitution' Term -> Substitution' Term -> Ordering Source #

(<) :: Substitution' Term -> Substitution' Term -> Bool Source #

(<=) :: Substitution' Term -> Substitution' Term -> Bool Source #

(>) :: Substitution' Term -> Substitution' Term -> Bool Source #

(>=) :: Substitution' Term -> Substitution' Term -> Bool Source #

max :: Substitution' Term -> Substitution' Term -> Substitution' Term Source #

min :: Substitution' Term -> Substitution' Term -> Substitution' Term Source #

(Subst t a, Ord a) => Ord (Tele a) Source # |
Instance details Methods compare :: Tele a -> Tele a -> Ordering Source # (<) :: Tele a -> Tele a -> Bool Source # (<=) :: Tele a -> Tele a -> Bool Source # (>) :: Tele a -> Tele a -> Bool Source # (>=) :: Tele a -> Tele a -> Bool Source # max :: Tele a -> Tele a -> Tele a Source # min :: Tele a -> Tele a -> Tele a Source #
Ord a => Ord (Type' a) Source # |
Instance details Methods compare :: Type' a -> Type' a -> Ordering Source # (<) :: Type' a -> Type' a -> Bool Source # (<=) :: Type' a -> Type' a -> Bool Source # (>) :: Type' a -> Type' a -> Bool Source # (>=) :: Type' a -> Type' a -> Bool Source # max :: Type' a -> Type' a -> Type' a Source # min :: Type' a -> Type' a -> Type' a Source #
(Subst t a, Ord a) => Ord (Abs a) Source # |
Instance details Methods compare :: Abs a -> Abs a -> Ordering Source # (<) :: Abs a -> Abs a -> Bool Source # (<=) :: Abs a -> Abs a -> Bool Source # (>) :: Abs a -> Abs a -> Bool Source # (>=) :: Abs a -> Abs a -> Bool Source # max :: Abs a -> Abs a -> Abs a Source # min :: Abs a -> Abs a -> Abs a Source #
(Subst t a, Ord a) => Ord (Elim' a) Source # |
Instance details Methods compare :: Elim' a -> Elim' a -> Ordering Source # (<) :: Elim' a -> Elim' a -> Bool Source # (<=) :: Elim' a -> Elim' a -> Bool Source # (>) :: Elim' a -> Elim' a -> Bool Source # (>=) :: Elim' a -> Elim' a -> Bool Source # max :: Elim' a -> Elim' a -> Elim' a Source # min :: Elim' a -> Elim' a -> Elim' a Source #
Abstract t => Abstract [t] Source # |
Instance details Methods abstract :: Telescope -> [t] -> [t] Source #
Abstract [Occurrence] Source # |
Instance details Methods abstract :: Telescope -> [Occurrence] -> [Occurrence] Source #
Abstract [Polarity] Source # |
Instance details Methods abstract :: Telescope -> [Polarity] -> [Polarity] Source #
Abstract t => Abstract (Maybe t) Source # |
Instance details Methods abstract :: Telescope -> Maybe t -> Maybe t Source #
DoDrop a => Abstract (Drop a) Source # |
Instance details Methods abstract :: Telescope -> Drop a -> Drop a Source #
Abstract a => Abstract (Case a) Source # |
Instance details Methods abstract :: Telescope -> Case a -> Case a Source #
Abstract a => Abstract (WithArity a) Source # |
Instance details Methods abstract :: Telescope -> WithArity a -> WithArity a Source #
Apply t => Apply [t] Source # |
Instance details Methods apply :: [t] -> Args -> [t] Source # applyE :: [t] -> Elims -> [t] Source #
Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns.
Instance details Methods apply :: [NamedArg (Pattern' a)] -> Args -> [NamedArg (Pattern' a)] Source # applyE :: [NamedArg (Pattern' a)] -> Elims -> [NamedArg (Pattern' a)] Source #
Apply [Occurrence] Source # |
Instance details Methods apply :: [Occurrence] -> Args -> [Occurrence] Source # applyE :: [Occurrence] -> Elims -> [Occurrence] Source #
Apply [Polarity] Source # |
Instance details Methods apply :: [Polarity] -> Args -> [Polarity] Source # applyE :: [Polarity] -> Elims -> [Polarity] Source #
Apply t => Apply (Maybe t) Source # |
Instance details Methods apply :: Maybe t -> Args -> Maybe t Source # applyE :: Maybe t -> Elims -> Maybe t Source #
DoDrop a => Apply (Drop a) Source # |
Instance details Methods apply :: Drop a -> Args -> Drop a Source # applyE :: Drop a -> Elims -> Drop a Source #
Apply t => Apply (Blocked t) Source # |
Instance details Methods apply :: Blocked t -> Args -> Blocked t Source # applyE :: Blocked t -> Elims -> Blocked t Source #
Subst Term a => Apply (Tele a) Source # |
Instance details Methods apply :: Tele a -> Args -> Tele a Source # applyE :: Tele a -> Elims -> Tele a Source #
Apply a => Apply (Case a) Source # |
Instance details Methods apply :: Case a -> Args -> Case a Source # applyE :: Case a -> Elims -> Case a Source #
Apply a => Apply (WithArity a) Source # |
Instance details Methods apply :: WithArity a -> Args -> WithArity a Source # applyE :: WithArity a -> Elims -> WithArity a Source #
Abstract v => Abstract (HashMap k v) Source # |
Instance details Methods abstract :: Telescope -> HashMap k v -> HashMap k v Source #
Abstract v => Abstract (Map k v) Source # |
Instance details Methods abstract :: Telescope -> Map k v -> Map k v Source #
(Apply a, Apply b) => Apply (a, b) Source # |
Instance details Methods apply :: (a, b) -> Args -> (a, b) Source # applyE :: (a, b) -> Elims -> (a, b) Source #
Apply v => Apply (HashMap k v) Source # |
Instance details Methods apply :: HashMap k v -> Args -> HashMap k v Source # applyE :: HashMap k v -> Elims -> HashMap k v Source #
Apply v => Apply (Map k v) Source # |
Instance details Methods apply :: Map k v -> Args -> Map k v Source # applyE :: Map k v -> Elims -> Map k v Source #
(Apply a, Apply b, Apply c) => Apply (a, b, c) Source # |
Instance details Methods apply :: (a, b, c) -> Args -> (a, b, c) Source # applyE :: (a, b, c) -> Elims -> (a, b, c) Source #