Agda.Syntax.Internal

Documentation

class TermSize a where

The size of a term is roughly the number of nodes in its syntax tree. This number need not be precise for logical correctness of Agda, it is only used for reporting (and maybe decisions regarding performance).

Not counting towards the term size are:

• sort and color annotations,
• projections.

Minimal complete definition

tsize

Methods

termSize :: a -> Int

tsize :: a -> Sum Int

Instances

TermSize LevelAtom

Defined in Agda.Syntax.Internal

Methods

termSize :: LevelAtom -> Int

tsize :: LevelAtom -> Sum Int

TermSize PlusLevel

Defined in Agda.Syntax.Internal

Methods

termSize :: PlusLevel -> Int

tsize :: PlusLevel -> Sum Int

TermSize Level

Defined in Agda.Syntax.Internal

Methods

termSize :: Level -> Int

tsize :: Level -> Sum Int

TermSize Sort

Defined in Agda.Syntax.Internal

Methods

termSize :: Sort -> Int

tsize :: Sort -> Sum Int

TermSize Term

Defined in Agda.Syntax.Internal

Methods

termSize :: Term -> Int

tsize :: Term -> Sum Int

(Foldable t, TermSize a) => TermSize (t a)

Defined in Agda.Syntax.Internal

Methods

termSize :: t a -> Int

tsize :: t a -> Sum Int

