Agda-2.8.0: 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

- sort :: Sort -> Type
- data TelV a = TelV {
  - theTel :: Tele (Dom a)
  - theCore :: a
  }
- piApply :: Type -> Args -> Type
- telView' :: Type -> TelView
- mkLam :: Arg ArgName -> Term -> Term
- funSort :: Sort -> Sort -> Sort
- renaming :: DeBruijn a => Impossible -> Permutation -> Substitution' a
- piSort :: Dom Term -> Sort -> Abs Sort -> Sort
- univSort :: Sort -> Sort
- mkPi :: Dom (ArgName, Type) -> Type -> Type
- lamView :: Term -> ([Arg ArgName], Term)
- applyTermE :: (Coercible Term t, Apply t, EndoSubst t) => (Empty -> Term -> Elims -> Term) -> t -> Elims -> t
- defApp :: QName -> Elims -> Elims -> Term
- conApp :: (Coercible t Term, Apply t) => (Empty -> Term -> Elims -> Term) -> ConHead -> ConInfo -> Elims -> Elims -> Term
- canProject :: QName -> Term -> Maybe (Arg Term)
- relToDontCare :: LensRelevance a => a -> Term -> Term
- argToDontCare :: Arg Term -> Term
- applyNLPatSubst :: TermSubst a => Substitution' NLPat -> a -> a
- teleLam :: Telescope -> Term -> Term
- telePi_ :: Telescope -> Type -> Type
- namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern]
- telVars :: Int -> Telescope -> [Arg DeBruijnPattern]
- abstractArgs :: Abstract a => Args -> a -> a
- renamingR :: DeBruijn a => Permutation -> Substitution' a
- renameP :: Subst a => Impossible -> Permutation -> a -> a
- applySubstTerm :: (Coercible t Term, EndoSubst t, Apply t) => Substitution' t -> t -> t
- levelTm :: Level -> Term
- applyNLSubstToDom :: SubstWith NLPat a => Substitution' NLPat -> Dom a -> Dom a
- fromPatternSubstitution :: PatternSubstitution -> Substitution
- applyPatSubst :: TermSubst a => PatternSubstitution -> a -> a
- usePatOrigin :: PatOrigin -> Pattern' a -> Pattern' a
- usePatternInfo :: PatternInfo -> Pattern' a -> Pattern' a
- projDropParsApply :: Projection -> ProjOrigin -> Relevance -> Args -> Term
- type TelView = TelV Type
- telView'UpTo :: Int -> Type -> TelView
- absV :: Dom a -> ArgName -> TelV a -> TelV a
- bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a
- bindsToTel :: [Name] -> Dom Type -> ListTel
- bindsToTel'1 :: (Name -> a) -> List1 Name -> Dom Type -> ListTel' a
- bindsToTel1 :: List1 Name -> Dom Type -> ListTel
- namedBindsToTel :: [NamedArg Name] -> Type -> Telescope
- domFromNamedArgName :: NamedArg Name -> Dom ()
- namedBindsToTel1 :: List1 (NamedArg Name) -> Type -> Telescope
- mkPiSort :: Dom Type -> Abs Type -> Sort
- unlamView :: [Arg ArgName] -> Term -> Term
- telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type
- telePi :: Telescope -> Type -> Type
- telePiVisible :: Telescope -> Type -> Type
- class TeleNoAbs a where
  - teleNoAbs :: a -> Term -> Term
- typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type]
- compiledClauseBody :: Clause -> Maybe Term
- univSort' :: Sort -> Either Blocker Sort
- ssort :: Level -> Type
- data SizeOfSort = SizeOfSort {
  - szSortUniv :: Univ
  - szSortSize :: Integer
  }
