Agda.TypeChecking.Substitute

Application

class Apply t where

Apply something to a bunch of arguments. Preserves blocking tags (application can never resolve blocking).

Methods

apply :: t -> Args -> t

applyE :: t -> Elims -> t

Instances

Apply Permutation

Methods

apply :: Permutation -> Args -> Permutation

applyE :: Permutation -> Elims -> Permutation

Apply ClauseBody

Methods

apply :: ClauseBody -> Args -> ClauseBody

applyE :: ClauseBody -> Elims -> ClauseBody

Apply Clause

Methods

apply :: Clause -> Args -> Clause

applyE :: Clause -> Elims -> Clause

Apply Sort

Methods

apply :: Sort -> Args -> Sort

applyE :: Sort -> Elims -> Sort

Apply Term

Methods

apply :: Term -> Args -> Term

applyE :: Term -> Elims -> Term

Apply CompiledClauses

Methods

apply :: CompiledClauses -> Args -> CompiledClauses

applyE :: CompiledClauses -> Elims -> CompiledClauses

Apply FunctionInverse

Methods

apply :: FunctionInverse -> Args -> FunctionInverse

applyE :: FunctionInverse -> Elims -> FunctionInverse

Apply PrimFun

Methods

apply :: PrimFun -> Args -> PrimFun

applyE :: PrimFun -> Elims -> PrimFun

Apply Defn

Methods

apply :: Defn -> Args -> Defn

applyE :: Defn -> Elims -> Defn

Apply Projection

Methods

apply :: Projection -> Args -> Projection

applyE :: Projection -> Elims -> Projection

Apply Definition

Methods

apply :: Definition -> Args -> Definition

applyE :: Definition -> Elims -> Definition

Apply RewriteRule

Methods

apply :: RewriteRule -> Args -> RewriteRule

applyE :: RewriteRule -> Elims -> RewriteRule

Apply DisplayTerm

Methods

apply :: DisplayTerm -> Args -> DisplayTerm

applyE :: DisplayTerm -> Elims -> DisplayTerm

Apply t => Apply [t]

Methods

apply :: [t] -> Args -> [t]

applyE :: [t] -> Elims -> [t]

Apply [Occurrence]

Methods

apply :: [Occurrence] -> Args -> [Occurrence]

applyE :: [Occurrence] -> Elims -> [Occurrence]

Apply [Polarity]

Methods

apply :: [Polarity] -> Args -> [Polarity]

applyE :: [Polarity] -> Elims -> [Polarity]

Apply t => Apply (Maybe t)

Methods

apply :: Maybe t -> Args -> Maybe t

applyE :: Maybe t -> Elims -> Maybe t

Apply a => Apply (Ptr a)

Methods

apply :: Ptr a -> Args -> Ptr a

applyE :: Ptr a -> Elims -> Ptr a

DoDrop a => Apply (Drop a)

Methods

apply :: Drop a -> Args -> Drop a

applyE :: Drop a -> Elims -> Drop a

Apply t => Apply (Blocked t)

Methods

apply :: Blocked t -> Args -> Blocked t

applyE :: Blocked t -> Elims -> Blocked t

Subst Term a => Apply (Tele a)

Methods

apply :: Tele a -> Args -> Tele a

applyE :: Tele a -> Elims -> Tele a

Apply a => Apply (Case a)

Methods

apply :: Case a -> Args -> Case a

applyE :: Case a -> Elims -> Case a

Apply a => Apply (WithArity a)

Methods

apply :: WithArity a -> Args -> WithArity a

applyE :: WithArity a -> Elims -> WithArity a

(Apply a, Apply b) => Apply (a, b)

Methods

apply :: (a, b) -> Args -> (a, b)

applyE :: (a, b) -> Elims -> (a, b)

Apply v => Apply (Map k v)

Methods

apply :: Map k v -> Args -> Map k v

applyE :: Map k v -> Elims -> Map k v

