Agda-2.6.1.3: 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

Instances details
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

Instances details
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

forall a.Suggest a => Suggestion a 

class Suggest a where Source #

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

Instances

Instances details
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

Instances details
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

Instances details
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 IntervalView Source #

Constructors

IZero 
IOne 
IMin (Arg Term) (Arg Term) 
IMax (Arg Term) (Arg Term) 
INeg (Arg Term) 
OTerm Term 

Instances

Instances details
Show IntervalView Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Instances details
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

Instances details
Eq Substitution Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Functor Substitution' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

Ord Substitution Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Foldable Substitution' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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

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

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

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

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

null :: Substitution' a -> Bool #

length :: Substitution' a -> Int #

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

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

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

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

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

Traversable Substitution' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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 :: forall r r'. (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) #

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

Instances details
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

Instances details
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 :: forall r r'. (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

Instances details
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 :: forall r r'. (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

Instances details
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 #

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 :: forall r r'. (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

Instances details
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 :: forall r r'. (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

Instances details
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 :: forall r r'. (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

Instances details
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 :: forall r r'. (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

Instances details
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 #

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 :: forall r r'. (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

Instances details
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 :: forall r r'. (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

Instances details
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 :: forall r r'. (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

Instances details
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

Methods

mentionsMetas :: HashSet MetaId -> LevelAtom -> Bool Source #

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 :: forall r r'. (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

Instances details
Eq PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

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

Methods

mentionsMetas :: HashSet MetaId -> PlusLevel -> Bool Source #

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

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 :: forall r r'. (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

Instances details
Eq Level Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Ord Level Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

compare :: Level -> Level -> Ordering #

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

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

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

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

max :: Level -> Level -> Level #

min :: Level -> Level -> Level #

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

Methods

mentionsMetas :: HashSet MetaId -> Level -> Bool Source #

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

Methods

match :: forall (m :: Type -> Type). MonadDisplayForm m => Level -> Level -> MaybeT m [WithOrigin Term] Source #

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

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 :: forall r r'. (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) #

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

Instances details
Eq Sort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Ord Sort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

compare :: Sort -> Sort -> Ordering #

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

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

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

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

max :: Sort -> Sort -> Sort #

min :: Sort -> Sort -> Sort #

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

Methods

mentionsMetas :: HashSet MetaId -> Sort -> Bool Source #

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

Methods

match :: forall (m :: Type -> Type). MonadDisplayForm m => Sort -> Sort -> MaybeT m [WithOrigin Term] Source #

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 #

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 :: forall r r'. (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) #

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

Instances details
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 #

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 :: forall r r'. (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

Methods

mentionsMetas :: HashSet MetaId -> Tele a -> Bool Source #

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

Defined in Agda.TypeChecking.Reduce

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Instances details
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

Instances details
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

Methods

mentionsMetas :: HashSet MetaId -> Type -> Bool Source #

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 #

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 :: forall r r'. (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

Instances details
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 #

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 :: forall r r'. (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

Methods

mentionsMetas :: HashSet MetaId -> Abs t -> Bool Source #

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

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

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Irrelevance

Methods

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

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

Defined in Agda.TypeChecking.Irrelevance

Methods

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

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

Instances details
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 #

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

Methods

mentionsMetas :: HashSet MetaId -> Elim -> Bool Source #

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 :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Elim' a -> r #

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

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

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

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

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

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

Defined in Agda.TypeChecking.Substitute

Methods

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

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

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

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

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

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

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

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

Defined in Agda.Syntax.Internal

Methods

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

show :: Elim' a -> String #

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

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

Defined in Agda.Syntax.Internal

Methods

rnf :: Elim' a -> () #

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

Defined in Agda.Syntax.Internal

Methods

pretty :: Elim' tm -> Doc Source #

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

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

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

Defined in Agda.Syntax.Internal

