Agda-2.6.2.2.20230105: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Substitute

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

Documentation

data TelV a Source #

Constructors

TelV 

Fields

Instances

Instances details
Functor TelV Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

fmap :: (a -> b) -> TelV a -> TelV b #

(<$) :: a -> TelV b -> TelV a #

Show a => Show (TelV a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

showsPrec :: Int -> TelV a -> ShowS #

show :: TelV a -> String #

showList :: [TelV a] -> ShowS #

(TermSubst a, Eq a) => Eq (TelV a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

(==) :: TelV a -> TelV a -> Bool #

(/=) :: TelV a -> TelV a -> Bool #

(TermSubst a, Ord a) => Ord (TelV a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

compare :: TelV a -> TelV a -> Ordering #

(<) :: TelV a -> TelV a -> Bool #

(<=) :: TelV a -> TelV a -> Bool #

(>) :: TelV a -> TelV a -> Bool #

(>=) :: TelV a -> TelV a -> Bool #

max :: TelV a -> TelV a -> TelV a #

min :: TelV a -> TelV a -> TelV a #

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

data SizeOfSort Source #

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

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

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

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

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

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

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

applyTermE :: forall t. (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 :: forall t. (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.

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.

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.

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

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

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

applySubstTerm :: forall t. (Coercible t Term, EndoSubst t, Apply t) => Substitution' t -> t -> t 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.

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.

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.

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

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

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!

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

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.

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

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

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.

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

InstantiateFull Substitution Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Foldable Substitution' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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

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

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

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

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

null :: Substitution' a -> Bool #

length :: Substitution' a -> Int #

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

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

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

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

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

Traversable Substitution' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

traverse :: Applicative f => (a -> f b) -> Substitution' a -> f (Substitution' b) #

sequenceA :: Applicative f => Substitution' (f a) -> f (Substitution' a) #

mapM :: Monad m => (a -> m b) -> Substitution' a -> m (Substitution' b) #

sequence :: Monad m => Substitution' (m a) -> m (Substitution' a) #

Functor Substitution' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

fmap :: (a -> b) -> Substitution' a -> Substitution' b #

(<$) :: a -> Substitution' b -> Substitution' a #

Eq Substitution Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Ord Substitution Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

TermSize a => TermSize (Substitution' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

NamesIn a => NamesIn (Substitution' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

(Pretty a, PrettyTCM a, EndoSubst a) => PrettyTCM (Substitution' a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

EmbPrj a => EmbPrj (Substitution' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EndoSubst a => Subst (Substitution' a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Substitution' a) Source #

Null (Substitution' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty a => Pretty (Substitution' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Generic (Substitution' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep (Substitution' a) :: Type -> Type #

Show a => Show (Substitution' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

NFData a => NFData (Substitution' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Substitution' a -> () #

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.6.2.2.20230105-inplace" '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))))))

Orphan instances

Abstract Clause Source # 
Instance details

Abstract Sort Source # 
Instance details

Abstract Telescope Source # 
Instance details

Abstract Term Source # 
Instance details

Abstract Type Source # 
Instance details

Abstract CompiledClauses Source # 
Instance details

Abstract Definition Source # 
Instance details

Abstract Defn Source # 
Instance details

Abstract FunctionInverse Source # 
Instance details

Abstract NumGeneralizableArgs Source # 
Instance details

Abstract PrimFun Source # 
Instance details

Abstract ProjLams Source # 
Instance details

Abstract Projection Source # 
Instance details

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

Abstract System Source # 
Instance details

Abstract Permutation Source # 
Instance details

Apply BraveTerm Source # 
Instance details

Apply Clause Source # 
Instance details

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

Apply Definition Source # 
Instance details

Apply Defn Source # 
Instance details

Methods

apply :: Defn -> Args -> Defn Source #

applyE :: Defn -> Elims -> Defn Source #

Apply DisplayTerm Source # 
Instance details

Apply ExtLamInfo Source # 
Instance details

Apply FunctionInverse Source # 
Instance details

Apply NumGeneralizableArgs Source # 
Instance details

Apply PrimFun Source # 
Instance details

Apply ProjLams Source # 
Instance details

Apply Projection Source # 
Instance details

Apply RewriteRule Source # 
Instance details

Apply System Source # 
Instance details

Apply Permutation Source # 
Instance details

Subst ProblemEq Source # 
Instance details

Associated Types

type SubstArg ProblemEq Source #

Subst Name Source # 
Instance details

Associated Types

type SubstArg Name Source #

Subst BraveTerm Source # 
Instance details

Associated Types

type SubstArg BraveTerm Source #

Subst ConPatternInfo Source # 
Instance details

Associated Types

type SubstArg ConPatternInfo Source #

Subst DeBruijnPattern Source # 
Instance details

Associated Types

type SubstArg DeBruijnPattern Source #

Subst EqualityTypeData Source # 
Instance details

Associated Types

type SubstArg EqualityTypeData Source #

Subst EqualityView Source # 
Instance details

Associated Types

type SubstArg EqualityView Source #

Subst Pattern Source # 
Instance details

Associated Types

type SubstArg Pattern Source #

Subst Term Source # 
Instance details

Associated Types

type SubstArg Term Source #

Subst Range Source # 
Instance details

Associated Types

type SubstArg Range Source #

Subst Candidate Source # 
Instance details

Associated Types

type SubstArg Candidate Source #

Subst CompareAs Source # 
Instance details

Associated Types

type SubstArg CompareAs Source #

Subst Constraint Source # 
Instance details

Associated Types

type SubstArg Constraint Source #

Subst DisplayForm Source # 
Instance details

Associated Types

type SubstArg DisplayForm Source #

Subst DisplayTerm Source # 
Instance details

Associated Types

type SubstArg DisplayTerm Source #

Subst NLPSort Source # 
Instance details

Associated Types

type SubstArg NLPSort Source #

Subst NLPType Source # 
Instance details

Associated Types

type SubstArg NLPType Source #

Subst NLPat Source # 
Instance details

Associated Types

type SubstArg NLPat Source #

Subst RewriteRule Source # 
Instance details

Associated Types

type SubstArg RewriteRule Source #

Subst () Source # 
Instance details

Associated Types

type SubstArg () Source #

Methods

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

DeBruijn BraveTerm Source # 
Instance details

DeBruijn NLPat Source # 
Instance details

Eq Level Source # 
Instance details

Methods

(==) :: Level -> Level -> Bool #

(/=) :: Level -> Level -> Bool #

Eq NotBlocked Source # 
Instance details

Eq PlusLevel Source # 
Instance details

Eq Sort Source # 
Instance details

Methods

(==) :: Sort -> Sort -> Bool #

(/=) :: Sort -> Sort -> Bool #

Eq Substitution Source # 
Instance details

Eq Term Source #

Syntactic Term equality, ignores stuff below DontCare and sharing.

Instance details

Methods

(==) :: Term -> Term -> Bool #

(/=) :: Term -> Term -> Bool #

Eq Candidate Source # 
Instance details

Eq CandidateKind Source # 
Instance details

Eq Section Source # 
Instance details

Methods

(==) :: Section -> Section -> Bool #

(/=) :: Section -> Section -> Bool #

Ord Level Source # 
Instance details

Methods

compare :: Level -> Level -> Ordering #

(<) :: Level -> Level -> Bool #

(<=) :: Level -> Level -> Bool #

(>) :: Level -> Level -> Bool #

(>=) :: Level -> Level -> Bool #

max :: Level -> Level -> Level #

min :: Level -> Level -> Level #

Ord PlusLevel Source # 
Instance details

Ord Sort Source # 
Instance details

Methods

compare :: Sort -> Sort -> Ordering #

(<) :: Sort -> Sort -> Bool #

(<=) :: Sort -> Sort -> Bool #

(>) :: Sort -> Sort -> Bool #

(>=) :: Sort -> Sort -> Bool #

max :: Sort -> Sort -> Sort #

min :: Sort -> Sort -> Sort #

Ord Substitution Source # 
Instance details

Ord Term Source # 
Instance details

Methods

compare :: Term -> Term -> Ordering #

(<) :: Term -> Term -> Bool #

(<=) :: Term -> Term -> Bool #

(>) :: Term -> Term -> Bool #

(>=) :: Term -> Term -> Bool #

max :: Term -> Term -> Term #

min :: Term -> Term -> Term #

Abstract a => Abstract (Case a) Source # 
Instance details

Methods

abstract :: Telescope -> Case a -> Case a Source #

Abstract a => Abstract (WithArity a) Source # 
Instance details

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

Abstract [Occurrence] Source # 
Instance details

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

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

Apply [Polarity] Source # 
Instance details

Apply [Occurrence] Source # 
Instance details

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

Methods

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

Subst a => Subst (WithHiding a) Source # 
Instance details

Associated Types

type SubstArg (WithHiding a) Source #

Subst a => Subst (Abs a) Source # 
Instance details

Associated Types

type SubstArg (Abs a) Source #

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

Subst a => Subst (Level' a) Source # 
Instance details

Associated Types

type SubstArg (Level' a) Source #

Subst a => Subst (PlusLevel' a) Source # 
Instance details

Associated Types

type SubstArg (PlusLevel' a) Source #

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

Associated Types

type SubstArg (Sort' a) Source #

EndoSubst a => Subst (Substitution' a) Source # 
Instance details

Associated Types

type SubstArg (Substitution' a) Source #

Subst a => Subst (Tele a) Source # 
Instance details

Associated Types

type SubstArg (Tele a) Source #

Subst a => Subst (Elim' a) Source # 
Instance details

Associated Types

type SubstArg (Elim' a) Source #

Subst a => Subst (Maybe a) Source # 
Instance details

Associated Types

type SubstArg (Maybe a) Source #

Subst a => Subst [a] Source # 
Instance details

Associated Types

type SubstArg [a] Source #

Methods

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

DeBruijn a => DeBruijn (Pattern' a) Source # 
Instance details

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

(/=) :: Abs a -> Abs a -> Bool #

Eq t => Eq (Blocked t) Source # 
Instance details

Methods

(==) :: Blocked t -> Blocked t -> Bool #

(/=) :: Blocked t -> Blocked t -> Bool #

Eq a => Eq (Pattern' a) Source # 
Instance details

Methods

(==) :: Pattern' a -> Pattern' a -> Bool #

(/=) :: Pattern' a -> Pattern' a -> Bool #

(Subst a, Eq a) => Eq (Tele a) Source # 
Instance details

Methods

(==) :: Tele a -> Tele a -> Bool #

(/=) :: Tele a -> Tele a -> Bool #

Eq a => Eq (Type' a) Source #

Syntactic Type equality, ignores sort annotations.

Instance details

Methods

(==) :: Type' a -> Type' a -> Bool #

(/=) :: Type' a -> Type' a -> Bool #

(Subst a, Eq a) => Eq (Elim' a) Source # 
Instance details

Methods

(==) :: Elim' a -> Elim' a -> Bool #

(/=) :: Elim' a -> Elim' a -> Bool #

(Subst a, Ord a) => Ord (Abs a) Source # 
Instance details

Methods

compare :: Abs a -> Abs a -> Ordering #

(<) :: Abs a -> Abs a -> Bool #

(<=) :: Abs a -> Abs a -> Bool #

(>) :: Abs a -> Abs a -> Bool #

(>=) :: Abs a -> Abs a -> Bool #

max :: Abs a -> Abs a -> Abs a #

min :: Abs a -> Abs a -> Abs a #

Ord a => Ord (Dom a) Source # 
Instance details

Methods

compare :: Dom a -> Dom a -> Ordering #

(<) :: Dom a -> Dom a -> Bool #

(<=) :: Dom a -> Dom a -> Bool #

(>) :: Dom a -> Dom a -> Bool #

(>=) :: Dom a -> Dom a -> Bool #

max :: Dom a -> Dom a -> Dom a #

min :: Dom a -> Dom a -> Dom a #

(Subst a, Ord a) => Ord (Tele a) Source # 
Instance details

Methods

compare :: Tele a -> Tele a -> Ordering #

(<) :: Tele a -> Tele a -> Bool #

(<=) :: Tele a -> Tele a -> Bool #

(>) :: Tele a -> Tele a -> Bool #

(>=) :: Tele a -> Tele a -> Bool #

max :: Tele a -> Tele a -> Tele a #

min :: Tele a -> Tele a -> Tele a #

Ord a => Ord (Type' a) Source # 
Instance details

Methods

compare :: Type' a -> Type' a -> Ordering #

(<) :: Type' a -> Type' a -> Bool #

(<=) :: Type' a -> Type' a -> Bool #

(>) :: Type' a -> Type' a -> Bool #

(>=) :: Type' a -> Type' a -> Bool #

max :: Type' a -> Type' a -> Type' a #

min :: Type' a -> Type' a -> Type' a #

(Subst a, Ord a) => Ord (Elim' a) Source # 
Instance details

Methods

compare :: Elim' a -> Elim' a -> Ordering #

(<) :: Elim' a -> Elim' a -> Bool #

(<=) :: Elim' a -> Elim' a -> Bool #

(>) :: Elim' a -> Elim' a -> Bool #

(>=) :: Elim' a -> Elim' a -> Bool #

max :: Elim' a -> Elim' a -> Elim' a #

min :: Elim' a -> Elim' a -> Elim' a #

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

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

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

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

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

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

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

Methods

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