Agda-2.6.1: 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' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.TypeChecking.Monad.Base

data Suggestion Source #

Constructors

Suggest a => Suggestion a 

class Suggest a where Source #

Suggest a name if available (i.e. name is not "_")

Instances
Suggest String Source # 
Instance details

Defined in Agda.Syntax.Internal

Suggest Name Source # 
Instance details

Defined in Agda.Syntax.Internal

Suggest Term Source # 
Instance details

Defined in Agda.Syntax.Internal

Suggest (Abs b) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Methods

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

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 IMPOSSIBLE. Apply this to closed terms you want to use in a non-empty context. Γ ⊢ EmptyS : ()

a :# (Substitution' a) infixr 4

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

Strengthen Empty (Substitution' a)

Strengthening substitution. First argument is IMPOSSIBLE. Apply this to a term which does not contain variable 0 to lower all de Bruijn indices by one. Γ ⊢ ρ : Δ --------------------------- Γ ⊢ Strengthen ρ : Δ, A

Wk !Int (Substitution' a)

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

Lift !Int (Substitution' a)

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

Instances
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 (True) or data type (False). In the former case, the PatOrigin of the conPInfo 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

  • conPInfo :: PatternInfo

    Information on the origin of the pattern.

  • conPRecord :: Bool

    False if data constructor. True 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 in the unifier (unifyStep) 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 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

Reduce DeBruijnPattern 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

ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

ToNLPat (Arg DeBruijnPattern) (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

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 PatternInfo x
x
DotP PatternInfo Term
.t
ConP ConHead ConPatternInfo [NamedArg (Pattern' x)]

c ps The subpatterns do not contain any projection copatterns.

LitP PatternInfo Literal

E.g. 5, "hello".

ProjP ProjOrigin QName

Projection copattern. Can only appear by itself.

IApplyP PatternInfo Term Term x

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

DefP PatternInfo 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) #

Reduce DeBruijnPattern 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

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

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

Defined in Agda.TypeChecking.Substitute

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 :: MonadPretty m => Pattern' a -> m 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

ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

ToNLPat (Arg DeBruijnPattern) (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

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

data PatternInfo Source #

Constructors

PatternInfo 
Instances
Eq PatternInfo Source # 
Instance details

Defined in Agda.Syntax.Internal

Data PatternInfo 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) -> PatternInfo -> c PatternInfo #

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

toConstr :: PatternInfo -> Constr #

dataTypeOf :: PatternInfo -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> PatternInfo -> PatternInfo #

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

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

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

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

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

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

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

Show PatternInfo Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange PatternInfo Source # 
Instance details

Defined in Agda.Syntax.Internal

EmbPrj PatternInfo 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

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

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

  • namedClausePats :: NAPs

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

  • clauseBody :: Maybe Term

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

  • clauseType :: Maybe (Arg Type)

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

  • clauseCatchall :: Bool

    Clause has been labelled as CATCHALL.

  • clauseRecursive :: Maybe Bool

    clauseBody contains recursive calls; computed by termination checker. Nothing means that termination checker has not run yet, or that clauseBody contains meta-variables; these could be filled with recursive calls later! Just False means definitely no recursive call. Just True means definitely a recursive call.

  • clauseUnreachable :: Maybe Bool

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

  • clauseEllipsis :: ExpandedEllipsis

    Was this clause created by expansion of an ellipsis?

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 a c => Clause -> FreeM a 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 #

EmbPrj Clause Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM Clause Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Clause -> m Doc Source #

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

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

EmbPrj Blocked_ Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.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 #

Data t => Data (Blocked t) 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) -> Blocked t -> c (Blocked t) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Blocked t) #

toConstr :: Blocked t -> Constr #

dataTypeOf :: Blocked t -> DataType #

dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (Blocked t)) #

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

gmapT :: (forall b. Data b => b -> b) -> Blocked t -> Blocked t #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Blocked t -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Blocked t -> r #

gmapQ :: (forall d. Data d => d -> u) -> Blocked t -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Blocked t -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Blocked t -> m (Blocked t) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Blocked t -> m (Blocked t) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Blocked t -> m (Blocked t) #

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 :: MonadPretty m => Blocked a -> m 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

EmbPrj NotBlocked Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

newtype BraveTerm Source #

Newtypes for terms that produce a dummy, rather than crash, when applied to incompatible eliminations.

Constructors

BraveTerm 

Fields

Instances
Data BraveTerm 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) -> BraveTerm -> c BraveTerm #

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

toConstr :: BraveTerm -> Constr #

dataTypeOf :: BraveTerm -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> BraveTerm -> BraveTerm #

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

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

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

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

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

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

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

Show BraveTerm Source # 
Instance details

Defined in Agda.Syntax.Internal

DeBruijn BraveTerm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply BraveTerm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst BraveTerm BraveTerm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

data LevelAtom' t Source #

An atomic term of type Level.

Constructors

MetaLevel MetaId [Elim' t]

A meta variable targeting Level under some eliminations.

BlockedLevel MetaId t

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

NeutralLevel NotBlocked t

A neutral term of type Level.

UnreducedLevel t

Introduced by instantiate, removed by reduce.

Instances
Eq LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Ord LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

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

Methods

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

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 #

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

AnyRigid LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat -> tcm Bool) -> LevelAtom -> tcm Bool Source #

Occurs LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

EqualSy LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

AbsTerm LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

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

Defined in Agda.TypeChecking.Substitute

Data t => Data (LevelAtom' t) 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' t -> c (LevelAtom' t) #

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

toConstr :: LevelAtom' t -> Constr #

dataTypeOf :: LevelAtom' t -> DataType #

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

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

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

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

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

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

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

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

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

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

Show t => Show (LevelAtom' t) Source # 
Instance details

Defined in Agda.Syntax.Internal

data PlusLevel' t Source #

Constructors

Plus Integer (LevelAtom' t)

n + ℓ.

Instances
Ord PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

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

Methods

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

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 #

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

AnyRigid PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat -> tcm Bool) -> PlusLevel -> tcm Bool Source #

Occurs PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

EqualSy PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

AbsTerm PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

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

Defined in Agda.TypeChecking.Substitute

Eq (PlusLevel' Term) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Data t => Data (PlusLevel' t) 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' t -> c (PlusLevel' t) #

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

toConstr :: PlusLevel' t -> Constr #

dataTypeOf :: PlusLevel' t -> DataType #

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

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

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

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

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

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

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

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

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

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

Show t => Show (PlusLevel' t) Source # 
Instance details

Defined in Agda.Syntax.Internal

data Level' t Source #

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

Constructors

Max Integer [PlusLevel' t] 
Instances
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 a c => Level -> FreeM a 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 #

EmbPrj Level Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM Level Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Level -> m 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 :: MonadMetaSolver m => Level -> m () 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

IsMeta Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: HasBuiltins m => Level -> m (Maybe MetaId) Source #

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 #

AnyRigid Level Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat -> tcm Bool) -> Level -> tcm Bool Source #

Occurs Level Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

EqualSy Level Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Level -> Level -> Bool Source #

AbsTerm Level Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

Reify Level Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Level -> m Expr Source #

reifyWhen :: MonadReify m => Bool -> Level -> m Expr Source #

NLPatToTerm NLPat Level Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

PatternFrom () Level NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

Match () NLPat Level Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

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

Defined in Agda.TypeChecking.Substitute

Eq (Level' Term) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Data t => Data (Level' t) 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' t -> c (Level' t) #

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

toConstr :: Level' t -> Constr #

dataTypeOf :: Level' t -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord (Level' Term) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Show t => Show (Level' t) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Level' t -> ShowS #

show :: Level' t -> String #

showList :: [Level' t] -> ShowS #

data Sort' t Source #

Sorts.

Constructors

Type (Level' t)

Set ℓ.

Prop (Level' t)

Prop ℓ.

Inf

Setω.

SizeUniv

SizeUniv, a sort inhabited by type Size.

PiSort (Dom' t (Type'' t t)) (Abs (Sort' t))

Sort of the pi type.

FunSort (Sort' t) (Sort' t)

Sort of a (non-dependent) function type.

UnivSort (Sort' t)

Sort of another sort.

MetaS !MetaId [Elim' t] 
DefS QName [Elim' t]

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
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 a c => Sort -> FreeM a 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 #

EmbPrj Sort Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM Sort Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Sort -> m 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 :: MonadMetaSolver m => Sort -> m () 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

IsMeta Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: HasBuiltins m => Sort -> m (Maybe MetaId) Source #

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

AnyRigid Sort Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat -> tcm Bool) -> Sort -> tcm Bool Source #

Occurs Sort Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

EqualSy Sort Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Sort -> Sort -> Bool Source #

AbsTerm Sort Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

Reify Sort Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Sort -> m Expr Source #

reifyWhen :: MonadReify m => Bool -> Sort -> m Expr Source #

NLPatToTerm NLPSort Sort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

PatternFrom () Sort NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

Match () NLPSort Sort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

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

Defined in Agda.TypeChecking.Substitute

Methods

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

Eq (Sort' Term) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Data t => Data (Sort' t) 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' t -> c (Sort' t) #

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

toConstr :: Sort' t -> Constr #

dataTypeOf :: Sort' t -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord (Sort' Term) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Show t => Show (Sort' t) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Sort' t -> ShowS #

show :: Sort' t -> String #

showList :: [Sort' t] -> ShowS #

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

AddContext Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

DropArgs Telescope Source #

NOTE: This creates telescopes with unbound de Bruijn indices.

Instance details

Defined in Agda.TypeChecking.DropArgs

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

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 #

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 #

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => Tele t -> FreeM a 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 #

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

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

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

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Tele t -> ReduceM (Tele t) 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 (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Internal

LensSort (Type' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal

type Type' a = Type'' Term a Source #

data Type'' t a Source #

Types are terms with a sort annotation.

Constructors

El 

Fields

Instances
NFData Type Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Type -> () #

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 #

PrettyTCM Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Type Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Type -> m 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

AddContext Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

DropArgs Telescope Source #

NOTE: This creates telescopes with unbound de Bruijn indices.

Instance details

Defined in Agda.TypeChecking.DropArgs

UnFreezeMeta Type Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => Type -> m () Source #

MentionsMeta Type Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Reduce Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Type Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

IsMeta Type Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: HasBuiltins m => Type -> m (Maybe MetaId) Source #

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)

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 #

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 #

AnyRigid Type Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat -> tcm Bool) -> Type -> tcm Bool Source #

Occurs Type Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

EqualSy Type Source #

Ignores sorts.

Instance details

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Type -> Type -> Bool 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

Methods

reify :: MonadReify m => Type -> m Expr Source #

reifyWhen :: MonadReify m => Bool -> Type -> m Expr Source #

NLPatToTerm NLPType Type Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

PatternFrom () Type NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

PatternFrom Type Term NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

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 #

Conversion TOM Type (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

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

Conversion MOT (Exp O) Type Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Type Source #

(Coercible a Term, Subst t a, Subst t b) => Subst t (Type'' a b) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' t -> Type'' a b -> Type'' a b 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 #

Functor (Type'' t) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

(<$) :: a -> Type'' t b -> Type'' t 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 #

Foldable (Type'' t) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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

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

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

toList :: Type'' t a -> [a] #

null :: Type'' t a -> Bool #

length :: Type'' t a -> Int #

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

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

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

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

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

Traversable (Type'' t) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

Decoration (Type'' t) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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 t => Free (Type' t) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => Type' t -> FreeM a 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 #

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

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => Dom (String, Type) -> m a -> m a Source #

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

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

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => Dom (Name, Type) -> m a -> m a Source #

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

AddContext (Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => Dom Type -> m a -> m a Source #

contextSize :: Dom Type -> Nat Source #

AddContext (KeepNames Telescope) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

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

Defined in Agda.TypeChecking.Monad.SizedTypes

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

Defined in Agda.TypeChecking.Reduce

Normalise t => Normalise (Type' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Type' t -> ReduceM (Type' t) Source #

Simplify t => Simplify (Type' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Type' t -> ReduceM (Type' t) Source #

Instantiate t => Instantiate (Type' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

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

(Data t, Data a) => Data (Type'' t 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'' t a -> c (Type'' t a) #

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

toConstr :: Type'' t a -> Constr #

dataTypeOf :: Type'' t a -> DataType #

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

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

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

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

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

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

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

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

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

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

(Show t, Show a) => Show (Type'' t a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

show :: Type'' t a -> String #

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

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 :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source #

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

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

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([Arg Name], Type) -> m a -> m a Source #

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

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

Defined in Agda.TypeChecking.Monad.Context

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

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([Name], Dom Type) -> m a -> m a Source #

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

AddContext (String, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => (String, Dom Type) -> m a -> m a Source #

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

AddContext (Name, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => (Name, Dom Type) -> m a -> m a Source #

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

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

Defined in Agda.TypeChecking.Monad.Context

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

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 #

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

Suggest (Abs b) 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 t => Free (Abs t) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => Abs t -> FreeM a 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 #

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 :: MonadMetaSolver m => Abs a -> m () 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

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

getMatchables :: Abs a -> [QName] Source #

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

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, AnyRigid a) => AnyRigid (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat -> tcm Bool) -> Abs a -> tcm Bool Source #

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

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: Abs a -> OccursM (Abs a) Source #

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

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

Ignores absName.

Instance details

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Abs a -> Abs a -> Bool 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 #

ToNLPat a b => ToNLPat (Abs a) (Abs b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Abs a -> Abs b Source #

NLPatToTerm p a => NLPatToTerm (Abs p) (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Abs i -> m (Name, a) Source #

reifyWhen :: MonadReify m => Bool -> Abs i -> m (Name, a) Source #

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

PrettyTCM Elim Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Elim -> m Doc Source #

MentionsMeta Elim Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Reduce Elim Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

IsPrefixOf Elims Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

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