(Apply a, Apply b, Apply c) => Apply (a, b, c)

Methods

apply :: (a, b, c) -> Args -> (a, b, c)

applyE :: (a, b, c) -> Elims -> (a, b, c)

applys :: Apply t => t -> [Term] -> t

Apply to some default arguments.

apply1 :: Apply t => t -> Term -> t

Apply to a single default argument.

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

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

conApp :: ConHead -> Args -> Elims -> Term

Eliminate a constructed term.

defApp :: QName -> Elims -> Elims -> Term

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

piApply :: Type -> Args -> Type

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

Abstraction

class Abstract t where

(abstract args v) apply args --> v[args].

Minimal complete definition

abstract

Methods

abstract :: Telescope -> t -> t

Instances

Abstract Permutation

Methods

abstract :: Telescope -> Permutation -> Permutation

Abstract ClauseBody

Methods

abstract :: Telescope -> ClauseBody -> ClauseBody

Abstract Clause

Methods

abstract :: Telescope -> Clause -> Clause

Abstract Sort

Methods

abstract :: Telescope -> Sort -> Sort

Abstract Telescope

Methods

abstract :: Telescope -> Telescope -> Telescope

Abstract Type

Methods

abstract :: Telescope -> Type -> Type

Abstract Term

Methods

abstract :: Telescope -> Term -> Term

Abstract CompiledClauses

Methods

abstract :: Telescope -> CompiledClauses -> CompiledClauses

Abstract FunctionInverse

Methods

abstract :: Telescope -> FunctionInverse -> FunctionInverse

Abstract PrimFun

Methods

abstract :: Telescope -> PrimFun -> PrimFun

Abstract Defn

Methods

abstract :: Telescope -> Defn -> Defn

Abstract Projection

Methods

abstract :: Telescope -> Projection -> Projection

Abstract Definition

Methods

abstract :: Telescope -> Definition -> Definition

Abstract RewriteRule

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

Methods

abstract :: Telescope -> RewriteRule -> RewriteRule

Abstract t => Abstract [t]

Methods

abstract :: Telescope -> [t] -> [t]

Abstract [Occurrence]

Methods

abstract :: Telescope -> [Occurrence] -> [Occurrence]

Abstract [Polarity]

Methods

abstract :: Telescope -> [Polarity] -> [Polarity]

Abstract t => Abstract (Maybe t)

Methods

abstract :: Telescope -> Maybe t -> Maybe t

DoDrop a => Abstract (Drop a)

Methods

abstract :: Telescope -> Drop a -> Drop a

Abstract a => Abstract (Case a)

Methods

abstract :: Telescope -> Case a -> Case a

Abstract a => Abstract (WithArity a)

Methods

abstract :: Telescope -> WithArity a -> WithArity a

Abstract v => Abstract (Map k v)

Methods

abstract :: Telescope -> Map k v -> Map k v

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

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

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

Explicit substitutions

class DeBruijn a where

Minimal complete definition

debruijnView

Methods

debruijnVar :: Int -> a

debruijnNamedVar :: String -> Int -> a

debruijnView :: a -> Maybe Int

Instances

DeBruijn Term

Methods

debruijnVar :: Int -> Term

debruijnNamedVar :: String -> Int -> Term

debruijnView :: Term -> Maybe Int

idS :: Substitution' a

wkS :: Int -> Substitution' a -> Substitution' a

raiseS :: Int -> Substitution' a

consS :: DeBruijn a => a -> Substitution' a -> Substitution' a

singletonS :: DeBruijn a => Int -> a -> Substitution' a

To replace index n by term u, do applySubst (singletonS n u).

liftS :: Int -> Substitution' a -> Substitution' a

Lift a substitution under k binders.

dropS :: Int -> Substitution' a -> Substitution' a

composeS :: Subst a a => Substitution' a -> Substitution' a -> Substitution' a