LensOrigin (Elim' a) Source #

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

Instance details

Defined in Agda.Syntax.Internal

IsProjElim (Elim' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.TypeChecking.Free.Precompute

Methods

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

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

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

Defined in Agda.Syntax.Internal.Defs

Methods

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

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

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

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

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

PrettyTCM (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Elim' DisplayTerm) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

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

Defined in Agda.Syntax.Internal.Names

Methods

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

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

Defined in Agda.TypeChecking.Reduce

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

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

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

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

Defined in Agda.TypeChecking.DisplayForm

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

Defined in Agda.TypeChecking.DisplayForm

Methods

match :: forall (m :: Type -> Type). MonadDisplayForm m => Elim' a -> Elim' a -> MaybeT m [WithOrigin Term] Source #

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

Defined in Agda.TypeChecking.Irrelevance

Methods

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

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

Defined in Agda.TypeChecking.Irrelevance

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

getMatchables :: Elim' a -> [QName] Source #

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

Defined in Agda.TypeChecking.Positivity

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

Defined in Agda.TypeChecking.Polarity

Methods

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

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

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

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

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: Elim' a -> OccursM (Elim' a) Source #

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

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

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Elim' a -> Elim' a -> Bool Source #

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

Defined in Agda.TypeChecking.Abstract

Methods

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

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

ToNLPat a b => ToNLPat (Elim' a) (Elim' b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Elim' a -> Elim' b Source #

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Elim' i -> m (Elim' a) Source #

reifyWhen :: MonadReify m => Bool -> Elim' i -> m (Elim' a) Source #

NLPatToTerm p a => NLPatToTerm (Elim' p) (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

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

Raw values.

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

Constructors

Var !Int Elims

x es neutral

Lam ArgInfo (Abs Term)

Terms are beta normal. Relevance is ignored

Lit Literal 
Def QName Elims

f es, possibly a delta/iota-redex

Con ConHead ConInfo Elims

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

Pi (Dom Type) (Abs Type)

dependent or non-dependent function space

Sort Sort 
Level Level 
MetaV !MetaId Elims 
DontCare Term

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

Dummy String Elims

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

Instances

Instances details
Eq Substitution Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Eq LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Eq PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Eq Level Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Eq Sort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Eq Term Source #

Syntactic Term equality, ignores stuff below DontCare and sharing.

Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Data Term Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

toConstr :: Term -> Constr #

dataTypeOf :: Term -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord Substitution Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Ord LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Ord PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Ord Level Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

compare :: Level -> Level -> Ordering #

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

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

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

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

max :: Level -> Level -> Level #

min :: Level -> Level -> Level #

Ord Sort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

compare :: Sort -> Sort -> Ordering #

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

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

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

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

max :: Sort -> Sort -> Sort #

min :: Sort -> Sort -> Sort #

Ord Term Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

compare :: Term -> Term -> Ordering #

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

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

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

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

max :: Term -> Term -> Term #

min :: Term -> Term -> Term #

Show Term Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Term -> ShowS #

show :: Term -> String #

showList :: [Term] -> ShowS #

NFData LevelAtom Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: LevelAtom -> () #

NFData PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: PlusLevel -> () #

NFData Level Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Level -> () #

NFData Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Sort -> () #

NFData Type Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Type -> () #

NFData Term Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Term -> () #

Pretty LevelAtom Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty Level Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty Type Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty Term Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

KillRange Substitution Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange LevelAtom Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange Level Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange Term Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

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

Suggest Term 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

DeBruijn LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.DeBruijn

DeBruijn PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.DeBruijn

DeBruijn Level Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.DeBruijn

DeBruijn Term Source #

We can substitute Terms for variables.

Instance details

Defined in Agda.TypeChecking.Substitute.DeBruijn

PrecomputeFreeVars LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

PrecomputeFreeVars PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

PrecomputeFreeVars Level Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

PrecomputeFreeVars Sort Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

PrecomputeFreeVars Type Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

PrecomputeFreeVars Term 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 #

Free PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free Level Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free Sort Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Free Term Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

Abstract Sort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Type Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Term Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract CompiledClauses 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 #

Apply Term Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Term -> Args -> Term Source #

applyE :: Term -> Elims -> Term Source #

Apply CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

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 #

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 #

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 #

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 #

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 #

TermLike Term Source # 
Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

GetDefs LevelAtom Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs Level Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs Sort Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs Type Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

GetDefs Term Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

EmbPrj LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Level Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Sort Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj Term Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

EmbPrj CompiledClauses 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 #

PrettyTCM Sort Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Sort -> m Doc 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 #

PrettyTCM Elim Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Term Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

NamesIn LevelAtom Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

NamesIn PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

NamesIn Level Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Level -> Set QName Source #

NamesIn Sort Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Sort -> Set QName Source #

NamesIn Term Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Term -> Set QName Source #

NamesIn CompiledClauses Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

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

PiApplyM Term Source # 
Instance details

Defined in Agda.TypeChecking.Telescope

Methods

piApplyM :: MonadReduce m => Type -> Term -> m Type Source #

IsSizeType Term Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

DropArgs Telescope Source #

NOTE: This creates telescopes with unbound de Bruijn indices.

Instance details

Defined in Agda.TypeChecking.DropArgs

DropArgs Term Source #

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

Instance details

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Term -> Term Source #

DropArgs CompiledClauses Source #

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

Instance details

Defined in Agda.TypeChecking.DropArgs

UnFreezeMeta LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

UnFreezeMeta PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

UnFreezeMeta Level Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

UnFreezeMeta Sort Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

UnFreezeMeta Type Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

UnFreezeMeta Term Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

IsInstantiatedMeta LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

IsInstantiatedMeta PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

IsInstantiatedMeta Level Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

IsInstantiatedMeta Term Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

MentionsMeta LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> LevelAtom -> Bool Source #

MentionsMeta PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> PlusLevel -> Bool Source #

MentionsMeta Level Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Level -> Bool Source #

MentionsMeta Sort Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Sort -> Bool Source #

MentionsMeta Type Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Type -> Bool Source #

MentionsMeta Elim Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Elim -> Bool Source #

MentionsMeta Term Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Term -> Bool Source #

InstantiateFull Substitution Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Term Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise Term Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify Term Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Type Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Elim Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

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

IsMeta Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

IsMeta Type Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

IsMeta Term Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

Instantiate LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate Term Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

SynEq LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

SynEq PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

SynEq Level Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

SynEq Sort Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

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)

SynEq Term Source #

Syntactic term equality ignores DontCare stuff.

Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

ToTerm Type Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

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

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

ForceNotFree PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

ForceNotFree Level Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

ForceNotFree Sort Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

ForceNotFree Type Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

ForceNotFree Term Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

SubstWithOrigin Term Source # 
Instance details

Defined in Agda.TypeChecking.DisplayForm

Match Level Source # 
Instance details

Defined in Agda.TypeChecking.DisplayForm

Methods

match :: forall (m :: Type -> Type). MonadDisplayForm m => Level -> Level -> MaybeT m [WithOrigin Term] Source #

Match Sort Source # 
Instance details

Defined in Agda.TypeChecking.DisplayForm

Methods

match :: forall (m :: Type -> Type). MonadDisplayForm m => Sort -> Sort -> MaybeT m [WithOrigin Term] Source #

Match Term Source # 
Instance details

Defined in Agda.TypeChecking.DisplayForm

Methods

match :: forall (m :: Type -> Type). MonadDisplayForm m => Term -> Term -> MaybeT m [WithOrigin Term] Source #

UsableModality Level Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

UsableModality Sort Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

UsableModality Term Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

UsableRelevance LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

UsableRelevance PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

UsableRelevance Level Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

UsableRelevance Sort Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

UsableRelevance Term Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

GetMatchables Term Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

ComputeOccurrences LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

ComputeOccurrences PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

ComputeOccurrences Level Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

ComputeOccurrences Type Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

ComputeOccurrences Term Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

HasPolarity LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Polarity

HasPolarity PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Polarity

HasPolarity Level Source # 
Instance details

Defined in Agda.TypeChecking.Polarity

Methods

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

HasPolarity Type Source # 
Instance details

Defined in Agda.TypeChecking.Polarity

Methods

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

HasPolarity Term Source # 
Instance details

Defined in Agda.TypeChecking.Polarity

Methods

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

AnyRigid LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

AnyRigid PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat -> tcm Bool) -> PlusLevel -> tcm Bool 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 #