TermSize a => TermSize (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

termSize :: Substitution' a -> Int

tsize :: Substitution' a -> Sum Int

class IsProjElim e where

Minimal complete definition

isProjElim

Methods

isProjElim :: e -> Maybe (ProjOrigin, QName)

Instances

IsProjElim Elim

Defined in Agda.Syntax.Internal

Methods

isProjElim :: Elim -> Maybe (ProjOrigin, QName)

IsProjElim e => IsProjElim (MaybeReduced e)

Defined in Agda.TypeChecking.Monad.Base

Methods

isProjElim :: MaybeReduced e -> Maybe (ProjOrigin, QName)

class Suggest a b where

Pick the better name suggestion, i.e., the one that is not just underscore.

Minimal complete definition

suggest

Methods

suggest :: a -> b -> String

Instances

Suggest String String

Defined in Agda.Syntax.Internal

Methods

suggest :: String -> String -> String

Suggest String (Abs b)

Defined in Agda.Syntax.Internal

Methods

suggest :: String -> Abs b -> String

Suggest Name (Abs b)

Defined in Agda.Syntax.Internal

Methods

suggest :: Name -> Abs b -> String

Suggest (Abs a) (Abs b)

Defined in Agda.Syntax.Internal

Methods

suggest :: Abs a -> Abs b -> String

class SgTel a where

Constructing a singleton telescope.

Minimal complete definition

sgTel

Methods

sgTel :: a -> Telescope

Instances

SgTel (Dom (ArgName, Type))

Defined in Agda.Syntax.Internal

Methods

sgTel :: Dom (ArgName, Type) -> Telescope

SgTel (Dom Type)

Defined in Agda.Syntax.Internal

Methods

sgTel :: Dom Type -> Telescope

SgTel (ArgName, Dom Type)

Defined in Agda.Syntax.Internal

Methods

sgTel :: (ArgName, Dom Type) -> Telescope

class TelToArgs a where

Drop the types from a telescope.

Minimal complete definition

telToArgs

Methods

telToArgs :: a -> [Arg ArgName]

Instances

TelToArgs ListTel

Defined in Agda.Syntax.Internal

Methods

telToArgs :: ListTel -> [Arg ArgName]

TelToArgs Telescope

Defined in Agda.Syntax.Internal

Methods

telToArgs :: Telescope -> [Arg ArgName]

type ListTel = ListTel' ArgName

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

Telescope as list.

data EqualityView

View type as equality type.

Constructors

EqualityType

Fields

• eqtSort :: Sort

  Sort of this type.

• eqtName :: QName

  Builtin EQUALITY.

• eqtParams :: [Arg Term]

  Hidden. Empty or Level.

• eqtType :: Arg Term

  Hidden

• eqtLhs :: Arg Term

  NotHidden

• eqtRhs :: Arg Term

  NotHidden

OtherType Type

reduced

Instances

Free EqualityView

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => EqualityView -> FreeM c

TermLike EqualityView

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> EqualityView -> m EqualityView

foldTerm :: Monoid m => (Term -> m) -> EqualityView -> m

PrettyTCM EqualityView

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: EqualityView -> TCM Doc

InstantiateFull EqualityView

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: EqualityView -> ReduceM EqualityView

Normalise EqualityView

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: EqualityView -> ReduceM EqualityView

Simplify EqualityView

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: EqualityView -> ReduceM EqualityView

Reduce EqualityView

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: EqualityView -> ReduceM EqualityView

reduceB' :: EqualityView -> ReduceM (Blocked EqualityView)

Instantiate EqualityView

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: EqualityView -> ReduceM EqualityView

Subst Term EqualityView

Defined in Agda.TypeChecking.Substitute

Methods

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

type PatternSubstitution = Substitution' DeBruijnPattern

type Substitution = Substitution' Term

data Substitution' a

Substitutions.

Constructors

IdS

Identity substitution. Γ ⊢ IdS : Γ

EmptyS Empty

Empty substitution, lifts from the empty context. First argument is (throwImpossible (Impossible "srcfullAgdaSyntaxInternal.hs" 572)). Apply this to closed terms you want to use in a non-empty context. Γ ⊢ EmptyS : ()

a :# (Substitution' a) infixr 4

Substitution extension, `cons'. Γ ⊢ u : Aρ Γ ⊢ ρ : Δ ---------------------- Γ ⊢ u :# ρ : Δ, A

Strengthen Empty (Substitution' a)

Strengthening substitution. First argument is (throwImpossible (Impossible "srcfullAgdaSyntaxInternal.hs" 585)). 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'

Defined in Agda.Syntax.Internal

Methods

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

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

Foldable Substitution'

Defined in Agda.Syntax.Internal

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'

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)

KillRange Substitution

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Substitution

InstantiateFull Substitution

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Substitution -> ReduceM Substitution

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

Defined in Agda.TypeChecking.Substitute

Methods

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

Eq (Substitution' Term)

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Data a => Data (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

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

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

toConstr :: Substitution' a -> Constr

dataTypeOf :: Substitution' a -> DataType

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

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

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

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

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

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

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

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

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

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

Ord (Substitution' Term)

Defined in Agda.TypeChecking.Substitute

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

Show a => Show (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

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

show :: Substitution' a -> String

showList :: [Substitution' a] -> ShowS

Null (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

empty :: Substitution' a

null :: Substitution' a -> Bool

Pretty a => Pretty (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

pretty :: Substitution' a -> Doc

prettyPrec :: Int -> Substitution' a -> Doc

prettyList :: [Substitution' a] -> Doc

TermSize a => TermSize (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

termSize :: Substitution' a -> Int

tsize :: Substitution' a -> Sum Int

EmbPrj a => EmbPrj (Substitution' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Substitution' a -> S Int32

icod_ :: Substitution' a -> S Int32

value :: Int32 -> R (Substitution' a)

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

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Substitution' a -> TCM Doc

class PatternVars a b | b -> a where

Extract pattern variables in left-to-right order. A DotP is also treated as variable (see docu for Clause).

Minimal complete definition

patternVars

Methods

patternVars :: b -> [Arg (Either a Term)]

Instances

PatternVars a b => PatternVars a [b]

Defined in Agda.Syntax.Internal

Methods

patternVars :: [b] -> [Arg (Either a Term)]

PatternVars a (NamedArg (Pattern' a))

Defined in Agda.Syntax.Internal

Methods

patternVars :: NamedArg (Pattern' a) -> [Arg (Either a Term)]

PatternVars a (Arg (Pattern' a))

Defined in Agda.Syntax.Internal

Methods

patternVars :: Arg (Pattern' a) -> [Arg (Either a Term)]

data ConPatternInfo

The ConPatternInfo states whether the constructor belongs to a record type (Just) or data type (Nothing). In the former case, the PatOrigin says whether the record pattern orginates from the expansion of an implicit pattern. The Type is the type of the whole record pattern. The scope used for the type is given by any outer scope plus the clause's telescope (clauseTel).

Constructors

ConPatternInfo

Fields

• conPRecord :: Maybe PatOrigin

  Nothing if data constructor. Just if record constructor.

• conPType :: Maybe (Arg Type)

  The type of the whole constructor pattern. Should be present (Just) if constructor pattern is is generated ordinarily by type-checking. Could be absent (Nothing) if pattern comes from some plugin (like Agsy). Needed e.g. for with-clause stripping.

• conPLazy :: Bool

  Lazy patterns are generated by the forcing translation (forcingTranslation) and are dropped by the clause compiler (TODO: not yet) (compileClauses) when the variables they bind are unused. The GHC backend compiles lazy matches to lazy patterns in Haskell (TODO: not yet).

Instances

Data ConPatternInfo

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConPatternInfo -> c ConPatternInfo

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConPatternInfo

toConstr :: ConPatternInfo -> Constr

dataTypeOf :: ConPatternInfo -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConPatternInfo)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConPatternInfo)

gmapT :: (forall b. Data b => b -> b) -> ConPatternInfo -> ConPatternInfo

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConPatternInfo -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConPatternInfo -> r

gmapQ :: (forall d. Data d => d -> u) -> ConPatternInfo -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ConPatternInfo -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConPatternInfo -> m ConPatternInfo

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConPatternInfo -> m ConPatternInfo

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConPatternInfo -> m ConPatternInfo

Show ConPatternInfo

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> ConPatternInfo -> ShowS

show :: ConPatternInfo -> String

showList :: [ConPatternInfo] -> ShowS

KillRange ConPatternInfo

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT ConPatternInfo

EmbPrj ConPatternInfo

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ConPatternInfo -> S Int32

icod_ :: ConPatternInfo -> S Int32

value :: Int32 -> R ConPatternInfo

InstantiateFull ConPatternInfo

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: ConPatternInfo -> ReduceM ConPatternInfo

Normalise ConPatternInfo

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: ConPatternInfo -> ReduceM ConPatternInfo

Subst Term ConPatternInfo

Defined in Agda.TypeChecking.Substitute

Methods

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

type DeBruijnPattern = Pattern' DBPatVar

data DBPatVar

Type used when numbering pattern variables.

Constructors

DBPatVar

Fields

• dbPatVarName :: PatVarName
• dbPatVarIndex :: Int

Instances

Eq DBPatVar

Defined in Agda.Syntax.Internal

Methods

(==) :: DBPatVar -> DBPatVar -> Bool

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

Data DBPatVar

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DBPatVar -> c DBPatVar

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DBPatVar

toConstr :: DBPatVar -> Constr

dataTypeOf :: DBPatVar -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DBPatVar)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DBPatVar)

gmapT :: (forall b. Data b => b -> b) -> DBPatVar -> DBPatVar

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DBPatVar -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DBPatVar -> r

gmapQ :: (forall d. Data d => d -> u) -> DBPatVar -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> DBPatVar -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DBPatVar -> m DBPatVar

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DBPatVar -> m DBPatVar

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DBPatVar -> m DBPatVar

Show DBPatVar

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> DBPatVar -> ShowS

show :: DBPatVar -> String

showList :: [DBPatVar] -> ShowS

Pretty DBPatVar

Defined in Agda.Syntax.Internal

Methods

pretty :: DBPatVar -> Doc

prettyPrec :: Int -> DBPatVar -> Doc

prettyList :: [DBPatVar] -> Doc

KillRange DBPatVar

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT DBPatVar

DeBruijn DeBruijnPattern

Defined in Agda.TypeChecking.Substitute

Methods

deBruijnVar :: Int -> DeBruijnPattern

debruijnNamedVar :: String -> Int -> DeBruijnPattern

deBruijnView :: DeBruijnPattern -> Maybe Int

EmbPrj DBPatVar

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DBPatVar -> S Int32

icod_ :: DBPatVar -> S Int32

value :: Int32 -> R DBPatVar

PrettyTCM DBPatVar

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: DBPatVar -> TCM Doc

InstantiateFull DBPatVar

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: DBPatVar -> ReduceM DBPatVar

Normalise DBPatVar

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: DBPatVar -> ReduceM DBPatVar

UsableSizeVars DeBruijnPattern

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: DeBruijnPattern -> TerM VarSet

UsableSizeVars MaskedDeBruijnPatterns

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: MaskedDeBruijnPatterns -> TerM VarSet

Subst DeBruijnPattern DeBruijnPattern

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' DeBruijnPattern -> DeBruijnPattern -> DeBruijnPattern

LabelPatVars Pattern DeBruijnPattern Int

Defined in Agda.Syntax.Internal.Pattern

Methods

labelPatVars :: Pattern -> State [Int] DeBruijnPattern

unlabelPatVars :: DeBruijnPattern -> Pattern

UsableSizeVars [DeBruijnPattern]

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: [DeBruijnPattern] -> TerM VarSet

UsableSizeVars (Masked DeBruijnPattern)

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet

type Pattern

Arguments

 = Pattern' PatVarName

The PatVarName is a name suggestion.

data Pattern' x

Patterns are variables, constructors, or wildcards. QName is used in ConP rather than Name since a constructor might come from a particular namespace. This also meshes well with the fact that values (i.e. the arguments we are matching with) use QName.

Constructors

VarP PatOrigin x

x

DotP PatOrigin Term

.t

ConP ConHead ConPatternInfo [NamedArg (Pattern' x)]

c ps The subpatterns do not contain any projection copatterns.

LitP Literal

E.g. 5, "hello".

ProjP ProjOrigin QName

Projection copattern. Can only appear by itself.

Instances

Functor Pattern'

Defined in Agda.Syntax.Internal

Methods

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

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

Foldable Pattern'

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => Pattern' m -> m

foldMap :: Monoid m => (a -> m) -> Pattern' a -> m

foldr :: (a -> b -> b) -> b -> Pattern' a -> b

foldr' :: (a -> b -> b) -> b -> Pattern' a -> b

foldl :: (b -> a -> b) -> b -> Pattern' a -> b

foldl' :: (b -> a -> b) -> b -> Pattern' a -> b

foldr1 :: (a -> a -> a) -> Pattern' a -> a

foldl1 :: (a -> a -> a) -> Pattern' a -> a

toList :: Pattern' a -> [a]

null :: Pattern' a -> Bool

length :: Pattern' a -> Int

elem :: Eq a => a -> Pattern' a -> Bool

maximum :: Ord a => Pattern' a -> a

minimum :: Ord a => Pattern' a -> a

sum :: Num a => Pattern' a -> a

product :: Num a => Pattern' a -> a

Traversable Pattern'

Defined in Agda.Syntax.Internal

Methods

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

sequenceA :: Applicative f => Pattern' (f a) -> f (Pattern' a)

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

sequence :: Monad m => Pattern' (m a) -> m (Pattern' a)

DeBruijn DeBruijnPattern

Defined in Agda.TypeChecking.Substitute

Methods

deBruijnVar :: Int -> DeBruijnPattern

debruijnNamedVar :: String -> Int -> DeBruijnPattern

deBruijnView :: DeBruijnPattern -> Maybe Int

DeBruijn SplitPattern

Defined in Agda.TypeChecking.Coverage.Match

Methods

deBruijnVar :: Int -> SplitPattern

debruijnNamedVar :: String -> Int -> SplitPattern

deBruijnView :: SplitPattern -> Maybe Int

UsableSizeVars DeBruijnPattern

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: DeBruijnPattern -> TerM VarSet

UsableSizeVars MaskedDeBruijnPatterns

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: MaskedDeBruijnPatterns -> TerM VarSet

UniverseBi Elims Pattern

Defined in Agda.Syntax.Internal

Methods

universeBi :: Elims -> [Pattern]

UniverseBi Args Pattern

Defined in Agda.Syntax.Internal

Methods

universeBi :: Args -> [Pattern]

Subst DeBruijnPattern DeBruijnPattern

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' DeBruijnPattern -> DeBruijnPattern -> DeBruijnPattern

Subst Term Pattern

Defined in Agda.TypeChecking.Substitute

Methods

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

Subst SplitPattern SplitPattern

Defined in Agda.TypeChecking.Coverage.Match

Methods

applySubst :: Substitution' SplitPattern -> SplitPattern -> SplitPattern

LabelPatVars Pattern DeBruijnPattern Int

Defined in Agda.Syntax.Internal.Pattern

Methods

labelPatVars :: Pattern -> State [Int] DeBruijnPattern

unlabelPatVars :: DeBruijnPattern -> Pattern

PatternVars a (NamedArg (Pattern' a))

Defined in Agda.Syntax.Internal

Methods

patternVars :: NamedArg (Pattern' a) -> [Arg (Either a Term)]

PatternVars a (Arg (Pattern' a))

Defined in Agda.Syntax.Internal

Methods

patternVars :: Arg (Pattern' a) -> [Arg (Either a Term)]

PatternLike a (Pattern' a)

Defined in Agda.Syntax.Internal.Pattern

Methods

foldrPattern :: Monoid m => (Pattern' a -> m -> m) -> Pattern' a -> m

traversePatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)

MapNamedArgPattern a (NamedArg (Pattern' a))

Modify the content of VarP, and the closest surrounding NamedArg.

Note: the mapNamedArg for Pattern' is not expressible simply by fmap or traverse etc., since ConP has NamedArg subpatterns, which are taken into account by mapNamedArg.

Defined in Agda.Syntax.Internal.Pattern

Methods

mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)

DeBruijn (Pattern' a) => TermToPattern Term (Pattern' a)

Defined in Agda.TypeChecking.Patterns.Internal

Methods

termToPattern :: Term -> TCM (Pattern' a)

Conversion TOM (Arg Pattern) (Pat O)

Defined in Agda.Auto.Convert

Methods

convert :: Arg Pattern -> TOM (Pat O)

Data x => Data (Pattern' x)

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pattern' x -> c (Pattern' x)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Pattern' x)

toConstr :: Pattern' x -> Constr

dataTypeOf :: Pattern' x -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Pattern' x))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Pattern' x))

gmapT :: (forall b. Data b => b -> b) -> Pattern' x -> Pattern' x

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pattern' x -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pattern' x -> r

gmapQ :: (forall d. Data d => d -> u) -> Pattern' x -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Pattern' x -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pattern' x -> m (Pattern' x)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern' x -> m (Pattern' x)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern' x -> m (Pattern' x)

Show x => Show (Pattern' x)

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Pattern' x -> ShowS

show :: Pattern' x -> String

showList :: [Pattern' x] -> ShowS

Pretty a => Pretty (Pattern' a)

Defined in Agda.Syntax.Internal

Methods

pretty :: Pattern' a -> Doc

prettyPrec :: Int -> Pattern' a -> Doc

prettyList :: [Pattern' a] -> Doc

KillRange a => KillRange (Pattern' a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Pattern' a)

IsProjP (Pattern' a)

Defined in Agda.Syntax.Internal

Methods

isProjP :: Pattern' a -> Maybe (ProjOrigin, AmbiguousQName)

Apply [NamedArg (Pattern' a)]

Make sure we only drop variable patterns.

Defined in Agda.TypeChecking.Substitute

Methods

apply :: [NamedArg (Pattern' a)] -> Args -> [NamedArg (Pattern' a)]

applyE :: [NamedArg (Pattern' a)] -> Elims -> [NamedArg (Pattern' a)]

CountPatternVars (Pattern' x)

Defined in Agda.Syntax.Internal.Pattern

Methods

countPatternVars :: Pattern' x -> Int

EmbPrj a => EmbPrj (Pattern' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Pattern' a -> S Int32

icod_ :: Pattern' a -> S Int32

value :: Int32 -> R (Pattern' a)

PrettyTCM a => PrettyTCM (Pattern' a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Pattern' a -> TCM Doc

NamesIn (Pattern' a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Pattern' a -> Set QName

InstantiateFull a => InstantiateFull (Pattern' a)

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Pattern' a -> ReduceM (Pattern' a)

Normalise a => Normalise (Pattern' a)

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Pattern' a -> ReduceM (Pattern' a)

NormaliseProjP (Pattern' x)

Defined in Agda.TypeChecking.Records

Methods

normaliseProjP :: HasConstInfo m => Pattern' x -> m (Pattern' x)

IsFlexiblePattern (Pattern' a)

Defined in Agda.TypeChecking.Rules.LHS

Methods

maybeFlexiblePattern :: Pattern' a -> MaybeT TCM FlexibleVarKind

isFlexiblePattern :: Pattern' a -> TCM Bool

UsableSizeVars [DeBruijnPattern]

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: [DeBruijnPattern] -> TerM VarSet

UsableSizeVars (Masked DeBruijnPattern)

Defined in Agda.Termination.Monad

Methods

usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet

PatternVarModalities (Pattern' x) x

Defined in Agda.Syntax.Internal.Pattern

Methods

patternVarModalities :: Pattern' x -> [(x, Modality)]

UniverseBi ([Type], [Clause]) Pattern

Defined in Agda.Syntax.Internal

Methods

universeBi :: ([Type], [Clause]) -> [Pattern]

data PatOrigin

Origin of the pattern: what did the user write in this position?

Constructors

PatOSystem

Pattern inserted by the system

PatOSplit

Pattern generated by case split

PatOVar Name

User wrote a variable pattern

PatODot

User wrote a dot pattern

PatOWild

User wrote a wildcard pattern

PatOCon

User wrote a constructor pattern

PatORec

User wrote a record pattern

PatOLit

User wrote a literal pattern

PatOAbsurd

User wrote an absurd pattern

Instances

Eq PatOrigin

Defined in Agda.Syntax.Internal

Methods

(==) :: PatOrigin -> PatOrigin -> Bool

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

Data PatOrigin

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PatOrigin -> c PatOrigin

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PatOrigin

toConstr :: PatOrigin -> Constr

dataTypeOf :: PatOrigin -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PatOrigin)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PatOrigin)

gmapT :: (forall b. Data b => b -> b) -> PatOrigin -> PatOrigin

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PatOrigin -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PatOrigin -> r

gmapQ :: (forall d. Data d => d -> u) -> PatOrigin -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> PatOrigin -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PatOrigin -> m PatOrigin

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PatOrigin -> m PatOrigin

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PatOrigin -> m PatOrigin

Show PatOrigin

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> PatOrigin -> ShowS

show :: PatOrigin -> String

showList :: [PatOrigin] -> ShowS

KillRange PatOrigin

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT PatOrigin

EmbPrj PatOrigin

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: PatOrigin -> S Int32

icod_ :: PatOrigin -> S Int32

value :: Int32 -> R PatOrigin

type PatVarName = ArgName

Pattern variables.

data Clause

A clause is a list of patterns and the clause body.

The telescope contains the types of the pattern variables and the de Bruijn indices say how to get from the order the variables occur in the patterns to the order they occur in the telescope. The body binds the variables in the order they appear in the telescope.

clauseTel ~ permute clausePerm (patternVars namedClausePats)

Terms in dot patterns are valid in the clause telescope.

For the purpose of the permutation and the body dot patterns count as variables. TODO: Change this!

Constructors

Clause

Fields

• clauseLHSRange :: Range
• clauseFullRange :: Range
• clauseTel :: Telescope

  Δ: The types of the pattern variables in dependency order.

• namedClausePats :: [NamedArg DeBruijnPattern]

  Δ ⊢ ps. The de Bruijn indices refer to Δ.

• clauseBody :: Maybe Term

  Just v with Δ ⊢ v for a regular clause, or Nothing for an absurd one.

• clauseType :: Maybe (Arg Type)

  Δ ⊢ t. The type of the rhs under clauseTel. Used, e.g., by TermCheck. Can be Irrelevant if we encountered an irrelevant projection pattern on the lhs.

• clauseCatchall :: Bool

  Clause has been labelled as CATCHALL.

• clauseUnreachable :: Maybe Bool

  Clause has been labelled as unreachable by the coverage checker. Nothing means coverage checker has not run yet (clause may be unreachable). Just False means clause is not unreachable. Just True means clause is unreachable.

Instances

Data Clause

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Clause -> c Clause

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Clause

toConstr :: Clause -> Constr

dataTypeOf :: Clause -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Clause)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Clause)

gmapT :: (forall b. Data b => b -> b) -> Clause -> Clause

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r

gmapQ :: (forall d. Data d => d -> u) -> Clause -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Clause -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Clause -> m Clause

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause -> m Clause

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause -> m Clause

Show Clause

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Clause -> ShowS

show :: Clause -> String

showList :: [Clause] -> ShowS

Null Clause

A null clause is one with no patterns and no rhs. Should not exist in practice.

Defined in Agda.Syntax.Internal

Methods

empty :: Clause

null :: Clause -> Bool

Pretty Clause

Defined in Agda.Syntax.Internal

Methods

pretty :: Clause -> Doc

prettyPrec :: Int -> Clause -> Doc

prettyList :: [Clause] -> Doc

KillRange Clause

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Clause

HasRange Clause

Defined in Agda.Syntax.Internal

Methods

getRange :: Clause -> Range

Free Clause

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => Clause -> FreeM c

Abstract Clause

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Clause -> Clause

Abstract FunctionInverse

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> FunctionInverse -> FunctionInverse

Apply Clause

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Clause -> Args -> Clause

applyE :: Clause -> Elims -> Clause

Apply FunctionInverse

Defined in Agda.TypeChecking.Substitute

Methods

apply :: FunctionInverse -> Args -> FunctionInverse

applyE :: FunctionInverse -> Elims -> FunctionInverse

GetDefs Clause

Defined in Agda.Syntax.Internal.Defs

Methods

getDefs :: MonadGetDefs m => Clause -> m ()

FunArity Clause

Get the number of initial Apply patterns in a clause.

Defined in Agda.Syntax.Internal.Pattern

Methods

funArity :: Clause -> Int

Free Clause

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: Clause -> FreeT

EmbPrj Clause

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Clause -> S Int32

icod_ :: Clause -> S Int32

value :: Int32 -> R Clause

PrettyTCM Clause

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Clause -> TCM Doc

DropArgs Clause

NOTE: does not work for recursive functions.

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Clause -> Clause

DropArgs FunctionInverse

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> FunctionInverse -> FunctionInverse

NamesIn Clause

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Clause -> Set QName

InstantiateFull Clause

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Clause -> ReduceM Clause

InstantiateFull FunctionInverse

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: FunctionInverse -> ReduceM FunctionInverse

NormaliseProjP Clause

Defined in Agda.TypeChecking.Records

Methods

normaliseProjP :: HasConstInfo m => Clause -> m Clause

ComputeOccurrences Clause

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Clause -> OccM OccurrencesBuilder

Occurs Clause

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Clause -> TCM Clause

metaOccurs :: MetaId -> Clause -> TCM ()

Conversion TOM Clause (Maybe ([Pat O], MExp O))

Defined in Agda.Auto.Convert

Methods

convert :: Clause -> TOM (Maybe ([Pat O], MExp O))

Conversion TOM [Clause] [([Pat O], MExp O)]

Defined in Agda.Auto.Convert

Methods

convert :: [Clause] -> TOM [([Pat O], MExp O)]

FunArity [Clause]

Get the number of common initial Apply patterns in a list of clauses.

Defined in Agda.Syntax.Internal.Pattern

Methods

funArity :: [Clause] -> Int

PrettyTCM (QNamed Clause)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: QNamed Clause -> TCM Doc

Reify (QNamed Clause) Clause

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: QNamed Clause0 -> TCM Clause

reifyWhen :: Bool -> QNamed Clause0 -> TCM Clause

UniverseBi ([Type], [Clause]) Pattern

Defined in Agda.Syntax.Internal

Methods

universeBi :: ([Type], [Clause]) -> [Pattern]

UniverseBi ([Type], [Clause]) Term

Defined in Agda.Syntax.Internal

Methods

universeBi :: ([Type], [Clause]) -> [Term]

type Blocked_ = Blocked ()

Blocked t without the t.

data Blocked t

Something where a meta variable may block reduction.

Constructors

Blocked

Fields

• theBlockingMeta :: MetaId
• ignoreBlocking :: t

NotBlocked

Fields

• blockingStatus :: NotBlocked
• ignoreBlocking :: t

Instances

Functor Blocked

Defined in Agda.Syntax.Internal

Methods

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

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

Applicative Blocked

Blocking by a meta is dominant.

Defined in Agda.Syntax.Internal

Methods

pure :: a -> Blocked a

(<*>) :: Blocked (a -> b) -> Blocked a -> Blocked b

liftA2 :: (a -> b -> c) -> Blocked a -> Blocked b -> Blocked c

(*>) :: Blocked a -> Blocked b -> Blocked b

(<*) :: Blocked a -> Blocked b -> Blocked a

Foldable Blocked

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => Blocked m -> m

foldMap :: Monoid m => (a -> m) -> Blocked a -> m

foldr :: (a -> b -> b) -> b -> Blocked a -> b

foldr' :: (a -> b -> b) -> b -> Blocked a -> b

foldl :: (b -> a -> b) -> b -> Blocked a -> b

foldl' :: (b -> a -> b) -> b -> Blocked a -> b

foldr1 :: (a -> a -> a) -> Blocked a -> a

foldl1 :: (a -> a -> a) -> Blocked a -> a

toList :: Blocked a -> [a]

null :: Blocked a -> Bool

length :: Blocked a -> Int

elem :: Eq a => a -> Blocked a -> Bool

maximum :: Ord a => Blocked a -> a

minimum :: Ord a => Blocked a -> a

sum :: Num a => Blocked a -> a

product :: Num a => Blocked a -> a

Traversable Blocked

Defined in Agda.Syntax.Internal

Methods

traverse :: Applicative f => (a -> f b) -> Blocked a -> f (Blocked b)

sequenceA :: Applicative f => Blocked (f a) -> f (Blocked a)

mapM :: Monad m => (a -> m b) -> Blocked a -> m (Blocked b)

sequence :: Monad m => Blocked (m a) -> m (Blocked a)

Semigroup Blocked_

Defined in Agda.Syntax.Internal

Methods

(<>) :: Blocked_ -> Blocked_ -> Blocked_

sconcat :: NonEmpty Blocked_ -> Blocked_

stimes :: Integral b => b -> Blocked_ -> Blocked_

Monoid Blocked_

Defined in Agda.Syntax.Internal

Methods

mempty :: Blocked_

mappend :: Blocked_ -> Blocked_ -> Blocked_

mconcat :: [Blocked_] -> Blocked_

Subst t a => Subst t (Blocked a)

Defined in Agda.TypeChecking.Substitute

Methods

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

Eq t => Eq (Blocked t)

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Show t => Show (Blocked t)

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Blocked t -> ShowS

show :: Blocked t -> String

showList :: [Blocked t] -> ShowS

KillRange a => KillRange (Blocked a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Blocked a)

Apply t => Apply (Blocked t)

Defined in Agda.TypeChecking.Substitute

Methods

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

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

TermLike a => TermLike (Blocked a)

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Blocked a -> m (Blocked a)

foldTerm :: Monoid m => (Term -> m) -> Blocked a -> m

PrettyTCM a => PrettyTCM (Blocked a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Blocked a -> TCM Doc

Instantiate a => Instantiate (Blocked a)

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Blocked a -> ReduceM (Blocked a)

data NotBlocked

Even if we are not stuck on a meta during reduction we can fail to reduce a definition by pattern matching for another reason.

Constructors

StuckOn Elim

The Elim is neutral and blocks a pattern match.

Underapplied

Not enough arguments were supplied to complete the matching.

AbsurdMatch

We matched an absurd clause, results in a neutral Def.

MissingClauses

We ran out of clauses, all considered clauses produced an actual mismatch. This can happen when try to reduce a function application but we are still missing some function clauses. See Agda.TypeChecking.Patterns.Match.

ReallyNotBlocked

Reduction was not blocked, we reached a whnf which can be anything but a stuck Def.

Instances

Eq NotBlocked

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Data NotBlocked

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NotBlocked -> c NotBlocked

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NotBlocked

toConstr :: NotBlocked -> Constr

dataTypeOf :: NotBlocked -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NotBlocked)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NotBlocked)

gmapT :: (forall b. Data b => b -> b) -> NotBlocked -> NotBlocked

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NotBlocked -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NotBlocked -> r

gmapQ :: (forall d. Data d => d -> u) -> NotBlocked -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> NotBlocked -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NotBlocked -> m NotBlocked

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NotBlocked -> m NotBlocked

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NotBlocked -> m NotBlocked

Show NotBlocked

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> NotBlocked -> ShowS

show :: NotBlocked -> String

showList :: [NotBlocked] -> ShowS

Semigroup NotBlocked

ReallyNotBlocked is the unit. MissingClauses is dominant. StuckOn{} should be propagated, if tied, we take the left.

Defined in Agda.Syntax.Internal

Methods

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

sconcat :: NonEmpty NotBlocked -> NotBlocked

stimes :: Integral b => b -> NotBlocked -> NotBlocked

Monoid NotBlocked

Defined in Agda.Syntax.Internal

Methods

mempty :: NotBlocked

mappend :: NotBlocked -> NotBlocked -> NotBlocked

mconcat :: [NotBlocked] -> NotBlocked

data LevelAtom

An atomic term of type Level.

Constructors

MetaLevel MetaId Elims

A meta variable targeting Level under some eliminations.

BlockedLevel MetaId Term

A term of type Level whose reduction is blocked by a meta.

NeutralLevel NotBlocked Term

A neutral term of type Level.

UnreducedLevel Term

Introduced by instantiate, removed by reduce.

Instances

Eq LevelAtom

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Data LevelAtom

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LevelAtom -> c LevelAtom

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LevelAtom

toConstr :: LevelAtom -> Constr

dataTypeOf :: LevelAtom -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LevelAtom)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LevelAtom)

gmapT :: (forall b. Data b => b -> b) -> LevelAtom -> LevelAtom

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LevelAtom -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LevelAtom -> r

gmapQ :: (forall d. Data d => d -> u) -> LevelAtom -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> LevelAtom -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LevelAtom -> m LevelAtom

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LevelAtom -> m LevelAtom

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LevelAtom -> m LevelAtom

Ord LevelAtom

Defined in Agda.TypeChecking.Substitute

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

Show LevelAtom

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> LevelAtom -> ShowS

show :: LevelAtom -> String

showList :: [LevelAtom] -> ShowS

NFData LevelAtom

Defined in Agda.Syntax.Internal

Methods

rnf :: LevelAtom -> ()

Pretty LevelAtom

Defined in Agda.Syntax.Internal

Methods

pretty :: LevelAtom -> Doc

prettyPrec :: Int -> LevelAtom -> Doc

prettyList :: [LevelAtom] -> Doc

KillRange LevelAtom

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT LevelAtom

TermSize LevelAtom

Defined in Agda.Syntax.Internal

Methods

termSize :: LevelAtom -> Int

tsize :: LevelAtom -> Sum Int

DeBruijn LevelAtom

Defined in Agda.TypeChecking.Substitute.DeBruijn

Methods

deBruijnVar :: Int -> LevelAtom

debruijnNamedVar :: String -> Int -> LevelAtom

deBruijnView :: LevelAtom -> Maybe Int

PrecomputeFreeVars LevelAtom

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: LevelAtom -> FV LevelAtom

Free LevelAtom

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => LevelAtom -> FreeM c

TermLike LevelAtom

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> LevelAtom -> m LevelAtom

foldTerm :: Monoid m => (Term -> m) -> LevelAtom -> m

GetDefs LevelAtom

Defined in Agda.Syntax.Internal.Defs

Methods

getDefs :: MonadGetDefs m => LevelAtom -> m ()

Free LevelAtom

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: LevelAtom -> FreeT

EmbPrj LevelAtom

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: LevelAtom -> S Int32

icod_ :: LevelAtom -> S Int32

value :: Int32 -> R LevelAtom

NamesIn LevelAtom

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: LevelAtom -> Set QName

UnFreezeMeta LevelAtom

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: LevelAtom -> TCM ()

IsInstantiatedMeta LevelAtom

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: LevelAtom -> TCM Bool

MentionsMeta LevelAtom

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMeta :: MetaId -> LevelAtom -> Bool

InstantiateFull LevelAtom

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: LevelAtom -> ReduceM LevelAtom

Normalise LevelAtom

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: LevelAtom -> ReduceM LevelAtom

Simplify LevelAtom

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: LevelAtom -> ReduceM LevelAtom

Reduce LevelAtom

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: LevelAtom -> ReduceM LevelAtom

reduceB' :: LevelAtom -> ReduceM (Blocked LevelAtom)

Instantiate LevelAtom

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: LevelAtom -> ReduceM LevelAtom

SynEq LevelAtom

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: LevelAtom -> LevelAtom -> SynEqM (LevelAtom, LevelAtom)

synEq' :: LevelAtom -> LevelAtom -> SynEqM (LevelAtom, LevelAtom)

HasPolarity LevelAtom

Defined in Agda.TypeChecking.Polarity

Methods

polarities :: Nat -> LevelAtom -> TCM [Polarity]

UsableRelevance LevelAtom

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: Relevance -> LevelAtom -> TCM Bool

ComputeOccurrences LevelAtom

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: LevelAtom -> OccM OccurrencesBuilder

FoldRigid LevelAtom

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> LevelAtom -> TCM m

Occurs LevelAtom

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> LevelAtom -> TCM LevelAtom

metaOccurs :: MetaId -> LevelAtom -> TCM ()

AbsTerm LevelAtom

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> LevelAtom -> LevelAtom

Subst Term LevelAtom

Defined in Agda.TypeChecking.Substitute

Methods

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

data PlusLevel

Constructors

ClosedLevel Integer

n, to represent Setₙ.

Plus Integer LevelAtom

n + ℓ.

Instances

Eq PlusLevel

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Data PlusLevel

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PlusLevel -> c PlusLevel

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PlusLevel

toConstr :: PlusLevel -> Constr

dataTypeOf :: PlusLevel -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PlusLevel)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PlusLevel)

gmapT :: (forall b. Data b => b -> b) -> PlusLevel -> PlusLevel

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PlusLevel -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PlusLevel -> r

gmapQ :: (forall d. Data d => d -> u) -> PlusLevel -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> PlusLevel -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PlusLevel -> m PlusLevel

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PlusLevel -> m PlusLevel

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PlusLevel -> m PlusLevel

Ord PlusLevel

Defined in Agda.TypeChecking.Substitute

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

Show PlusLevel

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> PlusLevel -> ShowS

show :: PlusLevel -> String

showList :: [PlusLevel] -> ShowS

NFData PlusLevel

Defined in Agda.Syntax.Internal

Methods

rnf :: PlusLevel -> ()

Pretty PlusLevel

Defined in Agda.Syntax.Internal

Methods

pretty :: PlusLevel -> Doc

prettyPrec :: Int -> PlusLevel -> Doc

prettyList :: [PlusLevel] -> Doc

KillRange PlusLevel

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT PlusLevel

TermSize PlusLevel

Defined in Agda.Syntax.Internal

Methods

termSize :: PlusLevel -> Int

tsize :: PlusLevel -> Sum Int

DeBruijn PlusLevel

Defined in Agda.TypeChecking.Substitute.DeBruijn

Methods

deBruijnVar :: Int -> PlusLevel

debruijnNamedVar :: String -> Int -> PlusLevel

deBruijnView :: PlusLevel -> Maybe Int

PrecomputeFreeVars PlusLevel

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: PlusLevel -> FV PlusLevel

Free PlusLevel

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => PlusLevel -> FreeM c

TermLike PlusLevel

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> PlusLevel -> m PlusLevel

foldTerm :: Monoid m => (Term -> m) -> PlusLevel -> m

GetDefs PlusLevel

Defined in Agda.Syntax.Internal.Defs

Methods

getDefs :: MonadGetDefs m => PlusLevel -> m ()

Free PlusLevel

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: PlusLevel -> FreeT

EmbPrj PlusLevel

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: PlusLevel -> S Int32

icod_ :: PlusLevel -> S Int32

value :: Int32 -> R PlusLevel

NamesIn PlusLevel

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: PlusLevel -> Set QName

UnFreezeMeta PlusLevel

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: PlusLevel -> TCM ()

IsInstantiatedMeta PlusLevel

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: PlusLevel -> TCM Bool

MentionsMeta PlusLevel

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMeta :: MetaId -> PlusLevel -> Bool

InstantiateFull PlusLevel

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: PlusLevel -> ReduceM PlusLevel

Normalise PlusLevel

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: PlusLevel -> ReduceM PlusLevel

Simplify PlusLevel

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: PlusLevel -> ReduceM PlusLevel

Reduce PlusLevel

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: PlusLevel -> ReduceM PlusLevel

reduceB' :: PlusLevel -> ReduceM (Blocked PlusLevel)

Instantiate PlusLevel

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: PlusLevel -> ReduceM PlusLevel

SynEq PlusLevel

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: PlusLevel -> PlusLevel -> SynEqM (PlusLevel, PlusLevel)

synEq' :: PlusLevel -> PlusLevel -> SynEqM (PlusLevel, PlusLevel)

HasPolarity PlusLevel

Defined in Agda.TypeChecking.Polarity

Methods

polarities :: Nat -> PlusLevel -> TCM [Polarity]

UsableRelevance PlusLevel

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: Relevance -> PlusLevel -> TCM Bool

ComputeOccurrences PlusLevel

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: PlusLevel -> OccM OccurrencesBuilder

FoldRigid PlusLevel

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> PlusLevel -> TCM m

Occurs PlusLevel

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> PlusLevel -> TCM PlusLevel

metaOccurs :: MetaId -> PlusLevel -> TCM ()

AbsTerm PlusLevel

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> PlusLevel -> PlusLevel

Subst Term PlusLevel

Defined in Agda.TypeChecking.Substitute

Methods

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

newtype Level

A level is a maximum expression of 0..n PlusLevel expressions each of which is a number or an atom plus a number.

The empty maximum is the canonical representation for level 0.

Constructors

Max [PlusLevel]

Instances

Eq Level

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Data Level

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Level -> c Level

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Level

toConstr :: Level -> Constr

dataTypeOf :: Level -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Level)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Level)

gmapT :: (forall b. Data b => b -> b) -> Level -> Level

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Level -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Level -> r

gmapQ :: (forall d. Data d => d -> u) -> Level -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Level -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Level -> m Level

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Level -> m Level

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Level -> m Level

Ord Level

Defined in Agda.TypeChecking.Substitute

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

Show Level

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Level -> ShowS

show :: Level -> String

showList :: [Level] -> ShowS

NFData Level

Defined in Agda.Syntax.Internal

Methods

rnf :: Level -> ()

Pretty Level

Defined in Agda.Syntax.Internal

Methods

pretty :: Level -> Doc

prettyPrec :: Int -> Level -> Doc

prettyList :: [Level] -> Doc

KillRange Level

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Level

TermSize Level

Defined in Agda.Syntax.Internal

Methods

termSize :: Level -> Int

tsize :: Level -> Sum Int

DeBruijn Level

Defined in Agda.TypeChecking.Substitute.DeBruijn

Methods

deBruijnVar :: Int -> Level

debruijnNamedVar :: String -> Int -> Level

deBruijnView :: Level -> Maybe Int

PrecomputeFreeVars Level

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Level -> FV Level

Free Level

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => Level -> FreeM c

TermLike Level

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Level -> m Level

foldTerm :: Monoid m => (Term -> m) -> Level -> m

GetDefs Level

Defined in Agda.Syntax.Internal.Defs

Methods

getDefs :: MonadGetDefs m => Level -> m ()

Free Level

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: Level -> FreeT

EmbPrj Level

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Level -> S Int32

icod_ :: Level -> S Int32

value :: Int32 -> R Level

PrettyTCM Level

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Level -> TCM Doc

NamesIn Level

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Level -> Set QName

UnFreezeMeta Level

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: Level -> TCM ()

IsInstantiatedMeta Level

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: Level -> TCM Bool

MentionsMeta Level

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMeta :: MetaId -> Level -> Bool

InstantiateFull Level

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Level -> ReduceM Level

Normalise Level

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Level -> ReduceM Level

Simplify Level

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Level -> ReduceM Level

Reduce Level

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Level -> ReduceM Level

reduceB' :: Level -> ReduceM (Blocked Level)

Instantiate Level

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Level -> ReduceM Level

SynEq Level

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Level -> Level -> SynEqM (Level, Level)

synEq' :: Level -> Level -> SynEqM (Level, Level)

Match Level

Defined in Agda.TypeChecking.DisplayForm

Methods

match :: Level -> Level -> MaybeT TCM [WithOrigin Term]

HasPolarity Level

Defined in Agda.TypeChecking.Polarity

Methods

polarities :: Nat -> Level -> TCM [Polarity]

UsableRelevance Level

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: Relevance -> Level -> TCM Bool

ComputeOccurrences Level

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Level -> OccM OccurrencesBuilder

FoldRigid Level

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Level -> TCM m

Occurs Level

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Level -> TCM Level

metaOccurs :: MetaId -> Level -> TCM ()

AbsTerm Level

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Level -> Level

Subst Term Level

Defined in Agda.TypeChecking.Substitute

Methods

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

Reify Level Expr

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Level -> TCM Expr

reifyWhen :: Bool -> Level -> TCM Expr

Match NLPat Level

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> NLPat -> Level -> NLM ()

data Sort

Sorts.

Constructors

Type Level

Set ℓ.

Prop

Dummy sort.

Inf

Setω.

SizeUniv

SizeUniv, a sort inhabited by type Size.

PiSort Sort (Abs Sort)

Sort of the pi type.

UnivSort Sort

Sort of another sort.

MetaS !MetaId Elims

Instances

Eq Sort

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Data Sort

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sort -> c Sort

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sort

toConstr :: Sort -> Constr

dataTypeOf :: Sort -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Sort)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sort)

gmapT :: (forall b. Data b => b -> b) -> Sort -> Sort

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r

gmapQ :: (forall d. Data d => d -> u) -> Sort -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Sort -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sort -> m Sort

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sort -> m Sort

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sort -> m Sort

Ord Sort

Defined in Agda.TypeChecking.Substitute

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

Show Sort

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Sort -> ShowS

show :: Sort -> String

showList :: [Sort] -> ShowS

NFData Sort

Defined in Agda.Syntax.Internal

Methods

rnf :: Sort -> ()

Pretty Sort

Defined in Agda.Syntax.Internal

Methods

pretty :: Sort -> Doc

prettyPrec :: Int -> Sort -> Doc

prettyList :: [Sort] -> Doc

KillRange Sort

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Sort

TermSize Sort

Defined in Agda.Syntax.Internal

Methods

termSize :: Sort -> Int

tsize :: Sort -> Sum Int

PrecomputeFreeVars Sort

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Sort -> FV Sort

Free Sort

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => Sort -> FreeM c

Abstract Sort

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Sort -> Sort

Apply Sort

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Sort -> Args -> Sort

applyE :: Sort -> Elims -> Sort

GetDefs Sort

Defined in Agda.Syntax.Internal.Defs

Methods

getDefs :: MonadGetDefs m => Sort -> m ()

Free Sort

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: Sort -> FreeT

EmbPrj Sort

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Sort -> S Int32

icod_ :: Sort -> S Int32

value :: Int32 -> R Sort

PrettyTCM Sort

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Sort -> TCM Doc

NamesIn Sort

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Sort -> Set QName

UnFreezeMeta Sort

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: Sort -> TCM ()

MentionsMeta Sort

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMeta :: MetaId -> Sort -> Bool

InstantiateFull Sort

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Sort -> ReduceM Sort

Normalise Sort

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Sort -> ReduceM Sort

Simplify Sort

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Sort -> ReduceM Sort

Reduce Sort

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Sort -> ReduceM Sort

reduceB' :: Sort -> ReduceM (Blocked Sort)

Instantiate Sort

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Sort -> ReduceM Sort

SynEq Sort

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Sort -> Sort -> SynEqM (Sort, Sort)

synEq' :: Sort -> Sort -> SynEqM (Sort, Sort)

Match Sort

Defined in Agda.TypeChecking.DisplayForm

Methods

match :: Sort -> Sort -> MaybeT TCM [WithOrigin Term]

UsableRelevance Sort

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: Relevance -> Sort -> TCM Bool

FoldRigid Sort

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Sort -> TCM m

Occurs Sort

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Sort -> TCM Sort

metaOccurs :: MetaId -> Sort -> TCM ()

AbsTerm Sort

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Sort -> Sort

Subst Term Sort

Defined in Agda.TypeChecking.Substitute

Methods

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

Reify Sort Expr

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Sort -> TCM Expr

reifyWhen :: Bool -> Sort -> TCM Expr

Match NLPat Sort

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> NLPat -> Sort -> NLM ()

PatternFrom Sort NLPat

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> Sort -> TCM NLPat

type Telescope = Tele (Dom Type)

data Tele a

Sequence of types. An argument of the first type is bound in later types and so on.

Constructors

EmptyTel

ExtendTel a (Abs (Tele a))

Abs is never NoAbs.

Instances

Functor Tele

Defined in Agda.Syntax.Internal

Methods

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

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

Foldable Tele

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => Tele m -> m

foldMap :: Monoid m => (a -> m) -> Tele a -> m

foldr :: (a -> b -> b) -> b -> Tele a -> b

foldr' :: (a -> b -> b) -> b -> Tele a -> b

foldl :: (b -> a -> b) -> b -> Tele a -> b

foldl' :: (b -> a -> b) -> b -> Tele a -> b

foldr1 :: (a -> a -> a) -> Tele a -> a

foldl1 :: (a -> a -> a) -> Tele a -> a

toList :: Tele a -> [a]

null :: Tele a -> Bool

length :: Tele a -> Int

elem :: Eq a => a -> Tele a -> Bool

maximum :: Ord a => Tele a -> a

minimum :: Ord a => Tele a -> a

sum :: Num a => Tele a -> a

product :: Num a => Tele a -> a

Traversable Tele

Defined in Agda.Syntax.Internal

Methods

traverse :: Applicative f => (a -> f b) -> Tele a -> f (Tele b)

sequenceA :: Applicative f => Tele (f a) -> f (Tele a)

mapM :: Monad m => (a -> m b) -> Tele a -> m (Tele b)

sequence :: Monad m => Tele (m a) -> m (Tele a)

TelToArgs Telescope

Defined in Agda.Syntax.Internal

Methods

telToArgs :: Telescope -> [Arg ArgName]

Abstract Telescope

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Telescope -> Telescope

TeleNoAbs Telescope

Defined in Agda.TypeChecking.Substitute

Methods

teleNoAbs :: Telescope -> Term -> Term

PrettyTCM Telescope

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Telescope -> TCM Doc

DropArgs Telescope

NOTE: This creates telescopes with unbound de Bruijn indices.

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Telescope -> Telescope

AddContext Telescope

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => Telescope -> tcm a -> tcm a

contextSize :: Telescope -> Nat

Reduce Telescope

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Telescope -> ReduceM Telescope

reduceB' :: Telescope -> ReduceM (Blocked Telescope)

Instantiate Telescope

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Telescope -> ReduceM Telescope

Reify Telescope Telescope

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Telescope0 -> TCM Telescope

reifyWhen :: Bool -> Telescope0 -> TCM Telescope

Subst t a => Subst t (Tele a)

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Data a => Data (Tele a)

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Tele a -> c (Tele a)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Tele a)

toConstr :: Tele a -> Constr

dataTypeOf :: Tele a -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Tele a))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Tele a))

gmapT :: (forall b. Data b => b -> b) -> Tele a -> Tele a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Tele a -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Tele a -> r

gmapQ :: (forall d. Data d => d -> u) -> Tele a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Tele a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Tele a -> m (Tele a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Tele a -> m (Tele a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Tele a -> m (Tele a)

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

Defined in Agda.TypeChecking.Substitute

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

Show a => Show (Tele a)

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Tele a -> ShowS

show :: Tele a -> String

showList :: [Tele a] -> ShowS

Null (Tele a)

Defined in Agda.Syntax.Internal

Methods

empty :: Tele a

null :: Tele a -> Bool

Pretty a => Pretty (Tele (Dom a))

Defined in Agda.Syntax.Internal

Methods

pretty :: Tele (Dom a) -> Doc

prettyPrec :: Int -> Tele (Dom a) -> Doc

prettyList :: [Tele (Dom a)] -> Doc

Sized (Tele a)

The size of a telescope is its length (as a list).

Defined in Agda.Syntax.Internal

Methods

size :: Tele a -> Int

KillRange a => KillRange (Tele a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Tele a)

Free a => Free (Tele a)

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => Tele a -> FreeM c

Subst Term a => Apply (Tele a)

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Free a => Free (Tele a)

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: Tele a -> FreeT

EmbPrj a => EmbPrj (Tele a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Tele a -> S Int32

icod_ :: Tele a -> S Int32

value :: Int32 -> R (Tele a)

NamesIn a => NamesIn (Tele a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Tele a -> Set QName

AddContext (KeepNames Telescope)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => KeepNames Telescope -> tcm a -> tcm a

contextSize :: KeepNames Telescope -> Nat

MentionsMeta a => MentionsMeta (Tele a)

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMeta :: MetaId -> Tele a -> Bool

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

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Tele a -> ReduceM (Tele a)

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

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Tele a -> ReduceM (Tele a)

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

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Tele a -> ReduceM (Tele a)

ComputeOccurrences a => ComputeOccurrences (Tele a)

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Tele a -> OccM OccurrencesBuilder

class LensSort a where

Minimal complete definition

lensSort

Methods

lensSort :: Lens' Sort a

getSort :: a -> Sort

Instances

LensSort a => LensSort (Dom a)

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' Sort (Dom a)

getSort :: Dom a -> Sort

LensSort (Type' a)

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' Sort (Type' a)

getSort :: Type' a -> Sort

LensSort a => LensSort (Abs a)

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' Sort (Abs a)

getSort :: Abs a -> Sort

type Type = Type' Term

data Type' a

Types are terms with a sort annotation.

Constructors

El

Fields

• _getSort :: Sort
• unEl :: a

Instances

Functor Type'

Defined in Agda.Syntax.Internal

Methods

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

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

Foldable Type'

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => Type' m -> m

foldMap :: Monoid m => (a -> m) -> Type' a -> m

foldr :: (a -> b -> b) -> b -> Type' a -> b

foldr' :: (a -> b -> b) -> b -> Type' a -> b

foldl :: (b -> a -> b) -> b -> Type' a -> b

foldl' :: (b -> a -> b) -> b -> Type' a -> b

foldr1 :: (a -> a -> a) -> Type' a -> a

foldl1 :: (a -> a -> a) -> Type' a -> a

toList :: Type' a -> [a]

null :: Type' a -> Bool

length :: Type' a -> Int

elem :: Eq a => a -> Type' a -> Bool

maximum :: Ord a => Type' a -> a

minimum :: Ord a => Type' a -> a

sum :: Num a => Type' a -> a

product :: Num a => Type' a -> a

Traversable Type'

Defined in Agda.Syntax.Internal

Methods

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

sequenceA :: Applicative f => Type' (f a) -> f (Type' a)

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

sequence :: Monad m => Type' (m a) -> m (Type' a)

NFData Type

Defined in Agda.Syntax.Internal

Methods

rnf :: Type -> ()

Decoration Type'

Defined in Agda.Syntax.Internal

Methods

traverseF :: Functor m => (a -> m b) -> Type' a -> m (Type' b)

distributeF :: Functor m => Type' (m a) -> m (Type' a)

Pretty Type

Defined in Agda.Syntax.Internal

Methods

pretty :: Type -> Doc

prettyPrec :: Int -> Type -> Doc

prettyList :: [Type] -> Doc

TelToArgs ListTel

Defined in Agda.Syntax.Internal

Methods

telToArgs :: ListTel -> [Arg ArgName]

TelToArgs Telescope

Defined in Agda.Syntax.Internal

Methods

telToArgs :: Telescope -> [Arg ArgName]

PrecomputeFreeVars Type

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Type -> FV Type

Abstract Telescope

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Telescope -> Telescope

Abstract Type

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Type -> Type

TermLike Type

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Type -> m Type

foldTerm :: Monoid m => (Term -> m) -> Type -> m

GetDefs Type

Defined in Agda.Syntax.Internal.Defs

Methods

getDefs :: MonadGetDefs m => Type -> m ()

Free Type

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: Type -> FreeT

TeleNoAbs ListTel

Defined in Agda.TypeChecking.Substitute

Methods

teleNoAbs :: ListTel -> Term -> Term

TeleNoAbs Telescope

Defined in Agda.TypeChecking.Substitute

Methods

teleNoAbs :: Telescope -> Term -> Term

PrettyTCM Telescope

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Telescope -> TCM Doc

PrettyTCM Type

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Type -> TCM Doc

DropArgs Telescope

NOTE: This creates telescopes with unbound de Bruijn indices.

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Telescope -> Telescope

AddContext Telescope

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => Telescope -> tcm a -> tcm a

contextSize :: Telescope -> Nat

UnFreezeMeta Type

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: Type -> TCM ()

MentionsMeta Type

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMeta :: MetaId -> Type -> Bool

Normalise Type

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Type -> ReduceM Type

Simplify Type

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Type -> ReduceM Type

Reduce Telescope

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Telescope -> ReduceM Telescope

reduceB' :: Telescope -> ReduceM (Blocked Telescope)

Reduce Type

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Type -> ReduceM Type

reduceB' :: Type -> ReduceM (Blocked Type)

Instantiate Telescope

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Telescope -> ReduceM Telescope

Instantiate Type

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Type -> ReduceM Type

SynEq Type

Syntactic equality ignores sorts.

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Type -> Type -> SynEqM (Type, Type)

synEq' :: Type -> Type -> SynEqM (Type, Type)

HasPolarity Type

Defined in Agda.TypeChecking.Polarity

Methods

polarities :: Nat -> Type -> TCM [Polarity]

ComputeOccurrences Type

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Type -> OccM OccurrencesBuilder

ToTerm Type

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Type -> Term)

toTermR :: TCM (Type -> ReduceM Term)

PrimTerm Type

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Type -> TCM Term

FoldRigid Type

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Type -> TCM m

Occurs Type

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Type -> TCM Type

metaOccurs :: MetaId -> Type -> TCM ()

AbsTerm Type

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Type -> Type

Reify Telescope Telescope

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Telescope0 -> TCM Telescope

reifyWhen :: Bool -> Telescope0 -> TCM Telescope

Reify Type Expr

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Type -> TCM Expr

reifyWhen :: Bool -> Type -> TCM Expr

Match NLPType Type

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> NLPType -> Type -> NLM ()

PatternFrom Type NLPType

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> Type -> TCM NLPType

Conversion TOM Type (MExp O)

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (MExp O)

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

Defined in Agda.TypeChecking.Substitute

Methods

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

Conversion MOT (Exp O) Type

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Type

Eq a => Eq (Type' a)

Syntactic Type equality, ignores sort annotations.

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Data a => Data (Type' a)

Defined in Agda.Syntax.Internal

Methods

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

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

toConstr :: Type' a -> Constr

dataTypeOf :: Type' a -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Type' a -> Type' a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type' a -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type' a -> r

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

gmapQi :: Int -> (forall d. Data d => d -> u) -> Type' a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Type' a -> m (Type' a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Type' a -> m (Type' a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Type' a -> m (Type' a)

Ord a => Ord (Type' a)

Defined in Agda.TypeChecking.Substitute

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

Show a => Show (Type' a)

Defined in Agda.Syntax.Internal

Methods

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

show :: Type' a -> String

showList :: [Type' a] -> ShowS

KillRange a => KillRange (Type' a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Type' a)

SgTel (Dom (ArgName, Type))

Defined in Agda.Syntax.Internal

Methods

sgTel :: Dom (ArgName, Type) -> Telescope

SgTel (Dom Type)

Defined in Agda.Syntax.Internal

Methods

sgTel :: Dom Type -> Telescope

LensSort (Type' a)

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' Sort (Type' a)

getSort :: Type' a -> Sort

Free a => Free (Type' a)

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => Type' a -> FreeM c

EmbPrj a => EmbPrj (Type' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Type' a -> S Int32

icod_ :: Type' a -> S Int32

value :: Int32 -> R (Type' a)

PrettyTCM (Type' NLPat)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Type' NLPat -> TCM Doc

NamesIn a => NamesIn (Type' a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Type' a -> Set QName

IsSizeType a => IsSizeType (Type' a)

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

isSizeType :: Type' a -> TCM (Maybe BoundedSize)

AddContext (Dom (String, Type))

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom (String, Type) -> tcm a -> tcm a

contextSize :: Dom (String, Type) -> Nat

AddContext (Dom (Name, Type))

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom (Name, Type) -> tcm a -> tcm a

contextSize :: Dom (Name, Type) -> Nat

AddContext (Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom Type -> tcm a -> tcm a

contextSize :: Dom Type -> Nat

AddContext (KeepNames Telescope)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => KeepNames Telescope -> tcm a -> tcm a

contextSize :: KeepNames Telescope -> Nat

InstantiateFull a => InstantiateFull (Type' a)

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Type' a -> ReduceM (Type' a)

UsableRelevance a => UsableRelevance (Type' a)

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: Relevance -> Type' a -> TCM Bool

SgTel (ArgName, Dom Type)

Defined in Agda.Syntax.Internal

Methods

sgTel :: (ArgName, Dom Type) -> Telescope

AddContext ([WithHiding Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => ([WithHiding Name], Dom Type) -> tcm a -> tcm a

contextSize :: ([WithHiding Name], Dom Type) -> Nat

AddContext ([Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => ([Name], Dom Type) -> tcm a -> tcm a

contextSize :: ([Name], Dom Type) -> Nat

AddContext (String, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => (String, Dom Type) -> tcm a -> tcm a

contextSize :: (String, Dom Type) -> Nat

AddContext (Name, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => (Name, Dom Type) -> tcm a -> tcm a

contextSize :: (Name, Dom Type) -> Nat

AddContext (KeepNames String, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => (KeepNames String, Dom Type) -> tcm a -> tcm a

contextSize :: (KeepNames String, Dom Type) -> Nat

UniverseBi ([Type], [Clause]) Pattern

Defined in Agda.Syntax.Internal

Methods

universeBi :: ([Type], [Clause]) -> [Pattern]

UniverseBi ([Type], [Clause]) Term

Defined in Agda.Syntax.Internal

Methods

universeBi :: ([Type], [Clause]) -> [Term]

data Abs a

Binder. Abs: The bound variable might appear in the body. NoAbs is pseudo-binder, it does not introduce a fresh variable, similar to the const of Haskell.

Constructors

Abs

The body has (at least) one free variable. Danger: unAbs doesn't shift variables properly

Fields

• absName :: ArgName
• unAbs :: a

NoAbs

Fields

• absName :: ArgName
• unAbs :: a

Instances

Functor Abs

Defined in Agda.Syntax.Internal

Methods

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

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

Foldable Abs

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => Abs m -> m

foldMap :: Monoid m => (a -> m) -> Abs a -> m

foldr :: (a -> b -> b) -> b -> Abs a -> b

foldr' :: (a -> b -> b) -> b -> Abs a -> b

foldl :: (b -> a -> b) -> b -> Abs a -> b

foldl' :: (b -> a -> b) -> b -> Abs a -> b

foldr1 :: (a -> a -> a) -> Abs a -> a

foldl1 :: (a -> a -> a) -> Abs a -> a

toList :: Abs a -> [a]

null :: Abs a -> Bool

length :: Abs a -> Int

elem :: Eq a => a -> Abs a -> Bool

maximum :: Ord a => Abs a -> a

minimum :: Ord a => Abs a -> a

sum :: Num a => Abs a -> a

product :: Num a => Abs a -> a

Traversable Abs

Defined in Agda.Syntax.Internal

Methods

traverse :: Applicative f => (a -> f b) -> Abs a -> f (Abs b)

sequenceA :: Applicative f => Abs (f a) -> f (Abs a)

mapM :: Monad m => (a -> m b) -> Abs a -> m (Abs b)

sequence :: Monad m => Abs (m a) -> m (Abs a)

Decoration Abs

Defined in Agda.Syntax.Internal

Methods

traverseF :: Functor m => (a -> m b) -> Abs a -> m (Abs b)

distributeF :: Functor m => Abs (m a) -> m (Abs a)

Suggest String (Abs b)

Defined in Agda.Syntax.Internal

Methods

suggest :: String -> Abs b -> String

Suggest Name (Abs b)

Defined in Agda.Syntax.Internal

Methods

suggest :: Name -> Abs b -> String

Subst t a => Subst t (Abs a)

Defined in Agda.TypeChecking.Substitute

Methods

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

Conversion MOT a b => Conversion MOT (Abs a) (Abs b)

Defined in Agda.Auto.Convert

Methods

convert :: Abs0 a -> MOT (Abs b)

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

Equality of binders relies on weakening which is a special case of renaming which is a special case of substitution.

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Data a => Data (Abs a)

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Abs a -> c (Abs a)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Abs a)

toConstr :: Abs a -> Constr

dataTypeOf :: Abs a -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Abs a))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Abs a))

gmapT :: (forall b. Data b => b -> b) -> Abs a -> Abs a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Abs a -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Abs a -> r

gmapQ :: (forall d. Data d => d -> u) -> Abs a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Abs a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Abs a -> m (Abs a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Abs a -> m (Abs a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Abs a -> m (Abs a)

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

Defined in Agda.TypeChecking.Substitute

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

Show a => Show (Abs a)

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Abs a -> ShowS

show :: Abs a -> String

showList :: [Abs a] -> ShowS

Sized a => Sized (Abs a)

Defined in Agda.Syntax.Internal

Methods

size :: Abs a -> Int

KillRange a => KillRange (Abs a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Abs a)

LensSort a => LensSort (Abs a)

Defined in Agda.Syntax.Internal

Methods

lensSort :: Lens' Sort (Abs a)

getSort :: Abs a -> Sort

PrecomputeFreeVars a => PrecomputeFreeVars (Abs a)

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Abs a -> FV (Abs a)

Free a => Free (Abs a)

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => Abs a -> FreeM c

TermLike a => TermLike (Abs a)

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Abs a -> m (Abs a)

foldTerm :: Monoid m => (Term -> m) -> Abs a -> m

GetDefs a => GetDefs (Abs a)

Defined in Agda.Syntax.Internal.Defs

Methods

getDefs :: MonadGetDefs m => Abs a -> m ()

Free a => Free (Abs a)

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: Abs a -> FreeT

EmbPrj a => EmbPrj (Abs a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Abs a -> S Int32

icod_ :: Abs a -> S Int32

value :: Int32 -> R (Abs a)

NamesIn a => NamesIn (Abs a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Abs a -> Set QName

UnFreezeMeta a => UnFreezeMeta (Abs a)

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: Abs a -> TCM ()

IsInstantiatedMeta a => IsInstantiatedMeta (Abs a)

Does not worry about raising.

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: Abs a -> TCM Bool

MentionsMeta t => MentionsMeta (Abs t)

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMeta :: MetaId -> Abs t -> Bool

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

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Abs a -> ReduceM (Abs a)

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

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Abs a -> ReduceM (Abs a)

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

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Abs a -> ReduceM (Abs a)

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

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Abs a -> ReduceM (Abs a)

reduceB' :: Abs a -> ReduceM (Blocked (Abs a))

Instantiate t => Instantiate (Abs t)

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Abs t -> ReduceM (Abs t)

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

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Abs a -> Abs a -> SynEqM (Abs a, Abs a)

synEq' :: Abs a -> Abs a -> SynEqM (Abs a, Abs a)

HasPolarity a => HasPolarity (Abs a)

Defined in Agda.TypeChecking.Polarity

Methods

polarities :: Nat -> Abs a -> TCM [Polarity]

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

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: Relevance -> Abs a -> TCM Bool

ComputeOccurrences a => ComputeOccurrences (Abs a)

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Abs a -> OccM OccurrencesBuilder

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

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Abs a -> TCM m

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

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Abs a -> TCM (Abs a)

metaOccurs :: MetaId -> Abs a -> TCM ()

(Subst Term a, AbsTerm a) => AbsTerm (Abs a)

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Abs a -> Abs a

Suggest (Abs a) (Abs b)

Defined in Agda.Syntax.Internal

Methods

suggest :: Abs a -> Abs b -> String

(Match a b, Subst t1 a, Subst t2 b) => Match (Abs a) (Abs b)

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> Abs a -> Abs b -> NLM ()

PatternFrom a b => PatternFrom (Abs a) (Abs b)

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> Abs a -> TCM (Abs b)

(Free i, Reify i a) => Reify (Abs i) (Name, a)

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Abs i -> TCM (Name, a)

reifyWhen :: Bool -> Abs i -> TCM (Name, a)

type ArgName = String

Names in binders and arguments.

type Elims

Arguments

 = [Elim]

eliminations ordered left-to-right.

type Elim = Elim' Term

data Elim' a

Eliminations, subsuming applications and projections.

Constructors

Apply (Arg a)

Application.

Proj ProjOrigin QName

Projection. QName is name of a record projection.

Instances

Functor Elim'

Defined in Agda.Syntax.Internal

Methods

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

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

Foldable Elim'

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => Elim' m -> m

foldMap :: Monoid m => (a -> m) -> Elim' a -> m

foldr :: (a -> b -> b) -> b -> Elim' a -> b

foldr' :: (a -> b -> b) -> b -> Elim' a -> b

foldl :: (b -> a -> b) -> b -> Elim' a -> b

foldl' :: (b -> a -> b) -> b -> Elim' a -> b

foldr1 :: (a -> a -> a) -> Elim' a -> a

foldl1 :: (a -> a -> a) -> Elim' a -> a

toList :: Elim' a -> [a]

null :: Elim' a -> Bool

length :: Elim' a -> Int

elem :: Eq a => a -> Elim' a -> Bool

maximum :: Ord a => Elim' a -> a

minimum :: Ord a => Elim' a -> a

sum :: Num a => Elim' a -> a

product :: Num a => Elim' a -> a

Traversable Elim'

Defined in Agda.Syntax.Internal

Methods

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

sequenceA :: Applicative f => Elim' (f a) -> f (Elim' a)

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

sequence :: Monad m => Elim' (m a) -> m (Elim' a)

IsProjElim Elim

Defined in Agda.Syntax.Internal

Methods

isProjElim :: Elim -> Maybe (ProjOrigin, QName)

PrettyTCM Elim

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Elim -> TCM Doc

MentionsMeta Elim

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMeta :: MetaId -> Elim -> Bool

Normalise Elim

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Elim -> ReduceM Elim

Simplify Elim

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Elim -> ReduceM Elim

Reduce Elim

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Elim -> ReduceM Elim

reduceB' :: Elim -> ReduceM (Blocked Elim)

Instantiate Elim

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Elim -> ReduceM Elim

IsPrefixOf Elims

Defined in Agda.TypeChecking.Abstract

Methods

isPrefixOf :: Elims -> Elims -> Maybe Elims

UniverseBi Elims Pattern

Defined in Agda.Syntax.Internal

Methods

universeBi :: Elims -> [Pattern]

UniverseBi Elims Term

Defined in Agda.Syntax.Internal

Methods

universeBi :: Elims -> [Term]

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

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Data a => Data (Elim' a)

Defined in Agda.Syntax.Internal

Methods

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

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

toConstr :: Elim' a -> Constr

dataTypeOf :: Elim' a -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Elim' a -> Elim' a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Elim' a -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Elim' a -> r

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

gmapQi :: Int -> (forall d. Data d => d -> u) -> Elim' a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a)

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

Defined in Agda.TypeChecking.Substitute

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

Show a => Show (Elim' a)

Defined in Agda.Syntax.Internal

Methods

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

show :: Elim' a -> String

showList :: [Elim' a] -> ShowS

NFData a => NFData (Elim' a)

Defined in Agda.Syntax.Internal

Methods

rnf :: Elim' a -> ()

Pretty tm => Pretty (Elim' tm)

Defined in Agda.Syntax.Internal

Methods

pretty :: Elim' tm -> Doc

prettyPrec :: Int -> Elim' tm -> Doc

prettyList :: [Elim' tm] -> Doc

KillRange a => KillRange (Elim' a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Elim' a)

LensOrigin (Elim' a)

This instance cheats on Proj, use with care. Projs are always assumed to be UserWritten, since they have no ArgInfo.

Defined in Agda.Syntax.Internal

Methods

getOrigin :: Elim' a -> Origin

setOrigin :: Origin -> Elim' a -> Elim' a

mapOrigin :: (Origin -> Origin) -> Elim' a -> Elim' a

PrecomputeFreeVars a => PrecomputeFreeVars (Elim' a)

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Elim' a -> FV (Elim' a)

Free a => Free (Elim' a)

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => Elim' a -> FreeM c

TermLike a => TermLike (Elim' a)

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Elim' a -> m (Elim' a)

foldTerm :: Monoid m => (Term -> m) -> Elim' a -> m

GetDefs a => GetDefs (Elim' a)

Defined in Agda.Syntax.Internal.Defs

Methods

getDefs :: MonadGetDefs m => Elim' a -> m ()

Free a => Free (Elim' a)

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: Elim' a -> FreeT

EmbPrj a => EmbPrj (Elim' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Elim' a -> S Int32

icod_ :: Elim' a -> S Int32

value :: Int32 -> R (Elim' a)

PrettyTCM (Elim' NLPat)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Elim' NLPat -> TCM Doc

PrettyTCM (Elim' DisplayTerm)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Elim' DisplayTerm -> TCM Doc

NamesIn a => NamesIn (Elim' a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Elim' a -> Set QName

InstantiateFull a => InstantiateFull (Elim' a)

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Elim' a -> ReduceM (Elim' a)

SynEq a => SynEq (Elim' a)

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Elim' a -> Elim' a -> SynEqM (Elim' a, Elim' a)

synEq' :: Elim' a -> Elim' a -> SynEqM (Elim' a, Elim' a)

SubstWithOrigin (Arg a) => SubstWithOrigin (Elim' a)

Defined in Agda.TypeChecking.DisplayForm

Methods

substWithOrigin :: Substitution -> [WithOrigin Term] -> Elim' a -> Elim' a

Match a => Match (Elim' a)

Defined in Agda.TypeChecking.DisplayForm

Methods

match :: Elim' a -> Elim' a -> MaybeT TCM [WithOrigin Term]

HasPolarity a => HasPolarity (Elim' a)

Defined in Agda.TypeChecking.Polarity

Methods

polarities :: Nat -> Elim' a -> TCM [Polarity]

UsableRelevance a => UsableRelevance (Elim' a)

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: Relevance -> Elim' a -> TCM Bool

ForcedVariables a => ForcedVariables (Elim' a)

Defined in Agda.TypeChecking.Forcing

Methods

forcedVariables :: Elim' a -> [(Modality, Nat)]

ComputeOccurrences a => ComputeOccurrences (Elim' a)

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Elim' a -> OccM OccurrencesBuilder

FoldRigid a => FoldRigid (Elim' a)

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Elim' a -> TCM m

Occurs a => Occurs (Elim' a)

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Elim' a -> TCM (Elim' a)

metaOccurs :: MetaId -> Elim' a -> TCM ()

AbsTerm a => AbsTerm (Elim' a)

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Elim' a -> Elim' a

PatternVarModalities a x => PatternVarModalities (Elim' a) x

Defined in Agda.Syntax.Internal.Pattern

Methods

patternVarModalities :: Elim' a -> [(x, Modality)]

Reify i a => Reify (Elim' i) (Elim' a)

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Elim' i -> TCM (Elim' a)

reifyWhen :: Bool -> Elim' i -> TCM (Elim' a)

Match a b => Match (Elim' a) (Elim' b)

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> Elim' a -> Elim' b -> NLM ()

PatternFrom a NLPat => PatternFrom (Elim' a) (Elim' NLPat)

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> Elim' a -> TCM (Elim' NLPat)

type ConInfo = ConOrigin

data Term

Raw values.

Def is used for both defined and undefined constants. Assume there is a type declaration and a definition for every constant, even if the definition is an empty list of clauses.

Constructors

Var !Int Elims

x es neutral

Lam ArgInfo (Abs Term)

Terms are beta normal. Relevance is ignored

Lit Literal

Def QName Elims

f es, possibly a delta/iota-redex

Con ConHead ConInfo Elims

c es or record { fs = es } es allows only Apply and IApply eliminations, and IApply only for data constructors.

Pi (Dom Type) (Abs Type)

dependent or non-dependent function space

Sort Sort

Level Level

MetaV !MetaId Elims

DontCare Term

Irrelevant stuff in relevant position, but created in an irrelevant context. Basically, an internal version of the irrelevance axiom .irrAx : .A -> A.

Instances

Eq Term

Syntactic Term equality, ignores stuff below DontCare and sharing.

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Data Term

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Term -> c Term

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Term

toConstr :: Term -> Constr

dataTypeOf :: Term -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Term)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term)

gmapT :: (forall b. Data b => b -> b) -> Term -> Term

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r

gmapQ :: (forall d. Data d => d -> u) -> Term -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Term -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Term -> m Term

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term

Ord Term

Defined in Agda.TypeChecking.Substitute

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

Show Term

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Term -> ShowS

show :: Term -> String

showList :: [Term] -> ShowS

NFData Type

Defined in Agda.Syntax.Internal

Methods

rnf :: Type -> ()

NFData Term

Defined in Agda.Syntax.Internal

Methods

rnf :: Term -> ()

Pretty Type

Defined in Agda.Syntax.Internal

Methods

pretty :: Type -> Doc

prettyPrec :: Int -> Type -> Doc

prettyList :: [Type] -> Doc

Pretty Term

Defined in Agda.Syntax.Internal

Methods

pretty :: Term -> Doc

prettyPrec :: Int -> Term -> Doc

prettyList :: [Term] -> Doc

Pretty CompiledClauses

Defined in Agda.TypeChecking.CompiledClause

Methods

pretty :: CompiledClauses -> Doc

prettyPrec :: Int -> CompiledClauses -> Doc

prettyList :: [CompiledClauses] -> Doc

KillRange Substitution

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Substitution

KillRange Term

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Term

KillRange CompiledClauses

Defined in Agda.TypeChecking.CompiledClause

Methods

killRange :: KillRangeT CompiledClauses

TermSize Term

Defined in Agda.Syntax.Internal

Methods

termSize :: Term -> Int

tsize :: Term -> Sum Int

IsProjElim Elim

Defined in Agda.Syntax.Internal

Methods

isProjElim :: Elim -> Maybe (ProjOrigin, QName)

TelToArgs ListTel

Defined in Agda.Syntax.Internal

Methods

telToArgs :: ListTel -> [Arg ArgName]

TelToArgs Telescope

Defined in Agda.Syntax.Internal

Methods

telToArgs :: Telescope -> [Arg ArgName]

DeBruijn Term

We can substitute Terms for variables.

Defined in Agda.TypeChecking.Substitute.DeBruijn

Methods

deBruijnVar :: Int -> Term

debruijnNamedVar :: String -> Int -> Term

deBruijnView :: Term -> Maybe Int

PrecomputeFreeVars Type

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Type -> FV Type

PrecomputeFreeVars Term

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Term -> FV Term

Free Term

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => Term -> FreeM c

Abstract Telescope

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Telescope -> Telescope

Abstract Type

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Type -> Type

Abstract Term

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Term -> Term

Abstract CompiledClauses

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> CompiledClauses -> CompiledClauses

Apply Term

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Term -> Args -> Term

applyE :: Term -> Elims -> Term

Apply CompiledClauses

Defined in Agda.TypeChecking.Substitute

Methods

apply :: CompiledClauses -> Args -> CompiledClauses

applyE :: CompiledClauses -> Elims -> CompiledClauses

TermLike Type

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Type -> m Type

foldTerm :: Monoid m => (Term -> m) -> Type -> m

TermLike Term

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Term -> m Term

foldTerm :: Monoid m => (Term -> m) -> Term -> m

GetDefs Type

Defined in Agda.Syntax.Internal.Defs

Methods

getDefs :: MonadGetDefs m => Type -> m ()

GetDefs Term

Defined in Agda.Syntax.Internal.Defs

Methods

getDefs :: MonadGetDefs m => Term -> m ()

Free Type

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: Type -> FreeT

Free Term

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: Term -> FreeT

TeleNoAbs ListTel

Defined in Agda.TypeChecking.Substitute

Methods

teleNoAbs :: ListTel -> Term -> Term

TeleNoAbs Telescope

Defined in Agda.TypeChecking.Substitute

Methods

teleNoAbs :: Telescope -> Term -> Term

EmbPrj Term

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Term -> S Int32

icod_ :: Term -> S Int32

value :: Int32 -> R Term

EmbPrj CompiledClauses

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CompiledClauses -> S Int32

icod_ :: CompiledClauses -> S Int32

value :: Int32 -> R CompiledClauses

PrettyTCM Telescope

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Telescope -> TCM Doc

PrettyTCM Type

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Type -> TCM Doc

PrettyTCM Elim

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Elim -> TCM Doc

PrettyTCM Term

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Term -> TCM Doc

DropArgs Telescope

NOTE: This creates telescopes with unbound de Bruijn indices.

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Telescope -> Telescope

DropArgs Term

Use for dropping initial lambdas in clause bodies. NOTE: does not reduce term, need lambdas to be present.

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Term -> Term

DropArgs CompiledClauses

To drop the first n arguments in a compiled clause, we reduce the split argument indices by n and drop n arguments from the bodies. NOTE: this only works for non-recursive functions, we are not dropping arguments to recursive calls in bodies.

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> CompiledClauses -> CompiledClauses

NamesIn Term

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Term -> Set QName

NamesIn CompiledClauses

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: CompiledClauses -> Set QName

IsSizeType Term

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

isSizeType :: Term -> TCM (Maybe BoundedSize)

AddContext Telescope

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => Telescope -> tcm a -> tcm a

contextSize :: Telescope -> Nat

UnFreezeMeta Type

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: Type -> TCM ()

UnFreezeMeta Term

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: Term -> TCM ()

IsInstantiatedMeta Term

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: Term -> TCM Bool

MentionsMeta Type

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMeta :: MetaId -> Type -> Bool

MentionsMeta Elim

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMeta :: MetaId -> Elim -> Bool

MentionsMeta Term

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMeta :: MetaId -> Term -> Bool

InstantiateFull Substitution

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Substitution -> ReduceM Substitution

InstantiateFull Term

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Term -> ReduceM Term

InstantiateFull CompiledClauses

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: CompiledClauses -> ReduceM CompiledClauses

Normalise Type

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Type -> ReduceM Type

Normalise Elim

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Elim -> ReduceM Elim

Normalise Term

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Term -> ReduceM Term

Simplify Type

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Type -> ReduceM Type

Simplify Elim

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Elim -> ReduceM Elim

Simplify Term

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Term -> ReduceM Term

Reduce Telescope

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Telescope -> ReduceM Telescope

reduceB' :: Telescope -> ReduceM (Blocked Telescope)

Reduce Type

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Type -> ReduceM Type

reduceB' :: Type -> ReduceM (Blocked Type)

Reduce Elim

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Elim -> ReduceM Elim

reduceB' :: Elim -> ReduceM (Blocked Elim)

Reduce Term

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Term -> ReduceM Term

reduceB' :: Term -> ReduceM (Blocked Term)

Instantiate Telescope

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Telescope -> ReduceM Telescope

Instantiate Type

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Type -> ReduceM Type

Instantiate Elim

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Elim -> ReduceM Elim

Instantiate Term

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Term -> ReduceM Term

SynEq Type

Syntactic equality ignores sorts.

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Type -> Type -> SynEqM (Type, Type)

synEq' :: Type -> Type -> SynEqM (Type, Type)

SynEq Term

Syntactic term equality ignores DontCare stuff.

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Term -> Term -> SynEqM (Term, Term)

synEq' :: Term -> Term -> SynEqM (Term, Term)

SubstWithOrigin Term

Defined in Agda.TypeChecking.DisplayForm

Methods

substWithOrigin :: Substitution -> [WithOrigin Term] -> Term -> Term

Match Term

Defined in Agda.TypeChecking.DisplayForm

Methods

match :: Term -> Term -> MaybeT TCM [WithOrigin Term]

HasPolarity Type

Defined in Agda.TypeChecking.Polarity

Methods

polarities :: Nat -> Type -> TCM [Polarity]

HasPolarity Term

Defined in Agda.TypeChecking.Polarity

Methods

polarities :: Nat -> Term -> TCM [Polarity]

UsableRelevance Term

Defined in Agda.TypeChecking.Irrelevance

Methods

usableRel :: Relevance -> Term -> TCM Bool

ForcedVariables Term

Assumes that the term is in normal form.

Defined in Agda.TypeChecking.Forcing

Methods

forcedVariables :: Term -> [(Modality, Nat)]

ComputeOccurrences Type

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Type -> OccM OccurrencesBuilder

ComputeOccurrences Term

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Term -> OccM OccurrencesBuilder

ToTerm Type

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Type -> Term)

toTermR :: TCM (Type -> ReduceM Term)

ToTerm Term

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Term -> Term)

toTermR :: TCM (Term -> ReduceM Term)

PrimTerm Type

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Type -> TCM Term

FoldRigid Type

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Type -> TCM m

FoldRigid Term

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Term -> TCM m

Occurs Type

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Type -> TCM Type

metaOccurs :: MetaId -> Type -> TCM ()

Occurs Term

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Term -> TCM Term

metaOccurs :: MetaId -> Term -> TCM ()

ReduceAndEtaContract Term

Defined in Agda.TypeChecking.MetaVars

Methods

reduceAndEtaContract :: Term -> TCM Term

NoProjectedVar Term

Defined in Agda.TypeChecking.MetaVars

Methods

noProjectedVar :: Term -> Either ProjVarExc ()

AbsTerm Type

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Type -> Type

AbsTerm Term

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Term -> Term

IsPrefixOf Elims

Defined in Agda.TypeChecking.Abstract

Methods

isPrefixOf :: Elims -> Elims -> Maybe Elims

IsPrefixOf Term

Defined in Agda.TypeChecking.Abstract

Methods

isPrefixOf :: Term -> Term -> Maybe Elims

IsPrefixOf Args

Defined in Agda.TypeChecking.Abstract

Methods

isPrefixOf :: Args -> Args -> Maybe Elims

UniverseBi Elims Pattern

Defined in Agda.Syntax.Internal

Methods

universeBi :: Elims -> [Pattern]

UniverseBi Elims Term

Defined in Agda.Syntax.Internal

Methods

universeBi :: Elims -> [Term]

UniverseBi Args Pattern

Defined in Agda.Syntax.Internal

Methods

universeBi :: Args -> [Pattern]

UniverseBi Args Term

Defined in Agda.Syntax.Internal

Methods

universeBi :: Args -> [Term]

Subst Term ()

Defined in Agda.TypeChecking.Substitute

Methods

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

Subst Term String

Defined in Agda.TypeChecking.Substitute

Methods

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

Subst Term Range

Defined in Agda.TypeChecking.Substitute

Methods

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

Subst Term QName

Defined in Agda.TypeChecking.Substitute.Class

Methods

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

Subst Term Name

Defined in Agda.TypeChecking.Substitute

Methods

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

Subst Term EqualityView

Defined in Agda.TypeChecking.Substitute

Methods

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

Subst Term ConPatternInfo

Defined in Agda.TypeChecking.Substitute

Methods

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

Subst Term Pattern

Defined in Agda.TypeChecking.Substitute

Methods

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

Subst Term LevelAtom

Defined in Agda.TypeChecking.Substitute

Methods

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

Subst Term PlusLevel

Defined in Agda.TypeChecking.Substitute

Methods

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

Subst Term Level

Defined in Agda.TypeChecking.Substitute

Methods

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

Subst Term Sort

Defined in Agda.TypeChecking.Substitute

Methods

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

Subst Term Term

Defined in Agda.TypeChecking.Substitute

Methods

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

Subst Term ProblemEq

Defined in Agda.TypeChecking.Substitute

Methods

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

Subst Term Candidate

Defined in Agda.TypeChecking.Substitute

Methods

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

Subst Term DisplayTerm

Defined in Agda.TypeChecking.Substitute

Methods

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

Subst Term DisplayForm

Defined in Agda.TypeChecking.Substitute

Methods

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

Subst Term Constraint

Defined in Agda.TypeChecking.Substitute

Methods

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

Subst Term AbsurdPattern

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

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

Subst Term DotPattern

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

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

Subst Term AsBinding

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

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

Subst Term SizeConstraint

Defined in Agda.TypeChecking.SizedTypes.Solve

Methods

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

Subst Term SizeMeta

Defined in Agda.TypeChecking.SizedTypes.Solve

Methods

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

Reify Telescope Telescope

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Telescope0 -> TCM Telescope

reifyWhen :: Bool -> Telescope0 -> TCM Telescope

Reify Type Expr

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Type -> TCM Expr

reifyWhen :: Bool -> Type -> TCM Expr

Reify Term Expr

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Term -> TCM Expr

reifyWhen :: Bool -> Term -> TCM Expr

Match NLPType Type

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> NLPType -> Type -> NLM ()

Match NLPat Term

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> NLPat -> Term -> NLM ()

PatternFrom Type NLPType

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> Type -> TCM NLPType

PatternFrom Term NLPat

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> Term -> TCM NLPat

Conversion TOM Type (MExp O)

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (MExp O)

Conversion TOM Term (MExp O)

Defined in Agda.Auto.Convert

Methods

convert :: Term -> TOM (MExp O)

Conversion TOM Args (MM (ArgList O) (RefInfo O))

Defined in Agda.Auto.Convert

Methods

convert :: Args -> TOM (MM (ArgList O) (RefInfo O))

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

Defined in Agda.TypeChecking.Substitute

Methods

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

Subst Term (Problem a)

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

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

DeBruijn (Pattern' a) => TermToPattern Term (Pattern' a)

Defined in Agda.TypeChecking.Patterns.Internal

Methods

termToPattern :: Term -> TCM (Pattern' a)

Conversion MOT (Exp O) Type

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Type

Conversion MOT (Exp O) Term

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Term

Subst Term (SizeExpr' NamedRigid SizeMeta)

Only for raise.

Defined in Agda.TypeChecking.SizedTypes.Solve

Methods

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

Eq (Substitution' Term)

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Ord (Substitution' Term)

Defined in Agda.TypeChecking.Substitute

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

SgTel (Dom (ArgName, Type))

Defined in Agda.Syntax.Internal

Methods

sgTel :: Dom (ArgName, Type) -> Telescope

SgTel (Dom Type)

Defined in Agda.Syntax.Internal

Methods

sgTel :: Dom Type -> Telescope

AddContext (Dom (String, Type))

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom (String, Type) -> tcm a -> tcm a

contextSize :: Dom (String, Type) -> Nat

AddContext (Dom (Name, Type))

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom (Name, Type) -> tcm a -> tcm a

contextSize :: Dom (Name, Type) -> Nat

AddContext (Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom Type -> tcm a -> tcm a

contextSize :: Dom Type -> Nat

AddContext (KeepNames Telescope)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => KeepNames Telescope -> tcm a -> tcm a

contextSize :: KeepNames Telescope -> Nat

SubstWithOrigin (Arg Term)

Defined in Agda.TypeChecking.DisplayForm

Methods

substWithOrigin :: Substitution -> [WithOrigin Term] -> Arg Term -> Arg Term

UniverseBi [Term] Term

Defined in Agda.Syntax.Internal

Methods

universeBi :: [Term] -> [Term]

SgTel (ArgName, Dom Type)

Defined in Agda.Syntax.Internal

Methods

sgTel :: (ArgName, Dom Type) -> Telescope

AddContext ([WithHiding Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => ([WithHiding Name], Dom Type) -> tcm a -> tcm a

contextSize :: ([WithHiding Name], Dom Type) -> Nat

AddContext ([Name], Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => ([Name], Dom Type) -> tcm a -> tcm a

contextSize :: ([Name], Dom Type) -> Nat

AddContext (String, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => (String, Dom Type) -> tcm a -> tcm a

contextSize :: (String, Dom Type) -> Nat

AddContext (Name, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => (Name, Dom Type) -> tcm a -> tcm a

contextSize :: (Name, Dom Type) -> Nat

AddContext (KeepNames String, Dom Type)

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => (KeepNames String, Dom Type) -> tcm a -> tcm a

contextSize :: (KeepNames String, Dom Type) -> Nat

UniverseBi ([Type], [Clause]) Pattern

Defined in Agda.Syntax.Internal

Methods

universeBi :: ([Type], [Clause]) -> [Pattern]

UniverseBi ([Type], [Clause]) Term

Defined in Agda.Syntax.Internal

Methods

universeBi :: ([Type], [Clause]) -> [Term]

class LensConName a where

Minimal complete definition

getConName

Methods

getConName :: a -> QName

setConName :: QName -> a -> a

mapConName :: (QName -> QName) -> a -> a

Instances

LensConName ConHead

Defined in Agda.Syntax.Internal

Methods

getConName :: ConHead -> QName

setConName :: QName -> ConHead -> ConHead

mapConName :: (QName -> QName) -> ConHead -> ConHead

data ConHead

Store the names of the record fields in the constructor. This allows reduction of projection redexes outside of TCM. For instance, during substitution and application.

Constructors

ConHead

Fields

• conName :: QName

  The name of the constructor.

• conInductive :: Induction

  Record constructors can be coinductive.

• conFields :: [QName]

  The name of the record fields. Empty list for data constructors. Arg is not needed here since it is stored in the constructor args.

Instances

Eq ConHead

Defined in Agda.Syntax.Internal

Methods

(==) :: ConHead -> ConHead -> Bool

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

Data ConHead

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConHead -> c ConHead

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConHead

toConstr :: ConHead -> Constr

dataTypeOf :: ConHead -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConHead)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConHead)

gmapT :: (forall b. Data b => b -> b) -> ConHead -> ConHead

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConHead -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConHead -> r

gmapQ :: (forall d. Data d => d -> u) -> ConHead -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ConHead -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConHead -> m ConHead

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConHead -> m ConHead

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConHead -> m ConHead

Ord ConHead

Defined in Agda.Syntax.Internal

Methods

compare :: ConHead -> ConHead -> Ordering

(<) :: ConHead -> ConHead -> Bool

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

(>) :: ConHead -> ConHead -> Bool

(>=) :: ConHead -> ConHead -> Bool

max :: ConHead -> ConHead -> ConHead

min :: ConHead -> ConHead -> ConHead

Show ConHead

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> ConHead -> ShowS

show :: ConHead -> String

showList :: [ConHead] -> ShowS

Pretty ConHead

Defined in Agda.Syntax.Internal

Methods

pretty :: ConHead -> Doc

prettyPrec :: Int -> ConHead -> Doc

prettyList :: [ConHead] -> Doc

KillRange ConHead

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT ConHead

SetRange ConHead

Defined in Agda.Syntax.Internal

Methods

setRange :: Range -> ConHead -> ConHead

HasRange ConHead

Defined in Agda.Syntax.Internal

Methods

getRange :: ConHead -> Range

LensConName ConHead

Defined in Agda.Syntax.Internal

Methods

getConName :: ConHead -> QName

setConName :: QName -> ConHead -> ConHead

mapConName :: (QName -> QName) -> ConHead -> ConHead

EmbPrj ConHead

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ConHead -> S Int32

icod_ :: ConHead -> S Int32

value :: Int32 -> R ConHead

PrettyTCM ConHead

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: ConHead -> TCM Doc

NamesIn ConHead

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: ConHead -> Set QName

InstantiateFull ConHead

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: ConHead -> ReduceM ConHead

type NamedArgs = [NamedArg Term]

type Args = [Arg Term]

Type of argument lists.

argNameToString :: ArgName -> String

stringToArgName :: String -> ArgName

appendArgNames :: ArgName -> ArgName -> ArgName

nameToArgName :: Name -> ArgName

stuckOn :: Elim -> NotBlocked -> NotBlocked

When trying to reduce f es, on match failed on one elimination e ∈ es that came with info r :: NotBlocked. stuckOn e r produces the new NotBlocked info.

MissingClauses must be propagated, as this is blockage that can be lifted in the future (as more clauses are added).

StuckOn e0 is also propagated, since it provides more precise information as StuckOn e (as e0 is the original reason why reduction got stuck and usually a subterm of e). An information like StuckOn (Apply (Arg info (Var i []))) (stuck on a variable) could be used by the lhs/coverage checker to trigger a split on that (pattern) variable.

In the remaining cases for r, we are terminally stuck due to StuckOn e. Propagating AbsurdMatch does not seem useful.

Underapplied must not be propagated, as this would mean that f es is underapplied, which is not the case (it is stuck). Note that Underapplied can only arise when projection patterns were missing to complete the original match (in e). (Missing ordinary pattern would mean the e is of function type, but we cannot match against something of function type.)

clausePats :: Clause -> [Arg DeBruijnPattern]

patVarNameToString :: PatVarName -> String

nameToPatVarName :: Name -> PatVarName

varP :: a -> Pattern' a

dotP :: Term -> Pattern' a

namedVarP :: PatVarName -> Named_ Pattern

namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern

noConPatternInfo :: ConPatternInfo

toConPatternInfo :: ConInfo -> ConPatternInfo

Build partial ConPatternInfo from ConInfo

fromConPatternInfo :: ConPatternInfo -> ConInfo

Build ConInfo from ConPatternInfo.

patternOrigin :: Pattern' x -> Maybe PatOrigin

Retrieve the origin of a pattern

properlyMatching :: DeBruijnPattern -> Bool

Does the pattern perform a match that could fail?

isEqualityType :: EqualityView -> Bool

absurdBody :: Abs Term

Absurd lambdas are internally represented as identity with variable name "()".

isAbsurdBody :: Abs Term -> Bool

absurdPatternName :: PatVarName

isAbsurdPatternName :: PatVarName -> Bool

var :: Nat -> Term

An unapplied variable.

dontCare :: Term -> Term

Add DontCare is it is not already a DontCare.

typeDontCare :: Type

A dummy type.

topSort :: Type

Top sort (Setomega).

sort :: Sort -> Type

varSort :: Int -> Sort

levelSuc :: Level -> Level

mkType :: Integer -> Sort

isSort :: Term -> Maybe Sort

impossibleTerm :: String -> Int -> Term

hackReifyToMeta :: Term

isHackReifyToMeta :: Term -> Bool

mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a)

A traversal for the names in a telescope.

mapAbsNames :: (ArgName -> ArgName) -> Tele a -> Tele a

replaceEmptyName :: ArgName -> Tele a -> Tele a

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

telFromList :: ListTel -> Telescope

Convert a list telescope to a telescope.

telToList :: Telescope -> ListTel

Convert a telescope to its list form.

blockingMeta :: Blocked t -> Maybe MetaId

blocked :: MetaId -> a -> Blocked a

notBlocked :: a -> Blocked a

stripDontCare :: Term -> Term

Removing a topmost DontCare constructor.

arity :: Type -> Nat

Doesn't do any reduction.

notInScopeName :: ArgName -> ArgName

Make a name that is not in scope.

unNotInScopeName :: ArgName -> ArgName

Remove the dot from a notInScopeName. This is used when printing function types that have abstracted over not-in-scope names.

unSpine :: Term -> Term

Convert top-level postfix projections into prefix projections.

unSpine' :: (ProjOrigin -> Bool) -> Term -> Term

Convert Proj projection eliminations according to their ProjOrigin into Def projection applications.

hasElims :: Term -> Maybe (Elims -> Term, Elims)

A view distinguishing the neutrals Var, Def, and MetaV which can be projected.

argFromElim :: Elim' a -> Arg a

Drop Apply constructor. (Unsafe!)

isApplyElim :: Elim' a -> Maybe (Arg a)

Drop Apply constructor. (Safe)

isApplyElim' :: Empty -> Elim' a -> Arg a

allApplyElims :: [Elim' a] -> Maybe [Arg a]

Drop Apply constructors. (Safe)

splitApplyElims :: [Elim' a] -> ([Arg a], [Elim' a])

Split at first non-Apply

dropProjElims :: IsProjElim e => [e] -> [e]

Discard Proj f entries.

argsFromElims :: Elims -> Args

Discards Proj f entries.

allProjElims :: Elims -> Maybe [(ProjOrigin, QName)]

Drop Proj constructors. (Safe)

pDom :: LensHiding a => a -> Doc -> Doc

module Agda.Syntax.Abstract.Name

newtype MetaId

A meta variable identifier is just a natural number.

Constructors

MetaId

Fields

• metaId :: Nat

Instances

Enum MetaId

Defined in Agda.Syntax.Common

Methods

succ :: MetaId -> MetaId

pred :: MetaId -> MetaId

toEnum :: Int -> MetaId

fromEnum :: MetaId -> Int

enumFrom :: MetaId -> [MetaId]

enumFromThen :: MetaId -> MetaId -> [MetaId]

enumFromTo :: MetaId -> MetaId -> [MetaId]

enumFromThenTo :: MetaId -> MetaId -> MetaId -> [MetaId]

Eq MetaId

Defined in Agda.Syntax.Common

Methods

(==) :: MetaId -> MetaId -> Bool

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

Integral MetaId

Defined in Agda.Syntax.Common

Methods

quot :: MetaId -> MetaId -> MetaId

rem :: MetaId -> MetaId -> MetaId

div :: MetaId -> MetaId -> MetaId

mod :: MetaId -> MetaId -> MetaId

quotRem :: MetaId -> MetaId -> (MetaId, MetaId)

divMod :: MetaId -> MetaId -> (MetaId, MetaId)

toInteger :: MetaId -> Integer

Data MetaId

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MetaId -> c MetaId

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MetaId

toConstr :: MetaId -> Constr

dataTypeOf :: MetaId -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MetaId)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MetaId)

gmapT :: (forall b. Data b => b -> b) -> MetaId -> MetaId

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MetaId -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MetaId -> r

gmapQ :: (forall d. Data d => d -> u) -> MetaId -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> MetaId -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId

Num MetaId

Defined in Agda.Syntax.Common

Methods

(+) :: MetaId -> MetaId -> MetaId

(-) :: MetaId -> MetaId -> MetaId

(*) :: MetaId -> MetaId -> MetaId

negate :: MetaId -> MetaId

abs :: MetaId -> MetaId

signum :: MetaId -> MetaId

fromInteger :: Integer -> MetaId

Ord MetaId

Defined in Agda.Syntax.Common

Methods

compare :: MetaId -> MetaId -> Ordering

(<) :: MetaId -> MetaId -> Bool

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

(>) :: MetaId -> MetaId -> Bool

(>=) :: MetaId -> MetaId -> Bool

max :: MetaId -> MetaId -> MetaId

min :: MetaId -> MetaId -> MetaId

Real MetaId

Defined in Agda.Syntax.Common

Methods

toRational :: MetaId -> Rational

Show MetaId

Show non-record version of this newtype.

Defined in Agda.Syntax.Common

Methods

showsPrec :: Int -> MetaId -> ShowS

show :: MetaId -> String

showList :: [MetaId] -> ShowS

NFData MetaId

Defined in Agda.Syntax.Common

Methods

rnf :: MetaId -> ()

Pretty MetaId

Defined in Agda.Syntax.Common

Methods

pretty :: MetaId -> Doc

prettyPrec :: Int -> MetaId -> Doc

prettyList :: [MetaId] -> Doc

GetDefs MetaId

Defined in Agda.Syntax.Internal.Defs

Methods

getDefs :: MonadGetDefs m => MetaId -> m ()

HasFresh MetaId

Defined in Agda.TypeChecking.Monad.Base

Methods

freshLens :: Lens' MetaId TCState

nextFresh' :: MetaId -> MetaId

EmbPrj MetaId

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: MetaId -> S Int32

icod_ :: MetaId -> S Int32

value :: Int32 -> R MetaId

PrettyTCM MetaId

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MetaId -> TCM Doc

UnFreezeMeta MetaId

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MetaId -> TCM ()

IsInstantiatedMeta MetaId

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: MetaId -> TCM Bool

FromTerm MetaId

Defined in Agda.TypeChecking.Primitive

Methods

fromTerm :: TCM (FromTermFunction MetaId)

ToTerm MetaId

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (MetaId -> Term)

toTermR :: TCM (MetaId -> ReduceM Term)

PrimTerm MetaId

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: MetaId -> TCM Term

Unquote MetaId

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM MetaId

Reify MetaId Expr

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MetaId -> TCM Expr

reifyWhen :: Bool -> MetaId -> TCM Expr