applySubst (ρ composeS σ) v == applySubst ρ (applySubst σ v)

splitS :: Int -> Substitution' a -> (Substitution' a, Substitution' a)

(++#) :: DeBruijn a => [a] -> Substitution' a -> Substitution' a infixr 4

prependS :: DeBruijn a => Empty -> [Maybe a] -> Substitution' a -> Substitution' a

parallelS :: DeBruijn a => [a] -> Substitution' a

compactS :: DeBruijn a => Empty -> [Maybe a] -> Substitution' a

strengthenS :: Empty -> Int -> Substitution' a

Γ ⊢ (strengthenS ⊥ |Δ|) : Γ,Δ

lookupS :: Subst a a => Substitution' a -> Nat -> a

Substitution and raisingshiftingweakening

class DeBruijn t => Subst t a | a -> t where

Apply a substitution.

Minimal complete definition

applySubst

Methods

applySubst :: Substitution' t -> a -> a

Instances

Subst Term ()

Methods

applySubst :: Substitution' Term -> () -> ()

Subst Term String

Methods

applySubst :: Substitution' Term -> String -> String

Subst Term Name

Methods

applySubst :: Substitution' Term -> Name -> Name

Subst Term EqualityView

Methods

applySubst :: Substitution' Term -> EqualityView -> EqualityView

Subst Term ConPatternInfo

Methods

applySubst :: Substitution' Term -> ConPatternInfo -> ConPatternInfo

Subst Term Pattern

Methods

applySubst :: Substitution' Term -> Pattern -> Pattern

Subst Term ClauseBody

Methods

applySubst :: Substitution' Term -> ClauseBody -> ClauseBody

Subst Term LevelAtom

Methods

applySubst :: Substitution' Term -> LevelAtom -> LevelAtom

Subst Term PlusLevel

Methods

applySubst :: Substitution' Term -> PlusLevel -> PlusLevel

Subst Term Level

Methods

applySubst :: Substitution' Term -> Level -> Level

Subst Term Sort

Methods

applySubst :: Substitution' Term -> Sort -> Sort

Subst Term Term

Methods

applySubst :: Substitution' Term -> Term -> Term

Subst Term Candidate

Methods

applySubst :: Substitution' Term -> Candidate -> Candidate

Subst Term RewriteRule

Methods

applySubst :: Substitution' Term -> RewriteRule -> RewriteRule

Subst Term NLPat

Methods

applySubst :: Substitution' Term -> NLPat -> NLPat

Subst Term DisplayTerm

Methods

applySubst :: Substitution' Term -> DisplayTerm -> DisplayTerm

Subst Term DisplayForm

Methods

applySubst :: Substitution' Term -> DisplayForm -> DisplayForm

Subst Term Constraint

Methods

applySubst :: Substitution' Term -> Constraint -> Constraint

Subst Term AsBinding

Methods

applySubst :: Substitution' Term -> AsBinding -> AsBinding

Subst Term DotPatternInst

Methods

applySubst :: Substitution' Term -> DotPatternInst -> DotPatternInst

Subst Term ProblemRest

Methods

applySubst :: Substitution' Term -> ProblemRest -> ProblemRest

Subst Term SizeConstraint

Methods

applySubst :: Substitution' Term -> SizeConstraint -> SizeConstraint

Subst Term SizeMeta

Methods

applySubst :: Substitution' Term -> SizeMeta -> SizeMeta

Subst t a => Subst t [a]

Methods

applySubst :: Substitution' t -> [a] -> [a]

Subst t a => Subst t (Maybe a)

Methods

applySubst :: Substitution' t -> Maybe a -> Maybe a

Subst t a => Subst t (Dom a)

Methods

applySubst :: Substitution' t -> Dom a -> Dom a

Subst t a => Subst t (Arg a)

Methods

applySubst :: Substitution' t -> Arg a -> Arg a

Subst t a => Subst t (Abs a)

Methods

applySubst :: Substitution' t -> Abs a -> Abs a

Subst t a => Subst t (Elim' a)

Methods

applySubst :: Substitution' t -> Elim' a -> Elim' a

Subst t a => Subst t (Tele a)

Methods

applySubst :: Substitution' t -> Tele a -> Tele a

Subst t a => Subst t (Blocked a)

Methods

applySubst :: Substitution' t -> Blocked a -> Blocked a

Subst t a => Subst t (Ptr a)

Methods

applySubst :: Substitution' t -> Ptr a -> Ptr a

Subst a a => Subst a (Substitution' a)

Methods

applySubst :: Substitution' a -> Substitution' a -> Substitution' a

Subst Term a => Subst Term (Type' a)

Methods

applySubst :: Substitution' Term -> Type' a -> Type' a

Subst Term (Problem' p)

Methods

applySubst :: Substitution' Term -> Problem' p -> Problem' p

(Subst t a, Subst t b) => Subst t (a, b)

Methods

applySubst :: Substitution' t -> (a, b) -> (a, b)

Subst t a => Subst t (Named name a)

Methods

applySubst :: Substitution' t -> Named name a -> Named name a

Subst Term (SizeExpr' NamedRigid SizeMeta)

Only for raise.

Methods

applySubst :: Substitution' Term -> SizeExpr' NamedRigid SizeMeta -> SizeExpr' NamedRigid SizeMeta

(Subst t a, Subst t b, Subst t c) => Subst t (a, b, c)

Methods

applySubst :: Substitution' t -> (a, b, c) -> (a, b, c)

(Subst t a, Subst t b, Subst t c, Subst t d) => Subst t (a, b, c, d)

Methods

applySubst :: Substitution' t -> (a, b, c, d) -> (a, b, c, d)

raise :: Subst t a => Nat -> a -> a

raiseFrom :: Subst t a => Nat -> Nat -> a -> a

subst :: Subst t a => Int -> t -> a -> a

Replace de Bruijn index i by a Term in something.

strengthen :: Subst t a => Empty -> a -> a

substUnder :: Subst t a => Nat -> t -> a -> a

Replace what is now de Bruijn index 0, but go under n binders. substUnder n u == subst n (raise n u).

Telescopes

type TelView = TelV Type

data TelV a

Constructors

TelV

Fields

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

Instances

Functor TelV

Methods

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

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

(Subst t a, Eq a) => Eq (TelV a)

Methods

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

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

(Subst t a, Ord a) => Ord (TelV a)

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

Show a => Show (TelV a)

Methods

showsPrec :: Int -> TelV a -> ShowS

show :: TelV a -> String

showList :: [TelV a] -> ShowS

type ListTel' a = [Dom (a, Type)]

type ListTel = ListTel' ArgName

telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope

telFromList :: ListTel -> Telescope

telToList :: Telescope -> ListTel

telToArgs :: Telescope -> [Arg ArgName]

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

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

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

bindsWithHidingToTel' :: (Name -> a) -> [WithHiding Name] -> Dom Type -> ListTel' a

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

bindsWithHidingToTel :: [WithHiding Name] -> Dom Type -> ListTel

telView' :: Type -> TelView

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

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

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

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

mkLam :: Arg ArgName -> Term -> Term

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

telePi :: Telescope -> Type -> Type

Uses free variable analysis to introduce noAbs bindings.

telePi_ :: Telescope -> Type -> Type

Everything will be a Abs.

teleLam :: Telescope -> Term -> Term

class TeleNoAbs a where

Performs void (noAbs) abstraction over telescope.

Minimal complete definition

teleNoAbs

Methods

teleNoAbs :: a -> Term -> Term

Instances

TeleNoAbs Telescope

Methods

teleNoAbs :: Telescope -> Term -> Term

TeleNoAbs ListTel

Methods

teleNoAbs :: ListTel -> Term -> Term

dLub :: Sort -> Abs Sort -> Sort

Dependent least upper bound, to assign a level to expressions like forall i -> Set i.

dLub s1 i.s2 = omega if i appears in the rigid variables of s2.

Functions on abstractions

absApp :: Subst t a => Abs a -> t -> a

Instantiate an abstraction. Strict in the term.

lazyAbsApp :: Subst t a => Abs a -> t -> a

Instantiate an abstraction. Lazy in the term, which allow it to be IMPOSSIBLE in the case where the variable shouldn't be used but we cannot use noabsApp. Used in Apply.

noabsApp :: Subst t a => Empty -> Abs a -> a

Instantiate an abstraction that doesn't use its argument.

absBody :: Subst t a => Abs a -> a

mkAbs :: (Subst t a, Free a) => ArgName -> a -> Abs a

reAbs :: (Subst t a, Free a) => Abs a -> Abs a

underAbs :: Subst t a => (a -> b -> b) -> a -> Abs b -> Abs b

underAbs k a b applies k to a and the content of abstraction b and puts the abstraction back. a is raised if abstraction was proper such that at point of application of k and the content of b are at the same context. Precondition: a and b are at the same context at call time.

underLambdas :: Subst Term a => Int -> (a -> Term -> Term) -> a -> Term -> Term

underLambdas n k a b drops n initial Lams from b, performs operation k on a and the body of b, and puts the Lams back. a is raised correctly according to the number of abstractions.

class GetBody a where

Methods to retrieve the clauseBody.

Minimal complete definition

getBody, getBodyUnraised

Methods

getBody :: a -> Maybe Term

Returns the properly raised clause Body, and Nothing if NoBody.

getBodyUnraised :: a -> Maybe Term

Just grabs the body, without raising the de Bruijn indices. This is useful if you want to consider the body in context clauseTel.

Instances

GetBody ClauseBody

Methods

getBody :: ClauseBody -> Maybe Term

getBodyUnraised :: ClauseBody -> Maybe Term

GetBody Clause

Methods

getBody :: Clause -> Maybe Term

getBodyUnraised :: Clause -> Maybe Term

Syntactic equality and order

Level stuff

pts :: Sort -> Sort -> Sort

The `rule', if Agda is considered as a functional pure type system (pts).

TODO: This needs to be properly implemented, requiring refactoring of Agda's handling of levels. Without impredicativity or SizeUniv, Agda's pts rule is just the least upper bound, which is total and commutative. The handling of levels relies on this simplification.

sLub :: Sort -> Sort -> Sort

lvlView :: Term -> Level

levelMax :: [PlusLevel] -> Level

sortTm :: Sort -> Term

levelSort :: Level -> Sort

levelTm :: Level -> Term

unLevelAtom :: LevelAtom -> Term

data Substitution' a

Substitutions.

Constructors

IdS

Identity substitution. Γ ⊢ IdS : Γ

EmptyS

Empty substitution, lifts from the empty context. 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 IMPOSSIBLE. 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'

Methods

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

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

Foldable Substitution'

Methods

fold :: Monoid m => Substitution' m -> 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'

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)

Pretty Substitution

Methods

pretty :: Substitution -> Doc

prettyPrec :: Int -> Substitution -> Doc

KillRange Substitution

Methods

killRange :: KillRangeT Substitution

InstantiateFull Substitution

Methods

instantiateFull' :: Substitution -> ReduceM Substitution

Subst a a => Subst a (Substitution' a)

Methods

applySubst :: Substitution' a -> Substitution' a -> Substitution' a

Show a => Show (Substitution' a)

Methods

showsPrec :: Int -> Substitution' a -> ShowS

show :: Substitution' a -> String

showList :: [Substitution' a] -> ShowS

TermSize a => TermSize (Substitution' a)

Methods

termSize :: Substitution' a -> Int

tsize :: Substitution' a -> Sum Int

(Show a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a)

Methods

prettyTCM :: Substitution' a -> TCM Doc

type Substitution = Substitution' Term

Orphan instances

Eq NotBlocked

Methods

(==) :: NotBlocked -> NotBlocked -> Bool

(/=) :: NotBlocked -> NotBlocked -> Bool

Eq LevelAtom

Methods

(==) :: LevelAtom -> LevelAtom -> Bool

(/=) :: LevelAtom -> LevelAtom -> Bool

Eq PlusLevel

Methods

(==) :: PlusLevel -> PlusLevel -> Bool

(/=) :: PlusLevel -> PlusLevel -> Bool

Eq Level

Methods

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

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

Eq Sort

Methods

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

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

Eq Term

Syntactic Term equality, ignores stuff below DontCare and sharing.

Methods

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

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

Eq Candidate

Methods

(==) :: Candidate -> Candidate -> Bool

(/=) :: Candidate -> Candidate -> Bool

Eq Section

Methods

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

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

Eq Constraint

Methods

(==) :: Constraint -> Constraint -> Bool

(/=) :: Constraint -> Constraint -> Bool

Ord NotBlocked

Methods

compare :: NotBlocked -> NotBlocked -> Ordering

(<) :: NotBlocked -> NotBlocked -> Bool

(<=) :: NotBlocked -> NotBlocked -> Bool

(>) :: NotBlocked -> NotBlocked -> Bool

(>=) :: NotBlocked -> NotBlocked -> Bool

max :: NotBlocked -> NotBlocked -> NotBlocked

min :: NotBlocked -> NotBlocked -> NotBlocked

Ord LevelAtom

Methods

compare :: LevelAtom -> LevelAtom -> Ordering

(<) :: LevelAtom -> LevelAtom -> Bool

(<=) :: LevelAtom -> LevelAtom -> Bool

(>) :: LevelAtom -> LevelAtom -> Bool

(>=) :: LevelAtom -> LevelAtom -> Bool

max :: LevelAtom -> LevelAtom -> LevelAtom

min :: LevelAtom -> LevelAtom -> LevelAtom

Ord PlusLevel

Methods

compare :: PlusLevel -> PlusLevel -> Ordering

(<) :: PlusLevel -> PlusLevel -> Bool

(<=) :: PlusLevel -> PlusLevel -> Bool

(>) :: PlusLevel -> PlusLevel -> Bool

(>=) :: PlusLevel -> PlusLevel -> Bool

max :: PlusLevel -> PlusLevel -> PlusLevel

min :: PlusLevel -> PlusLevel -> PlusLevel

Ord Level

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 Sort

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 Term

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

Eq (Substitution' Term)

Methods

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

(/=) :: Substitution' Term -> Substitution' Term -> Bool

Eq t => Eq (Blocked t)

Methods

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

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

(Subst t a, Eq a) => Eq (Tele a)

Methods

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

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

Eq a => Eq (Type' a)

Syntactic Type equality, ignores sort annotations.

Methods

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

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

(Subst t a, Eq a) => Eq (Abs a)

Methods

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

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

(Subst t a, Eq a) => Eq (Elim' a)

Methods

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

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

Ord (Substitution' Term)

Methods

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

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

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

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

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

max :: Substitution' Term -> Substitution' Term -> Substitution' Term

min :: Substitution' Term -> Substitution' Term -> Substitution' Term

Ord t => Ord (Blocked t)

Methods

compare :: Blocked t -> Blocked t -> Ordering

(<) :: Blocked t -> Blocked t -> Bool

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

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

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

max :: Blocked t -> Blocked t -> Blocked t

min :: Blocked t -> Blocked t -> Blocked t

(Subst t a, Ord a) => Ord (Tele a)

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)

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 t a, Ord a) => Ord (Abs a)

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

(Subst t a, Ord a) => Ord (Elim' a)

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