AnyRigid Sort Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat -> tcm Bool) -> Sort -> tcm Bool 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 #

AnyRigid Term Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

Occurs LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Occurs PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Occurs Level Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Occurs Sort Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Occurs Type Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Occurs Term Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

ReduceAndEtaContract Term Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars

NoProjectedVar Term Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars

EqualSy LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

EqualSy PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

EqualSy Level Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

EqualSy Sort Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

EqualSy Type Source #

Ignores sorts.

Instance details

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Type -> Type -> Bool Source #

EqualSy Term Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Term -> Term -> Bool Source #

AbsTerm LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

AbsTerm PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

AbsTerm Level Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

AbsTerm Sort Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

AbsTerm Type Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

AbsTerm Term Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

IsPrefixOf Elims Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

IsPrefixOf Term Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

IsPrefixOf Args Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Subst Term () Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

Subst Term String Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term Range Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term QName Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.Class

Subst Term Name Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term ConPatternInfo Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term Pattern Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term Term Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term ProblemEq Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term SingleLevel Source # 
Instance details

Defined in Agda.TypeChecking.Level

Subst Term AbsurdPattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Subst Term DotPattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Subst Term AsBinding Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Subst Term SizeConstraint Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Subst Term SizeMeta Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Subst Term CType Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Data

Subst Term LType Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Data

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 #

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 #

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 #

Reify Term Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

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

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

