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

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Internal

Synopsis

Documentation

class TermSize a where Source #

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

tsize :: a -> Sum Int Source #

Instances
TermSize LevelAtom Source # 
Instance details

Defined in Agda.Syntax.Internal

TermSize PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

TermSize Level Source # 
Instance details

Defined in Agda.Syntax.Internal

TermSize Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

TermSize Term Source # 
Instance details

Defined in Agda.Syntax.Internal

(Foldable t, TermSize a) => TermSize (t a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

termSize :: t a -> Int Source #

tsize :: t a -> Sum Int Source #

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

Defined in Agda.Syntax.Internal

class IsProjElim e where Source #

Instances
IsProjElim Elim Source # 
Instance details

Defined in Agda.Syntax.Internal

IsProjElim e => IsProjElim (MaybeReduced e) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

class Suggest a b where Source #

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

Methods

suggest :: a -> b -> String Source #

Instances
Suggest String String Source # 
Instance details

Defined in Agda.Syntax.Internal

Suggest String (Abs b) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

suggest :: String -> Abs b -> String Source #

Suggest Name (Abs b) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

suggest :: Name -> Abs b -> String Source #

Suggest (Abs a) (Abs b) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

class SgTel a where Source #

Constructing a singleton telescope.

Methods

sgTel :: a -> Telescope Source #

Instances
SgTel (Dom (ArgName, Type)) Source # 
Instance details

Defined in Agda.Syntax.Internal

SgTel (Dom Type) Source # 
Instance details

Defined in Agda.Syntax.Internal

SgTel (ArgName, Dom Type) Source # 
Instance details

Defined in Agda.Syntax.Internal

class TelToArgs a where Source #

Drop the types from a telescope.

Methods

telToArgs :: a -> [Arg ArgName] Source #

Instances
TelToArgs ListTel Source # 
Instance details

Defined in Agda.Syntax.Internal

TelToArgs Telescope Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Telescope as list.

data PathView Source #

View type as path type.

Constructors

PathType 

Fields

OType Type

reduced

data EqualityView Source #

View type as equality type.

Constructors

EqualityType 

Fields

OtherType Type

reduced

Instances
Free EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

TermLike EqualityView Source # 
Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

PrettyTCM EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

InstantiateFull EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Subst Term EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

data Substitution' a Source #

Substitutions.

Constructors

IdS

Identity substitution. Γ ⊢ IdS : Γ

EmptyS Empty

Empty substitution, lifts from the empty context. First argument is (throwImpossible (Impossible "srcfullAgdaSyntaxInternal.hs" 610)). 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" 623)). Apply this to a term which does not contain variable 0 to lower all de Bruijn indices by one. Γ ⊢ ρ : Δ --------------------------- Γ ⊢ Strengthen ρ : Δ, A

Wk !Int (Substitution' a)

Weakning substitution, lifts to an extended context. Γ ⊢ ρ : Δ ------------------- Γ, Ψ ⊢ Wk |Ψ| ρ : Δ

Lift !Int (Substitution' a)

Lifting substitution. Use this to go under a binder. Lift 1 ρ == var 0 :# Wk 1 ρ. Γ ⊢ ρ : Δ ------------------------- Γ, Ψρ ⊢ Lift |Ψ| ρ : Δ, Ψ

Instances
Functor Substitution' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

Foldable Substitution' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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

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

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

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

null :: Substitution' a -> Bool #

length :: Substitution' a -> Int #

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

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

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

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

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

Traversable Substitution' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

KillRange Substitution Source # 
Instance details

Defined in Agda.Syntax.Internal

InstantiateFull Substitution Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

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

Defined in Agda.TypeChecking.Substitute

Eq (Substitution' Term) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

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

Defined in Agda.Syntax.Internal

Methods

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

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

Defined in Agda.TypeChecking.Substitute

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

Defined in Agda.Syntax.Internal

Null (Substitution' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

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

Defined in Agda.TypeChecking.Pretty

class PatternVars a b | b -> a where Source #

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

Methods

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

Instances
PatternVars a b => PatternVars a [b] Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

PatternVars a (NamedArg (Pattern' a)) Source # 
Instance details

Defined in Agda.Syntax.Internal

PatternVars a (Arg (Pattern' a)) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

data ConPatternInfo Source #

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.

  • conPFallThrough :: Bool

    Should the match block on non-canonical terms or can it proceed to the catch-all clause?

  • 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 Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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 Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange ConPatternInfo Source # 
Instance details

Defined in Agda.Syntax.Internal

EmbPrj ConPatternInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

InstantiateFull ConPatternInfo Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise ConPatternInfo Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Subst Term ConPatternInfo Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

data DBPatVar Source #

Type used when numbering pattern variables.

Constructors

DBPatVar 
Instances
Eq DBPatVar Source # 
Instance details

Defined in Agda.Syntax.Internal

Data DBPatVar Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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 Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty DBPatVar Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange DBPatVar Source # 
Instance details

Defined in Agda.Syntax.Internal

DeBruijn DeBruijnPattern Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

DeBruijn DBPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.DeBruijn

EmbPrj DBPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM DBPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

InstantiateFull DBPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise DBPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

UsableSizeVars DeBruijnPattern Source # 
Instance details

Defined in Agda.Termination.Monad

UsableSizeVars MaskedDeBruijnPatterns Source # 
Instance details

Defined in Agda.Termination.Monad

Subst DeBruijnPattern DeBruijnPattern Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

LabelPatVars Pattern DeBruijnPattern Int Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

UsableSizeVars [DeBruijnPattern] Source # 
Instance details

Defined in Agda.Termination.Monad

UsableSizeVars (Masked DeBruijnPattern) Source # 
Instance details

Defined in Agda.Termination.Monad

type Pattern Source #

Arguments

 = Pattern' PatVarName

The PatVarName is a name suggestion.

data Pattern' x Source #

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.

IApplyP PatOrigin Term Term x

Path elimination pattern, like VarP but keeps track of endpoints.

DefP PatOrigin QName [NamedArg (Pattern' x)]

Used for HITs, the QName should be the one from primHComp.

Instances
Functor Pattern' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

Foldable Pattern' Source # 
Instance details

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' Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

DeBruijn SplitPattern Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.Match

UsableSizeVars DeBruijnPattern Source # 
Instance details

Defined in Agda.Termination.Monad

UsableSizeVars MaskedDeBruijnPatterns Source # 
Instance details

Defined in Agda.Termination.Monad

UniverseBi Elims Pattern Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

universeBi :: Elims -> [Pattern] #

UniverseBi Args Pattern Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

universeBi :: Args -> [Pattern] #

Subst DeBruijnPattern DeBruijnPattern Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term Pattern Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst SplitPattern SplitPattern Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.Match

LabelPatVars Pattern DeBruijnPattern Int Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

PatternVars a (NamedArg (Pattern' a)) Source # 
Instance details

Defined in Agda.Syntax.Internal

PatternVars a (Arg (Pattern' a)) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

PatternLike a (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

Methods

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

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

MapNamedArgPattern a (NamedArg (Pattern' a)) Source #

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.

Instance details

Defined in Agda.Syntax.Internal.Pattern

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

Defined in Agda.TypeChecking.Patterns.Internal

Conversion TOM (Arg Pattern) (Pat O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

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

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

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Data x => Data (Pattern' x) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

show :: Pattern' x -> String #

showList :: [Pattern' x] -> ShowS #

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal

IsProjP (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Apply [NamedArg (Pattern' a)] Source #

Make sure we only drop variable patterns.

Instance details

Defined in Agda.TypeChecking.Substitute

CountPatternVars (Pattern' x) Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

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

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Pattern' a -> TCM Doc Source #

NamesIn (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Pattern' a -> Set QName Source #

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

Defined in Agda.TypeChecking.Reduce

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

Defined in Agda.TypeChecking.Reduce

NormaliseProjP (Pattern' x) Source # 
Instance details

Defined in Agda.TypeChecking.Records

UsableSizeVars [DeBruijnPattern] Source # 
Instance details

Defined in Agda.Termination.Monad

UsableSizeVars (Masked DeBruijnPattern) Source # 
Instance details

Defined in Agda.Termination.Monad

IsFlexiblePattern (Pattern' a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS

PatternVarModalities (Pattern' x) x Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

UniverseBi ([Type], [Clause]) Pattern Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

data PatOrigin Source #

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 Source # 
Instance details

Defined in Agda.Syntax.Internal

Data PatOrigin Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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 Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange PatOrigin Source # 
Instance details

Defined in Agda.Syntax.Internal

EmbPrj PatOrigin Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

type PatVarName = ArgName Source #

Pattern variables.

data Clause Source #

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

Instances
Data Clause Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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 Source # 
Instance details

Defined in Agda.Syntax.Internal

Null Clause Source #

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

Instance details

Defined in Agda.Syntax.Internal

Pretty Clause Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange Clause Source # 
Instance details

Defined in Agda.Syntax.Internal

HasRange Clause Source # 
Instance details

Defined in Agda.Syntax.Internal

Free Clause Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Abstract Clause Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Clause Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

GetDefs Clause Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

FunArity Clause Source #

Get the number of initial Apply patterns in a clause.

Instance details

Defined in Agda.Syntax.Internal.Pattern

Methods

funArity :: Clause -> Int Source #

Free Clause Source # 
Instance details

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: Clause -> FreeT

EmbPrj Clause Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM Clause Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

NamesIn Clause Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

DropArgs Clause Source #

NOTE: does not work for recursive functions.

Instance details

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Clause -> Clause Source #

DropArgs FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.DropArgs

InstantiateFull Clause Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

NormaliseProjP Clause Source # 
Instance details

Defined in Agda.TypeChecking.Records

ComputeOccurrences Clause Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Occurs Clause Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

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

Conversion TOM [Clause] [([Pat O], MExp O)] Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

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

FunArity [Clause] Source #

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

Instance details

Defined in Agda.Syntax.Internal.Pattern

Methods

funArity :: [Clause] -> Int Source #

PrettyTCM (QNamed Clause) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Reify (QNamed Clause) Clause Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

UniverseBi ([Type], [Clause]) Pattern Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

UniverseBi ([Type], [Clause]) Term Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

type NAPs = [NamedArg DeBruijnPattern] Source #

Named pattern arguments.

type Blocked_ = Blocked () Source #

Blocked t without the t.

data Blocked t Source #

Something where a meta variable may block reduction.

Instances
Functor Blocked Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

Applicative Blocked Source #

Blocking by a meta is dominant.

Instance details

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 Source # 
Instance details

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 Source # 
Instance details

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_ Source # 
Instance details

Defined in Agda.Syntax.Internal

Monoid Blocked_ Source # 
Instance details

Defined in Agda.Syntax.Internal

Subst t a => Subst t (Blocked a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

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

Defined in Agda.TypeChecking.Substitute

Methods

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

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

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

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Blocked t -> ShowS #

show :: Blocked t -> String #

showList :: [Blocked t] -> ShowS #

KillRange a => KillRange (Blocked a) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Blocked t -> Args -> Blocked t Source #

applyE :: Blocked t -> Elims -> Blocked t Source #

TermLike a => TermLike (Blocked a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

PrettyTCM a => PrettyTCM (Blocked a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Blocked a -> TCM Doc Source #

Instantiate a => Instantiate (Blocked a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

data NotBlocked Source #

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 Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Data NotBlocked Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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 Source # 
Instance details

Defined in Agda.Syntax.Internal

Semigroup NotBlocked Source #

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

Instance details

Defined in Agda.Syntax.Internal

Monoid NotBlocked Source # 
Instance details

Defined in Agda.Syntax.Internal

data LevelAtom Source #

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 Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Data LevelAtom Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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 Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Show LevelAtom Source # 
Instance details

Defined in Agda.Syntax.Internal

NFData LevelAtom Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: LevelAtom -> () #

Pretty LevelAtom Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange LevelAtom Source # 
Instance details

Defined in Agda.Syntax.Internal

TermSize LevelAtom Source # 
Instance details

Defined in Agda.Syntax.Internal

DeBruijn LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.DeBruijn

PrecomputeFreeVars LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

Free LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

TermLike LevelAtom Source # 
Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

GetDefs LevelAtom Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

Free LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: LevelAtom -> FreeT

EmbPrj LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

NamesIn LevelAtom Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

UnFreezeMeta LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

IsInstantiatedMeta LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

MentionsMeta LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

InstantiateFull LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

SynEq LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

ForceNotFree LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => LevelAtom -> m LevelAtom

UsableRelevance LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

ComputeOccurrences LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

HasPolarity LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Polarity

FoldRigid LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

AbsTerm LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Subst Term LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

data PlusLevel Source #

Constructors

ClosedLevel Integer

n, to represent Setₙ.

Plus Integer LevelAtom

n + ℓ.

Instances
Eq PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Data PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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 Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Show PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

NFData PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: PlusLevel -> () #

Pretty PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

TermSize PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

DeBruijn PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.DeBruijn

PrecomputeFreeVars PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

Free PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

TermLike PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

GetDefs PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

Free PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: PlusLevel -> FreeT

EmbPrj PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

NamesIn PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

UnFreezeMeta PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

IsInstantiatedMeta PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

MentionsMeta PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

InstantiateFull PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

SynEq PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

ForceNotFree PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => PlusLevel -> m PlusLevel

UsableRelevance PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

ComputeOccurrences PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

HasPolarity PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Polarity

FoldRigid PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

AbsTerm PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Subst Term PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

newtype Level Source #

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 Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Data Level Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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 Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Level -> ShowS #

show :: Level -> String #

showList :: [Level] -> ShowS #

NFData Level Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Level -> () #

Pretty Level Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange Level Source # 
Instance details

Defined in Agda.Syntax.Internal

TermSize Level Source # 
Instance details

Defined in Agda.Syntax.Internal

DeBruijn Level Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.DeBruijn

PrecomputeFreeVars Level Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

Free Level Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

TermLike Level Source # 
Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

GetDefs Level Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

Free Level Source # 
Instance details

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: Level -> FreeT

EmbPrj Level Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM Level Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Level -> TCM Doc Source #

NamesIn Level Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Level -> Set QName Source #

UnFreezeMeta Level Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: Level -> TCM () Source #

IsInstantiatedMeta Level Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

MentionsMeta Level Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

InstantiateFull Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

SynEq Level Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

ForceNotFree Level Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => Level -> m Level

Match Level Source # 
Instance details

Defined in Agda.TypeChecking.DisplayForm

UsableModality Level Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

UsableRelevance Level Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

ComputeOccurrences Level Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

HasPolarity Level Source # 
Instance details

Defined in Agda.TypeChecking.Polarity

Methods

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

FoldRigid Level Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs Level Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

AbsTerm Level Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Level -> Level Source #

Subst Term Level Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Reify Level Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Match () NLPat Level Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

data Sort Source #

Sorts.

Constructors

Type Level

Set ℓ.

Prop Level

Prop ℓ.

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 
DefS QName Elims

A postulated sort.

DummyS String

A (part of a) term or type which is only used for internal purposes. Replaces the abuse of Prop for a dummy sort. The String typically describes the location where we create this dummy, but can contain other information as well.

Instances
Eq Sort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Data Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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 Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Sort -> ShowS #

show :: Sort -> String #

showList :: [Sort] -> ShowS #

NFData Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Sort -> () #

Pretty Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

TermSize Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

PrecomputeFreeVars Sort Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

Free Sort Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Abstract Sort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Sort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Sort -> Args -> Sort Source #

applyE :: Sort -> Elims -> Sort Source #

TermLike Sort Source # 
Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Sort -> m Sort Source #

foldTerm :: Monoid m => (Term -> m) -> Sort -> m Source #

GetDefs Sort Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

Free Sort Source # 
Instance details

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: Sort -> FreeT

EmbPrj Sort Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM Sort Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Sort -> TCM Doc Source #

NamesIn Sort Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Sort -> Set QName Source #

UnFreezeMeta Sort Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: Sort -> TCM () Source #

MentionsMeta Sort Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

InstantiateFull Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

SynEq Sort Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

ForceNotFree Sort Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => Sort -> m Sort

Match Sort Source # 
Instance details

Defined in Agda.TypeChecking.DisplayForm

UsableModality Sort Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

UsableRelevance Sort Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

FoldRigid Sort Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs Sort Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

AbsTerm Sort Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Sort -> Sort Source #

Subst Term Sort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Reify Sort Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Match () NLPat Sort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

PatternFrom () Sort NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> () -> Sort -> TCM NLPat Source #

data Tele a Source #

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 Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

Foldable Tele Source # 
Instance details

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 Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Internal

Abstract Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

PrettyTCM Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

TeleNoAbs Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

DropArgs Telescope Source #

NOTE: This creates telescopes with unbound de Bruijn indices.

Instance details

Defined in Agda.TypeChecking.DropArgs

AddContext Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Telescope -> Nat Source #

Reduce Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reify Telescope Telescope Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

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

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Defined in Agda.TypeChecking.Substitute

Methods

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

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

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

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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) Source # 
Instance details

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

Defined in Agda.Syntax.Internal

Methods

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

show :: Tele a -> String #

showList :: [Tele a] -> ShowS #

Null (Tele a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

empty :: Tele a Source #

null :: Tele a -> Bool Source #

Pretty a => Pretty (Tele (Dom a)) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Tele (Dom a) -> Doc Source #

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

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

Sized (Tele a) Source #

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

Instance details

Defined in Agda.Syntax.Internal

Methods

size :: Tele a -> Int Source #

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Tele a -> Args -> Tele a Source #

applyE :: Tele a -> Elims -> Tele a Source #

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

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Tele a -> m (Tele a) Source #

foldTerm :: Monoid m => (Term -> m) -> Tele a -> m Source #

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

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: Tele a -> FreeT

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Tele a -> S Int32 Source #

icod_ :: Tele a -> S Int32 Source #

value :: Int32 -> R (Tele a) Source #

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

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Tele a -> Set QName Source #

AddContext (KeepNames Telescope) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

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

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMeta :: MetaId -> Tele a -> Bool Source #

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

Defined in Agda.TypeChecking.Reduce

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Positivity

class LensSort a where Source #

Minimal complete definition

lensSort

Instances
LensSort a => LensSort (Dom a) Source # 
Instance details

Defined in Agda.Syntax.Internal

LensSort a => LensSort (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Internal

LensSort (Type' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal

data Type' a Source #

Types are terms with a sort annotation.

Constructors

El 

Fields

Instances
Functor Type' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

Foldable Type' Source # 
Instance details

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' Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Type -> () #

Decoration Type' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

Pretty Type Source # 
Instance details

Defined in Agda.Syntax.Internal

TelToArgs ListTel Source # 
Instance details

Defined in Agda.Syntax.Internal

TelToArgs Telescope Source # 
Instance details

Defined in Agda.Syntax.Internal

PrecomputeFreeVars Type Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

Abstract Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Type Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

TermLike Type Source # 
Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

GetDefs Type Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

Free Type Source # 
Instance details

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: Type -> FreeT

PrettyTCM Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Type Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Type -> TCM Doc Source #

TeleNoAbs ListTel Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

teleNoAbs :: ListTel -> Term -> Term Source #

TeleNoAbs Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

DropArgs Telescope Source #

NOTE: This creates telescopes with unbound de Bruijn indices.

Instance details

Defined in Agda.TypeChecking.DropArgs

AddContext Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Telescope -> Nat Source #

UnFreezeMeta Type Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: Type -> TCM () Source #

MentionsMeta Type Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Normalise Type Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify Type Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Type Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate Type Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

SynEq Type Source #

Syntactic equality ignores sorts.

Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

ForceNotFree Type Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => Type -> m Type

ComputeOccurrences Type Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

HasPolarity Type Source # 
Instance details

Defined in Agda.TypeChecking.Polarity

Methods

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

FoldRigid Type Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs Type Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

ToTerm Type Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimTerm Type Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Type -> TCM Term Source #

AbsTerm Type Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Type -> Type Source #

Reify Telescope Telescope Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Reify Type Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Match () NLPType Type Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

Match Type NLPat Term Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM () Source #

PatternFrom () Type NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> () -> Type -> TCM NLPType Source #

PatternFrom Type Term NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Conversion TOM Type (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (MExp O) Source #

Subst Term a => Subst Term (Type' a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Conversion MOT (Exp O) Type Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Type Source #

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

Syntactic Type equality, ignores sort annotations.

Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

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

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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) Source # 
Instance details

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

Defined in Agda.Syntax.Internal

Methods

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

show :: Type' a -> String #

showList :: [Type' a] -> ShowS #

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

Defined in Agda.Syntax.Internal

SgTel (Dom (ArgName, Type)) Source # 
Instance details

Defined in Agda.Syntax.Internal

SgTel (Dom Type) Source # 
Instance details

Defined in Agda.Syntax.Internal

LensSort (Type' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Type' a -> S Int32 Source #

icod_ :: Type' a -> S Int32 Source #

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

PrettyTCM (Type' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

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

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Type' a -> Set QName Source #

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

Defined in Agda.TypeChecking.Monad.SizedTypes

AddContext (Dom (String, Type)) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (Dom (Name, Type)) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Dom Type -> Nat Source #

AddContext (KeepNames Telescope) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

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

Defined in Agda.TypeChecking.Reduce

UsableRelevance a => UsableModality (Type' a) Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

Methods

usableMod :: Modality -> Type' a -> TCM Bool Source #

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

Defined in Agda.TypeChecking.Irrelevance

SgTel (ArgName, Dom Type) Source # 
Instance details

Defined in Agda.Syntax.Internal

AddContext ([NamedArg Name], Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: ([NamedArg Name], Type) -> Nat Source #

AddContext ([Arg Name], Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: ([Arg Name], Type) -> Nat Source #

AddContext ([WithHiding Name], Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext ([Name], Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (String, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (Name, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

AddContext (KeepNames String, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

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

UniverseBi ([Type], [Clause]) Pattern Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

UniverseBi ([Type], [Clause]) Term Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

PatternFrom (Type, Term) Elims [Elim' NLPat] Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Match (Type, Term) [Elim' NLPat] Elims Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> (Type, Term) -> [Elim' NLPat] -> Elims -> NLM () Source #

data Abs a Source #

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

NoAbs 

Fields

Instances
Functor Abs Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

Foldable Abs Source # 
Instance details

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 Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

Suggest String (Abs b) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

suggest :: String -> Abs b -> String Source #

Suggest Name (Abs b) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

suggest :: Name -> Abs b -> String Source #

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

Defined in Agda.TypeChecking.Substitute

Methods

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

Conversion MOT a b => Conversion MOT (Abs a) (Abs b) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

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

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

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

Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

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

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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) Source # 
Instance details

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

Defined in Agda.Syntax.Internal

Methods

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

show :: Abs a -> String #

showList :: [Abs a] -> ShowS #

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

Defined in Agda.Syntax.Internal

Methods

size :: Abs a -> Int Source #

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.TypeChecking.Free.Precompute

Methods

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

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

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

Defined in Agda.Syntax.Internal.Defs

Methods

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

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

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: Abs a -> FreeT

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Abs a -> S Int32 Source #

icod_ :: Abs a -> S Int32 Source #

value :: Int32 -> R (Abs a) Source #

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

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Abs a -> Set QName Source #

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

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: Abs a -> TCM () Source #

IsInstantiatedMeta a => IsInstantiatedMeta (Abs a) Source #

Does not worry about raising.

Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

MentionsMeta t => MentionsMeta (Abs t) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMeta :: MetaId -> Abs t -> Bool Source #

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Instantiate t => Instantiate (Abs t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

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

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)

(Reduce a, ForceNotFree a) => ForceNotFree (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => Abs a -> m (Abs a)

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

Defined in Agda.TypeChecking.Irrelevance

Methods

usableMod :: Modality -> Abs a -> TCM Bool Source #

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

Defined in Agda.TypeChecking.Irrelevance

Methods

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

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

Defined in Agda.TypeChecking.Positivity

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

Defined in Agda.TypeChecking.Polarity

Methods

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

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

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

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

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

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

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

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Abs a -> Abs a Source #

Suggest (Abs a) (Abs b) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

(Free i, Reify i a) => Reify (Abs i) (Name, a) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

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

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

type ArgName = String Source #

Names in binders and arguments.

type Elims Source #

Arguments

 = [Elim]

eliminations ordered left-to-right.

data Elim' a Source #

Eliminations, subsuming applications and projections.

Constructors

Apply (Arg a)

Application.

Proj ProjOrigin QName

Projection. QName is name of a record projection.

IApply a a a

IApply x y r, x and y are the endpoints

Instances
Functor Elim' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

Foldable Elim' Source # 
Instance details

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' Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Internal

PrettyTCM Elim Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Elim -> TCM Doc Source #

MentionsMeta Elim Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Normalise Elim Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify Elim Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Elim Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate Elim Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

IsPrefixOf Elims Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

UniverseBi Elims Pattern Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

universeBi :: Elims -> [Pattern] #

UniverseBi Elims Term Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

universeBi :: Elims -> [Term] #

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

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Defined in Agda.TypeChecking.Substitute

Methods

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

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

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

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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) Source # 
Instance details

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

Defined in Agda.Syntax.Internal

Methods

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

show :: Elim' a -> String #

showList :: [Elim' a] -> ShowS #

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

Defined in Agda.Syntax.Internal

Methods

rnf :: Elim' a -> () #

Pretty tm => Pretty (Elim' tm) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Elim' tm -> Doc Source #

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

prettyList :: [Elim' tm] -> Doc Source #

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

Defined in Agda.Syntax.Internal

LensOrigin (Elim' a) Source #

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

Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.TypeChecking.Free.Precompute

Methods

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

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

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

Defined in Agda.Syntax.Internal.Defs

Methods

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

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

Defined in Agda.TypeChecking.Free.Old

Methods

freeVars' :: Elim' a -> FreeT

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Elim' a -> S Int32 Source #

icod_ :: Elim' a -> S Int32 Source #

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

PrettyTCM (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Elim' DisplayTerm) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

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

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Elim' a -> Set QName Source #

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

Defined in Agda.TypeChecking.Reduce

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

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)

(Reduce a, ForceNotFree a) => ForceNotFree (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => Elim' a -> m (Elim' a)

(SubstWithOrigin a, SubstWithOrigin (Arg a)) => SubstWithOrigin (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.DisplayForm

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

Defined in Agda.TypeChecking.DisplayForm

Methods

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

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

Defined in Agda.TypeChecking.Irrelevance

Methods

usableMod :: Modality -> Elim' a -> TCM Bool Source #

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

Defined in Agda.TypeChecking.Irrelevance

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

Defined in Agda.TypeChecking.Forcing

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

Defined in Agda.TypeChecking.Positivity

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

Defined in Agda.TypeChecking.Polarity

Methods

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

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

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

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

Defined in Agda.TypeChecking.MetaVars.Occurs

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

Defined in Agda.TypeChecking.Abstract

Methods

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

PatternVarModalities a x => PatternVarModalities (Elim' a) x Source # 
Instance details

Defined in Agda.Syntax.Internal.Pattern

Reify i a => Reify (Elim' i) (Elim' a) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

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

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

PatternFrom (Type, Term) Elims [Elim' NLPat] Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Match (Type, Term) [Elim' NLPat] Elims Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> (Type, Term) -> [Elim' NLPat] -> Elims -> NLM () Source #

data Term Source #

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.

Dummy String

A (part of a) term or type which is only used for internal purposes. Replaces the Sort Prop hack. The String typically describes the location where we create this dummy, but can contain other information as well.

Instances
Eq Term Source #

Syntactic Term equality, ignores stuff below DontCare and sharing.

Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Data Term Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> 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 Source # 
Instance details

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 #