- pattern SmallSort :: Univ -> SizeOfSort
- pattern LargeSort :: Univ -> Integer -> SizeOfSort
- sizeOfSort :: Sort -> Either Blocker SizeOfSort
- isSmallSort :: Sort -> Bool
- funSort' :: Sort -> Sort -> Either Blocker Sort
- levelLub :: Level -> Level -> Level
- piSort' :: Dom Term -> Sort -> Abs Sort -> Either Blocker Sort
- levelMax :: Integer -> [PlusLevel] -> Level
- module Agda.TypeChecking.Substitute.Class
- module Agda.TypeChecking.Substitute.DeBruijn
- data Substitution' a
  - = IdS
  - | EmptyS Impossible
  - | a :# (Substitution' a)
  - | Strengthen Impossible !Int (Substitution' a)
  - | Wk !Int (Substitution' a)
  - | Lift !Int (Substitution' a)
- type Substitution = Substitution' Term

# Documentation

sort :: Sort -> Type Source #

data TelV a Source #

Constructors

TelV |

Fields

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

#### Instances

Instances details

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 #
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 #
(TermSubst 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 #
(TermSubst 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 #

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.

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.

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

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

renaming :: DeBruijn a => Impossible -> Permutation -> Substitution' a Source #

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

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

univSort :: Sort -> Sort Source #

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

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

lamView :: Term -> ([Arg ArgName], Term) Source #

applyTermE :: (Coercible Term t, Apply t, EndoSubst t) => (Empty -> Term -> Elims -> Term) -> t -> Elims -> t Source #

Apply `Elims` while using the given function to report ill-typed redexes. Recursive calls for `applyE` and `applySubst` happen at type `t` to propagate the same strategy to subtrees.

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.

conApp :: (Coercible t Term, Apply t) => (Empty -> Term -> Elims -> Term) -> ConHead -> ConInfo -> Elims -> Elims -> Term Source #

Eliminate a constructed term.

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

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

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

argToDontCare :: Arg Term -> Term Source #

applyNLPatSubst :: TermSubst a => Substitution' NLPat -> a -> a Source #

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`.

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

Everything will be an `Abs`.

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

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

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

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

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

renameP :: Subst a => Impossible -> Permutation -> a -> a Source #

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

applySubstTerm :: (Coercible t Term, EndoSubst t, Apply t) => Substitution' t -> t -> t Source #

levelTm :: Level -> Term Source #

applyNLSubstToDom :: SubstWith NLPat a => Substitution' NLPat -> Dom a -> Dom a Source #

fromPatternSubstitution :: PatternSubstitution -> Substitution Source #

applyPatSubst :: TermSubst a => PatternSubstitution -> a -> a Source #

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

usePatternInfo :: PatternInfo -> Pattern' a -> Pattern' a Source #

projDropParsApply :: Projection -> ProjOrigin -> Relevance -> 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.

type TelView = TelV Type Source #

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`.

absV :: Dom a -> ArgName -> TelV a -> TelV a Source #

Add given binding to the front of the telescope.

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 #

bindsToTel'1 :: (Name -> a) -> List1 Name -> Dom Type -> ListTel' a Source #

bindsToTel1 :: List1 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 #

namedBindsToTel1 :: List1 (NamedArg Name) -> Type -> Telescope Source #

mkPiSort :: Dom Type -> Abs Type -> Sort Source #

unlamView :: [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.

telePiVisible :: Telescope -> Type -> Type Source #

Only abstract the visible components of the telescope, and all that bind variables. Everything will be an `Abs`! Caution: quadratic time!

class TeleNoAbs a where Source #

Performs void (`noAbs`) abstraction over telescope.

Methods

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

#### Instances

Instances details

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 #

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' :: Sort -> Either Blocker Sort Source #

`univSort' univInf s` gets the next higher sort of `s`, if it is known (i.e. it is not just `UnivSort s`).

Precondition: `s` is reduced

ssort :: Level -> Type Source #

data SizeOfSort Source #

A sort can either be small (Set l, Prop l, Size, ...) or large (Setω n).

Constructors

SizeOfSort |

Fields

- szSortUniv :: Univ
- szSortSize :: Integer

pattern SmallSort :: Univ -> SizeOfSort Source #

pattern LargeSort :: Univ -> Integer -> SizeOfSort Source #

sizeOfSort :: Sort -> Either Blocker SizeOfSort Source #

Returns `Left blocker` for unknown (blocked) sorts, and otherwise returns `Right s` where `s` indicates the size and fibrancy.

isSmallSort :: Sort -> Bool Source #

funSort' :: Sort -> Sort -> Either Blocker Sort Source #

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

This function should only be called on reduced sorts, since the `LevelUniv` rules should only apply when the sort does not reduce to `Set`.

levelLub :: Level -> Level -> Level Source #

Given two levels `a` and `b`, compute `a ⊔ b` and return its canonical form.

piSort' :: Dom Term -> Sort -> Abs Sort -> Either Blocker Sort Source #

Compute the sort of a pi type from the sorts of its domain and codomain. This function should only be called on reduced sorts, since the `LevelUniv` rules should only apply when the sort doesn't reduce to `Set`

levelMax :: Integer -> [PlusLevel] -> Level Source #

module Agda.TypeChecking.Substitute.Class

module Agda.TypeChecking.Substitute.DeBruijn

data Substitution' a Source #

Substitutions.

Constructors

IdS | Identity substitution. `Γ ⊢ IdS : Γ`
EmptyS Impossible | Empty substitution, lifts from the empty context. First argument is `IMPOSSIBLE`. 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 Impossible !Int (Substitution' a)

Strengthening substitution. First argument is `IMPOSSIBLE`. In `'Strengthen err n ρ` the number `n` must be non-negative. This substitution should only be applied to values `t` for which none of the variables `0` up to `n - 1` are free in `t[ρ]`, and in that case `n` is subtracted from all free de Bruijn indices in `t[ρ]`. Γ ⊢ ρ : Δ |Θ| = n --------------------------- Γ ⊢ Strengthen n ρ : Δ, Θ @

Wk !Int (Substitution' a) | Weakening 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

Instances details

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 #
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 #

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 #
Eq Substitution Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Substitution -> Substitution -> Bool Source # (/=) :: Substitution -> Substitution -> Bool Source #
Ord Substitution Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

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

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

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

max :: Substitution -> Substitution -> Substitution Source #

min :: Substitution -> Substitution -> Substitution 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 #
NamesIn a => NamesIn (Substitution' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Substitution' a -> m Source #
(Pretty a, PrettyTCM a, EndoSubst a) => PrettyTCM (Substitution' a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Substitution' a -> m Doc Source #
EmbPrj a => EmbPrj (Substitution' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Substitution' a -> S Word32 Source # icod_ :: Substitution' a -> S Word32 Source # value :: Word32 -> R (Substitution' a) Source #
EndoSubst a => Subst (Substitution' a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Substitution' a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Substitution' a) = a

Methods

applySubst :: Substitution' (SubstArg (Substitution' a)) -> Substitution' a -> Substitution' a Source #

Null (Substitution' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods empty :: Substitution' a Source # null :: Substitution' a -> Bool Source #
NFData a => NFData (Substitution' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Substitution' a -> () Source #
Generic (Substitution' a) Source # |

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep (Substitution' a) |

Instance details

Defined in Agda.Syntax.Internal

type Rep (Substitution' a) = D1 ('MetaData "Substitution'" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((C1 ('MetaCons "IdS" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "EmptyS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible)) :+: C1 ('MetaCons ":#" ('InfixI 'RightAssociative 4) 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))))) :+: (C1 ('MetaCons "Strengthen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a)))) :+: (C1 ('MetaCons "Wk" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))) :+: C1 ('MetaCons "Lift" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))))))

Methods

from :: Substitution' a -> Rep (Substitution' a) x Source #

to :: Rep (Substitution' a) x -> Substitution' a 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 #
type SubstArg (Substitution' a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Substitution' a) = a
type Rep (Substitution' a) Source # |

Instance details

Defined in Agda.Syntax.Internal

type Rep (Substitution' a) = D1 ('MetaData "Substitution'" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((C1 ('MetaCons "IdS" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "EmptyS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible)) :+: C1 ('MetaCons ":#" ('InfixI 'RightAssociative 4) 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))))) :+: (C1 ('MetaCons "Strengthen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a)))) :+: (C1 ('MetaCons "Wk" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))) :+: C1 ('MetaCons "Lift" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))))))

type Substitution = Substitution' Term Source #

# Orphan instances

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 Term Source # |
Instance details Methods abstract :: Telescope -> Term -> Term Source #
Abstract Type Source # |
Instance details Methods abstract :: Telescope -> Type -> Type Source #
Abstract CompiledClauses Source # |
Instance details Methods abstract :: Telescope -> CompiledClauses -> CompiledClauses Source #
Abstract Definition Source # |
Instance details Methods abstract :: Telescope -> Definition -> Definition Source #
Abstract Defn Source # |
Instance details Methods abstract :: Telescope -> Defn -> Defn Source #
Abstract FunctionInverse Source # |
Instance details Methods abstract :: Telescope -> FunctionInverse -> FunctionInverse Source #
Abstract NumGeneralizableArgs Source # |
Instance details Methods abstract :: Telescope -> NumGeneralizableArgs -> NumGeneralizableArgs Source #
Abstract PrimFun Source # |
Instance details Methods abstract :: Telescope -> PrimFun -> PrimFun Source #
Abstract ProjLams Source # |
Instance details Methods abstract :: Telescope -> ProjLams -> ProjLams Source #
Abstract Projection Source # |
Instance details Methods abstract :: Telescope -> Projection -> Projection 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 #
Abstract System Source # |
Instance details Methods abstract :: Telescope -> System -> System Source #
Abstract Permutation Source # |
Instance details Methods abstract :: Telescope -> Permutation -> Permutation Source #
Apply BraveTerm Source # |
Instance details Methods apply :: BraveTerm -> Args -> BraveTerm Source # applyE :: BraveTerm -> Elims -> BraveTerm 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 Definition Source # |
Instance details Methods apply :: Definition -> Args -> Definition Source # applyE :: Definition -> Elims -> Definition Source #
Apply Defn Source # |
Instance details Methods apply :: Defn -> Args -> Defn Source # applyE :: Defn -> Elims -> Defn Source #
Apply DisplayTerm Source # |
Instance details Methods apply :: DisplayTerm -> Args -> DisplayTerm Source # applyE :: DisplayTerm -> Elims -> DisplayTerm Source #
Apply ExtLamInfo Source # |
Instance details Methods apply :: ExtLamInfo -> Args -> ExtLamInfo Source # applyE :: ExtLamInfo -> Elims -> ExtLamInfo Source #
Apply FunctionInverse Source # |
Instance details Methods apply :: FunctionInverse -> Args -> FunctionInverse Source # applyE :: FunctionInverse -> Elims -> FunctionInverse Source #
Apply NumGeneralizableArgs Source # |
Instance details Methods apply :: NumGeneralizableArgs -> Args -> NumGeneralizableArgs Source # applyE :: NumGeneralizableArgs -> Elims -> NumGeneralizableArgs Source #
Apply PrimFun Source # |
Instance details Methods apply :: PrimFun -> Args -> PrimFun Source # applyE :: PrimFun -> Elims -> PrimFun 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 RewriteRule Source # |
Instance details Methods apply :: RewriteRule -> Args -> RewriteRule Source # applyE :: RewriteRule -> Elims -> RewriteRule Source #
Apply System Source # |
Instance details Methods apply :: System -> Args -> System Source # applyE :: System -> Elims -> System Source #
Apply Permutation Source # |
Instance details Methods apply :: Permutation -> Args -> Permutation Source # applyE :: Permutation -> Elims -> Permutation Source #
Subst ProblemEq Source # |

Instance details

Associated Types

type SubstArg ProblemEq |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg ProblemEq = Term

Methods

applySubst :: Substitution' (SubstArg ProblemEq) -> ProblemEq -> ProblemEq Source #

Subst Name Source # |

Instance details

Associated Types

type SubstArg Name |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Name = Term

Methods

applySubst :: Substitution' (SubstArg Name) -> Name -> Name Source #

Subst BraveTerm Source # |

Instance details

Associated Types

type SubstArg BraveTerm |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg BraveTerm = BraveTerm

Methods

applySubst :: Substitution' (SubstArg BraveTerm) -> BraveTerm -> BraveTerm Source #

Subst ConPatternInfo Source # |

Instance details

Associated Types

type SubstArg ConPatternInfo |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg ConPatternInfo = Term

Methods

applySubst :: Substitution' (SubstArg ConPatternInfo) -> ConPatternInfo -> ConPatternInfo Source #

Subst DeBruijnPattern Source # |

Instance details

Associated Types

type SubstArg DeBruijnPattern |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg DeBruijnPattern = DeBruijnPattern

Methods

applySubst :: Substitution' (SubstArg DeBruijnPattern) -> DeBruijnPattern -> DeBruijnPattern Source #

Subst EqualityTypeData Source # |

Instance details

Associated Types

type SubstArg EqualityTypeData |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg EqualityTypeData = Term

Methods

applySubst :: Substitution' (SubstArg EqualityTypeData) -> EqualityTypeData -> EqualityTypeData Source #

Subst EqualityView Source # |

Instance details

Associated Types

type SubstArg EqualityView |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg EqualityView = Term

Methods

applySubst :: Substitution' (SubstArg EqualityView) -> EqualityView -> EqualityView Source #

Subst Pattern Source # |

Instance details

Associated Types

type SubstArg Pattern |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Pattern = Term

Methods

applySubst :: Substitution' (SubstArg Pattern) -> Pattern -> Pattern Source #

Subst Term Source # |

Instance details

Associated Types

type SubstArg Term |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Term = Term

Methods

applySubst :: Substitution' (SubstArg Term) -> Term -> Term Source #

Subst Range Source # |

Instance details

Associated Types

type SubstArg Range |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Range = Term

Methods

applySubst :: Substitution' (SubstArg Range) -> Range -> Range Source #

Subst Candidate Source # |

Instance details

Associated Types

type SubstArg Candidate |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Candidate = Term

Methods

applySubst :: Substitution' (SubstArg Candidate) -> Candidate -> Candidate Source #

Subst CompareAs Source # |

Instance details

Associated Types

type SubstArg CompareAs |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg CompareAs = Term

Methods

applySubst :: Substitution' (SubstArg CompareAs) -> CompareAs -> CompareAs Source #

Subst Constraint Source # |

Instance details

Associated Types

type SubstArg Constraint |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Constraint = Term

Methods

applySubst :: Substitution' (SubstArg Constraint) -> Constraint -> Constraint Source #

Subst DisplayForm Source # |

Instance details

Associated Types

type SubstArg DisplayForm |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg DisplayForm = Term

Methods

applySubst :: Substitution' (SubstArg DisplayForm) -> DisplayForm -> DisplayForm Source #

Subst DisplayTerm Source # |

Instance details

Associated Types

type SubstArg DisplayTerm |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg DisplayTerm = Term

Methods

applySubst :: Substitution' (SubstArg DisplayTerm) -> DisplayTerm -> DisplayTerm Source #

Subst LetBinding Source # |

Instance details

Associated Types

type SubstArg LetBinding |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg LetBinding = Term

Methods

applySubst :: Substitution' (SubstArg LetBinding) -> LetBinding -> LetBinding Source #

Subst NLPSort Source # |

Instance details

Associated Types

type SubstArg NLPSort |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg NLPSort = NLPat

Methods

applySubst :: Substitution' (SubstArg NLPSort) -> NLPSort -> NLPSort Source #

Subst NLPType Source # |

Instance details

Associated Types

type SubstArg NLPType |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg NLPType = NLPat

Methods

applySubst :: Substitution' (SubstArg NLPType) -> NLPType -> NLPType Source #

Subst NLPat Source # |

Instance details

Associated Types

type SubstArg NLPat |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg NLPat = NLPat

Methods

applySubst :: Substitution' (SubstArg NLPat) -> NLPat -> NLPat Source #

Subst RewriteRule Source # |

Instance details

Associated Types

type SubstArg RewriteRule |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg RewriteRule = NLPat

Methods

applySubst :: Substitution' (SubstArg RewriteRule) -> RewriteRule -> RewriteRule Source #

Subst ContextEntry Source # |

Instance details

Associated Types

type SubstArg ContextEntry |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg ContextEntry = Term

Methods

applySubst :: Substitution' (SubstArg ContextEntry) -> ContextEntry -> ContextEntry Source #

Subst () Source # |

Instance details

Associated Types

type SubstArg () |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg () = Term

Methods

applySubst :: Substitution' (SubstArg ()) -> () -> () Source #

DeBruijn BraveTerm Source # |
Instance details Methods deBruijnVar :: Int -> BraveTerm Source # deBruijnNamedVar :: String -> Int -> BraveTerm Source # deBruijnView :: BraveTerm -> Maybe Int Source #
DeBruijn NLPat Source # |
Instance details Methods deBruijnVar :: Int -> NLPat Source # deBruijnNamedVar :: String -> Int -> NLPat Source # deBruijnView :: NLPat -> Maybe Int Source #
Eq Level Source # |
Instance details Methods (==) :: Level -> Level -> Bool Source # (/=) :: Level -> Level -> Bool Source #
Eq NotBlocked Source # |
Instance details Methods (==) :: NotBlocked -> NotBlocked -> Bool Source # (/=) :: NotBlocked -> NotBlocked -> Bool Source #
Eq PlusLevel Source # |
Instance details Methods (==) :: PlusLevel -> PlusLevel -> Bool Source # (/=) :: PlusLevel -> PlusLevel -> Bool Source #
Eq Sort Source # |
Instance details Methods (==) :: Sort -> Sort -> Bool Source # (/=) :: Sort -> Sort -> Bool Source #
Eq Substitution Source # |
Instance details Methods (==) :: Substitution -> Substitution -> Bool Source # (/=) :: Substitution -> Substitution -> 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 CandidateKind Source # |
Instance details Methods (==) :: CandidateKind -> CandidateKind -> Bool Source # (/=) :: CandidateKind -> CandidateKind -> Bool Source #
Eq Section Source # |
Instance details Methods (==) :: Section -> Section -> Bool Source # (/=) :: Section -> Section -> Bool 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 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 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 Substitution Source # |

Instance details

Methods

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

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

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

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

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

max :: Substitution -> Substitution -> Substitution Source #

min :: Substitution -> Substitution -> Substitution 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 #
Ord Candidate Source # |
Instance details Methods compare :: Candidate -> Candidate -> Ordering Source # (<) :: Candidate -> Candidate -> Bool Source # (<=) :: Candidate -> Candidate -> Bool Source # (>) :: Candidate -> Candidate -> Bool Source # (>=) :: Candidate -> Candidate -> Bool Source # max :: Candidate -> Candidate -> Candidate Source # min :: Candidate -> Candidate -> Candidate Source #
Ord CandidateKind Source # |

Instance details

Methods

compare :: CandidateKind -> CandidateKind -> Ordering Source #

(<) :: CandidateKind -> CandidateKind -> Bool Source #

(<=) :: CandidateKind -> CandidateKind -> Bool Source #

(>) :: CandidateKind -> CandidateKind -> Bool Source #

(>=) :: CandidateKind -> CandidateKind -> Bool Source #

max :: CandidateKind -> CandidateKind -> CandidateKind Source #

min :: CandidateKind -> CandidateKind -> CandidateKind 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 #
DoDrop a => Abstract (Drop a) Source # |
Instance details Methods abstract :: Telescope -> Drop a -> Drop a Source #
Abstract t => Abstract (Maybe t) Source # |
Instance details Methods abstract :: Telescope -> Maybe t -> Maybe t Source #
Abstract [Polarity] Source # |
Instance details Methods abstract :: Telescope -> [Polarity] -> [Polarity] Source #
Abstract [Occurrence] Source # |
Instance details Methods abstract :: Telescope -> [Occurrence] -> [Occurrence] Source #
Abstract t => Abstract [t] Source # |
Instance details Methods abstract :: Telescope -> [t] -> [t] Source #
Apply t => Apply (Blocked t) Source # |
Instance details Methods apply :: Blocked t -> Args -> Blocked t Source # applyE :: Blocked t -> Elims -> Blocked t Source #
TermSubst 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 #
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 (Maybe t) Source # |
Instance details Methods apply :: Maybe t -> Args -> Maybe t Source # applyE :: Maybe t -> Elims -> Maybe t Source #
Apply t => Apply (Maybe t) Source # |
Instance details Methods apply :: Maybe t -> Args -> Maybe t Source # applyE :: Maybe t -> Elims -> Maybe 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 [Polarity] Source # |
Instance details Methods apply :: [Polarity] -> Args -> [Polarity] Source # applyE :: [Polarity] -> Elims -> [Polarity] Source #
Apply [Occurrence] Source # |
Instance details Methods apply :: [Occurrence] -> Args -> [Occurrence] Source # applyE :: [Occurrence] -> Elims -> [Occurrence] Source #
Apply t => Apply [t] Source # |
Instance details Methods apply :: [t] -> Args -> [t] Source # applyE :: [t] -> Elims -> [t] Source #
Subst a => Subst (Arg a) Source # |

Instance details

Associated Types

type SubstArg (Arg a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Arg a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Arg a)) -> Arg a -> Arg a Source #

Subst a => Subst (Ranged a) Source # |

Instance details

Associated Types

type SubstArg (Ranged a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Ranged a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Ranged a)) -> Ranged a -> Ranged a Source #

Subst a => Subst (WithHiding a) Source # |

Instance details

Associated Types

type SubstArg (WithHiding a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (WithHiding a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (WithHiding a)) -> WithHiding a -> WithHiding a Source #

Subst a => Subst (Abs a) Source # |

Instance details

Associated Types

type SubstArg (Abs a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Abs a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Abs a)) -> Abs a -> Abs a Source #

Subst a => Subst (Blocked a) Source # |

Instance details

Associated Types

type SubstArg (Blocked a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Blocked a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Blocked a)) -> Blocked a -> Blocked a Source #

Subst a => Subst (Level' a) Source # |

Instance details

Associated Types

type SubstArg (Level' a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Level' a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Level' a)) -> Level' a -> Level' a Source #

Subst a => Subst (PlusLevel' a) Source # |

Instance details

Associated Types

type SubstArg (PlusLevel' a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (PlusLevel' a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (PlusLevel' a)) -> PlusLevel' a -> PlusLevel' a Source #

(Coercible a Term, Subst a) => Subst (Sort' a) Source # |

Instance details

Associated Types

type SubstArg (Sort' a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Sort' a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Sort' a)) -> Sort' a -> Sort' a Source #

EndoSubst a => Subst (Substitution' a) Source # |

Instance details

Associated Types

type SubstArg (Substitution' a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Substitution' a) = a

Methods

applySubst :: Substitution' (SubstArg (Substitution' a)) -> Substitution' a -> Substitution' a Source #

Subst a => Subst (Tele a) Source # |

Instance details

Associated Types

type SubstArg (Tele a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Tele a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Tele a)) -> Tele a -> Tele a Source #

Subst a => Subst (Elim' a) Source # |

Instance details

Associated Types

type SubstArg (Elim' a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Elim' a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Elim' a)) -> Elim' a -> Elim' a Source #

Subst a => Subst (List1 a) Source # |

Instance details

Associated Types

type SubstArg (List1 a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (List1 a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (List1 a)) -> List1 a -> List1 a Source #

Subst a => Subst (Maybe a) Source # |

Instance details

Associated Types

type SubstArg (Maybe a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Maybe a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Maybe a)) -> Maybe a -> Maybe a Source #

Subst a => Subst [a] Source # |

Instance details

Associated Types

type SubstArg [a] |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg [a] = SubstArg a

Methods

applySubst :: Substitution' (SubstArg [a]) -> [a] -> [a] Source #

DeBruijn a => DeBruijn (Pattern' a) Source # |
Instance details Methods deBruijnVar :: Int -> Pattern' a Source # deBruijnNamedVar :: String -> Int -> Pattern' a Source # deBruijnView :: Pattern' a -> Maybe Int Source #
(Subst 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 #
Eq t => Eq (Blocked t) Source # |
Instance details Methods (==) :: Blocked t -> Blocked t -> Bool Source # (/=) :: Blocked t -> Blocked t -> Bool Source #
Eq a => Eq (Pattern' a) Source # |
Instance details Methods (==) :: Pattern' a -> Pattern' a -> Bool Source # (/=) :: Pattern' a -> Pattern' a -> Bool Source #
(Subst 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 a, Eq a) => Eq (Elim' a) Source # |
Instance details Methods (==) :: Elim' a -> Elim' a -> Bool Source # (/=) :: Elim' a -> Elim' a -> Bool Source #
(Subst 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 #
Ord a => Ord (Dom a) Source # |
Instance details Methods compare :: Dom a -> Dom a -> Ordering Source # (<) :: Dom a -> Dom a -> Bool Source # (<=) :: Dom a -> Dom a -> Bool Source # (>) :: Dom a -> Dom a -> Bool Source # (>=) :: Dom a -> Dom a -> Bool Source # max :: Dom a -> Dom a -> Dom a Source # min :: Dom a -> Dom a -> Dom a Source #
(Subst 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 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 v => Abstract (Map k v) Source # |
Instance details Methods abstract :: Telescope -> Map k v -> Map k v Source #
Abstract v => Abstract (HashMap k v) Source # |
Instance details Methods abstract :: Telescope -> HashMap k v -> 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 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 a, Apply b) => Apply (a, b) Source # |
Instance details Methods apply :: (a, b) -> Args -> (a, b) Source # applyE :: (a, b) -> Elims -> (a, b) Source #
Subst a => Subst (Named name a) Source # |

Instance details

Associated Types

type SubstArg (Named name a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Named name a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Named name a)) -> Named name a -> Named name a Source #

(Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Dom' a b) Source # |

Instance details

Associated Types

type SubstArg (Dom' a b) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Dom' a b) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Dom' a b)) -> Dom' a b -> Dom' a b Source #

(Coercible a Term, Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Type'' a b) Source # |

Instance details

Associated Types

type SubstArg (Type'' a b) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Type'' a b) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Type'' a b)) -> Type'' a b -> Type'' a b Source #

(Ord k, Subst a) => Subst (Map k a) Source # |

Instance details

Associated Types

type SubstArg (Map k a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Map k a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Map k a)) -> Map k a -> Map k a Source #

(Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (a, b) Source # |

Instance details

Associated Types

type SubstArg (a, b) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (a, b) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (a, b)) -> (a, b) -> (a, b) 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 #
(Subst a, Subst b, Subst c, SubstArg a ~ SubstArg b, SubstArg b ~ SubstArg c) => Subst (a, b, c) Source # |

Instance details

Associated Types

type SubstArg (a, b, c) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (a, b, c) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (a, b, c)) -> (a, b, c) -> (a, b, c) Source #

(Subst a, Subst b, Subst c, Subst d, SubstArg a ~ SubstArg b, SubstArg b ~ SubstArg c, SubstArg c ~ SubstArg d) => Subst (a, b, c, d) Source # |

Instance details

Associated Types

type SubstArg (a, b, c, d) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (a, b, c, d) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (a, b, c, d)) -> (a, b, c, d) -> (a, b, c, d) Source #