NLPatToTerm Nat Term Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

NLPatToTerm NLPSort Sort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

NLPatToTerm NLPType Type Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

NLPatToTerm NLPat Level Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

NLPatToTerm NLPat Term 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 #

PatternFrom () Sort NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

Match () NLPType Type Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

Match () NLPat Level Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> () -> NLPat -> Level -> 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 TOM Term (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

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

Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

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

Subst Term (Problem a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

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

Defined in Agda.TypeChecking.Patterns.Internal

Conversion MOT (Exp O) Type Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Type Source #

Conversion MOT (Exp O) Term Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Term Source #

PatternFrom t a b => PatternFrom t (Dom a) (Dom b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> t -> Dom a -> TCM (Dom b) Source #

Match t a b => Match t (Dom a) (Dom b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> t -> Dom a -> Dom b -> NLM () Source #

Subst Term (SizeExpr' NamedRigid SizeMeta) Source #

Only for raise.

Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

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 #

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 #

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

Defined in Agda.TypeChecking.Substitute

Methods

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

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

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

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

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

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

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

NFData e => NFData (Dom e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Dom e -> () #

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

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.TypeChecking.Free.Precompute

Methods

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

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 #

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

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

Defined in Agda.Syntax.Internal.Defs

Methods

getDefs :: MonadGetDefs m => Dom a -> m () 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 #

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Dom a -> S Int32 Source #

icod_ :: Dom a -> S Int32 Source #

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

PrettyTCM (Type' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Dom a -> m Doc Source #

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

Defined in Agda.Syntax.Internal.Names

Methods

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

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

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Dom 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

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

Defined in Agda.TypeChecking.Monad.SizedTypes

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

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Dom t -> Bool Source #

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 #

Normalise t => Normalise (Dom t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

Simplify t => Simplify (Dom t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

Reduce t => Reduce (Dom t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Dom t -> ReduceM (Dom t) Source #

reduceB' :: Dom t -> ReduceM (Blocked (Dom t)) Source #

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

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

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

SubstWithOrigin (Arg Term) Source # 
Instance details

Defined in Agda.TypeChecking.DisplayForm

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

Defined in Agda.TypeChecking.Irrelevance

Methods

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

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

Defined in Agda.TypeChecking.Irrelevance

Methods

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

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

Defined in Agda.TypeChecking.Irrelevance

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

Defined in Agda.TypeChecking.Irrelevance

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

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

Defined in Agda.TypeChecking.Positivity

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

Defined in Agda.TypeChecking.Polarity

Methods

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

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

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

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

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

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

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

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Dom a) Source #

EqualSy a => EqualSy (Dom a) Source #

Ignore the tactic.

Instance details

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Dom a -> Dom a -> Bool Source #

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

Defined in Agda.TypeChecking.Abstract

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Dom a -> Dom b Source #

Reify i a => Reify (Dom i) (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Dom i -> m (Arg a) Source #

reifyWhen :: MonadReify m => Bool -> Dom i -> m (Arg a) Source #

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

PatternFrom t a b => PatternFrom (Dom t) (Arg a) (Arg b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> Dom t -> Arg a -> TCM (Arg b) Source #

Match t a b => Match (Dom t) (Arg a) (Arg b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> Dom t -> Arg a -> Arg b -> NLM () Source #

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

ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

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 #

class LensConName a where Source #

Minimal complete definition

getConName

Methods

getConName :: a -> QName Source #

setConName :: QName -> a -> a Source #

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

Instances

Instances details
LensConName ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

data ConHead Source #

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

Constructors

ConHead 

Fields

  • conName :: QName

    The name of the constructor.

  • conInductive :: Induction

    Record constructors can be coinductive.

  • conFields :: [Arg QName]

    The name of the record fields. Empty list for data constructors. Arg is stored since the info in the constructor args might not be accurate because of subtyping (issue #2170).

Instances

Instances details
Eq ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

toConstr :: ConHead -> Constr #

dataTypeOf :: ConHead -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

Show ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

Pretty ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

KillRange ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

SetRange ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

HasRange ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

LensConName ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

EmbPrj ConHead Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM ConHead Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

NamesIn ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

InstantiateFull ConHead Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

type Args = [Arg Term] Source #

Type of argument lists.

data Dom' t e Source #

Similar to Arg, but we need to distinguish an irrelevance annotation in a function domain (the domain itself is not irrelevant!) from an irrelevant argument.

Dom is used in Pi of internal syntax, in Context and Telescope. Arg is used for actual arguments (Var, Con, Def etc.) and in Abstract syntax and other situations.

cubical
When domFinite = True for the domain of a Pi type, the elements should be compared by tabulating the domain type. Only supported in case the domain type is primIsOne, to obtain the correct equality for partial elements.

Constructors

Dom 

Fields

Instances

Instances details
TelToArgs ListTel Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Reduce Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reify Telescope Telescope Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

PatternFrom t a b => PatternFrom t (Dom a) (Dom b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> t -> Dom a -> TCM (Dom b) Source #

Match t a b => Match t (Dom a) (Dom b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> t -> Dom a -> Dom b -> NLM () Source #

LensNamed NamedName (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

(Subst t a, Subst t b) => Subst t (Dom' a b) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' t -> Dom' a b -> Dom' a b Source #

Functor (Dom' t) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

(<$) :: a -> Dom' t b -> Dom' t a #

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

Defined in Agda.TypeChecking.Substitute

Methods

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

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

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

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

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

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

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

Foldable (Dom' t) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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

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

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

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

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

null :: Dom' t a -> Bool #

length :: Dom' t a -> Int #

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

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

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

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

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

Traversable (Dom' t) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

NFData e => NFData (Dom e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Dom e -> () #

Decoration (Dom' t) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

distributeF :: Functor m => Dom' t (m a) -> m (Dom' t a) 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 #

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

Defined in Agda.Syntax.Internal

SgTel (Dom Type) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.TypeChecking.Free.Precompute

Methods

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

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

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Defined in Agda.Syntax.Internal.Generic

Methods

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

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

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

Defined in Agda.Syntax.Internal.Defs

Methods

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

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Dom a -> S Int32 Source #

icod_ :: Dom a -> S Int32 Source #

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

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Dom a -> m Doc Source #

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

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Dom 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 (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

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

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Dom t -> Bool Source #

Normalise t => Normalise (Dom t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

Simplify t => Simplify (Dom t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

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

Reduce t => Reduce (Dom t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Dom t -> ReduceM (Dom t) Source #

reduceB' :: Dom t -> ReduceM (Blocked (Dom t)) Source #

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

Defined in Agda.TypeChecking.SyntacticEquality

Methods

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

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

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

Defined in Agda.TypeChecking.Free.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Irrelevance

Methods

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

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

Defined in Agda.TypeChecking.Irrelevance

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

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

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

Defined in Agda.TypeChecking.Positivity

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

Defined in Agda.TypeChecking.Polarity

Methods

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

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

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

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

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

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

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

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

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Dom a) Source #

EqualSy a => EqualSy (Dom a) Source #

Ignore the tactic.

Instance details

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Dom a -> Dom a -> Bool Source #

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

Defined in Agda.TypeChecking.Abstract

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Dom a -> Dom b Source #

Reify i a => Reify (Dom i) (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Dom i -> m (Arg a) Source #

reifyWhen :: MonadReify m => Bool -> Dom i -> m (Arg a) Source #

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

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

PatternFrom t a b => PatternFrom (Dom t) (Arg a) (Arg b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> Dom t -> Arg a -> TCM (Arg b) Source #

Match t a b => Match (Dom t) (Arg a) (Arg b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> Dom t -> Arg a -> Arg b -> NLM () Source #

Eq a => Eq (Dom' t a) Source #

Ignores Origin and FreeVariables and tactic.

Instance details

Defined in Agda.Syntax.Internal

Methods

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

(/=) :: Dom' t a -> Dom' t a -> Bool #

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

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

toConstr :: Dom' t e -> Constr #

dataTypeOf :: Dom' t e -> DataType #

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

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

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

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

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

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

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

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

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

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

(Show t, Show e) => Show (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Dom' t e -> ShowS #

show :: Dom' t e -> String #

showList :: [Dom' t e] -> ShowS #

(Pretty t, Pretty e) => Pretty (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Dom' t e -> Doc Source #

prettyPrec :: Int -> Dom' t e -> Doc Source #

prettyList :: [Dom' t e] -> Doc Source #

(KillRange t, KillRange a) => KillRange (Dom' t a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Dom' t a) Source #

HasRange a => HasRange (Dom' t a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

getRange :: Dom' t a -> Range Source #

LensArgInfo (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

getArgInfo :: Dom' t e -> ArgInfo Source #

setArgInfo :: ArgInfo -> Dom' t e -> Dom' t e Source #

mapArgInfo :: (ArgInfo -> ArgInfo) -> Dom' t e -> Dom' t e Source #

LensFreeVariables (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

LensOrigin (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

getOrigin :: Dom' t e -> Origin Source #

setOrigin :: Origin -> Dom' t e -> Dom' t e Source #

mapOrigin :: (Origin -> Origin) -> Dom' t e -> Dom' t e Source #

LensCohesion (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

getCohesion :: Dom' t e -> Cohesion Source #

setCohesion :: Cohesion -> Dom' t e -> Dom' t e Source #

mapCohesion :: (Cohesion -> Cohesion) -> Dom' t e -> Dom' t e Source #

LensRelevance (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

LensQuantity (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

getQuantity :: Dom' t e -> Quantity Source #

setQuantity :: Quantity -> Dom' t e -> Dom' t e Source #

mapQuantity :: (Quantity -> Quantity) -> Dom' t e -> Dom' t e Source #

LensModality (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

getModality :: Dom' t e -> Modality Source #

setModality :: Modality -> Dom' t e -> Dom' t e Source #

mapModality :: (Modality -> Modality) -> Dom' t e -> Dom' t e Source #

LensHiding (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

getHiding :: Dom' t e -> Hiding Source #

setHiding :: Hiding -> Dom' t e -> Dom' t e Source #

mapHiding :: (Hiding -> Hiding) -> Dom' t e -> Dom' t e Source #

SgTel (ArgName, Dom Type) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

(InstantiateFull t, InstantiateFull e) => InstantiateFull (Dom' t e) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Dom' t e -> ReduceM (Dom' t e) Source #

(Instantiate t, Instantiate e) => Instantiate (Dom' t e) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Dom' t e -> ReduceM (Dom' t e) Source #

ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

pattern ClosedLevel :: Integer -> Level Source #

Constant level n

argFromDom :: Dom' t a -> Arg a Source #

stuckOn :: Elim -> NotBlocked -> NotBlocked Source #

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

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

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

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

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

varP :: a -> Pattern' a Source #

absurdP :: Int -> DeBruijnPattern Source #

Make an absurd pattern with the given de Bruijn index.

patternInfo :: Pattern' x -> Maybe PatternInfo Source #

Retrieve the PatternInfo from a pattern

patternOrigin :: Pattern' x -> Maybe PatOrigin Source #

Retrieve the origin of a pattern

properlyMatching :: Pattern' a -> Bool Source #

Does the pattern perform a match that could fail?

properlyMatching' Source #

Arguments

:: Bool

Should absurd patterns count as proper match?

-> Bool

Should projection patterns count as proper match?

-> Pattern' a

The pattern.

-> Bool 

absurdBody :: Abs Term Source #

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

var :: Nat -> Term Source #

An unapplied variable.

dontCare :: Term -> Term Source #

Add DontCare is it is not already a DontCare.

dummyTerm' :: String -> Int -> Term Source #

Aux: A dummy term to constitute a dummy termlevelsort/type.

dummyLevel' :: String -> Int -> Level Source #

Aux: A dummy level to constitute a level/sort.

dummyTerm :: String -> Int -> Term Source #

A dummy term created at location. Note: use macro DUMMY_TERM !

dummyLevel :: String -> Int -> Level Source #

A dummy level created at location. Note: use macro DUMMY_LEVEL !

dummySort :: String -> Int -> Sort Source #

A dummy sort created at location. Note: use macro DUMMY_SORT !

dummyType :: String -> Int -> Type Source #

A dummy type created at location. Note: use macro DUMMY_TYPE !

dummyDom :: String -> Int -> Dom Type Source #

Context entries without a type have this dummy type. Note: use macro DUMMY_DOM !

topSort :: Type Source #

Top sort (Setomega).

levelPlus :: Integer -> Level -> Level Source #

Given a constant m and level l, compute m + l

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

A traversal for the names in a telescope.

telFromList :: ListTel -> Telescope Source #

Convert a list telescope to a telescope.

telToList :: Tele (Dom t) -> [Dom (ArgName, t)] Source #

Convert a telescope to its list form.

listTel :: Lens' ListTel Telescope Source #

Lens to edit a Telescope as a list.

stripDontCare :: Term -> Term Source #

Removing a topmost DontCare constructor.

arity :: Type -> Nat Source #

Doesn't do any reduction.

unSpine :: Term -> Term Source #

Convert top-level postfix projections into prefix projections.

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

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

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

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

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

Drop Apply constructor. (Safe)

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

Drop Apply constructors. (Safe)

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

Split at first non-Apply

argsFromElims :: Elims -> Args Source #

Discards Proj f entries.

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

Drop Proj constructors. (Safe)

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

newtype MetaId Source #

A meta variable identifier is just a natural number.

Constructors

MetaId 

Fields

Instances

Instances details
Enum MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Eq MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

Integral MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Data MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

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

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

toConstr :: MetaId -> Constr #

dataTypeOf :: MetaId -> DataType #

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

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

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

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

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

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

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

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

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

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

Num MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Ord MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Real MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Show MetaId Source #

Show non-record version of this newtype.

Instance details

Defined in Agda.Syntax.Common

Generic MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep MetaId :: Type -> Type #

Methods

from :: MetaId -> Rep MetaId x #

to :: Rep MetaId x -> MetaId #

NFData MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

rnf :: MetaId -> () #

Hashable MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

hashWithSalt :: Int -> MetaId -> Int

hash :: MetaId -> Int

Pretty MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

GetDefs MetaId Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

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

HasFresh MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

PrettyTCM MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

UnFreezeMeta MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

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

IsInstantiatedMeta MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

FromTerm MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimTerm MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Unquote MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Singleton MetaId () Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

singleton :: MetaId -> () Source #

Singleton MetaId MetaSet Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Reify MetaId Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type Rep MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

type Rep MetaId = D1 ('MetaData "MetaId" "Agda.Syntax.Common" "Agda-2.6.1.3-inplace" 'True) (C1 ('MetaCons "MetaId" 'PrefixI 'True) (S1 ('MetaSel ('Just "metaId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Nat)))