Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Internal

Synopsis

class TermSize a where
class IsProjElim e where
class Suggest a b where
class SgTel a where
class TelToArgs a where
type ListTel = ListTel' ArgName
type ListTel' a = [Dom (a, Type)]
data EqualityView
- = EqualityType {
  - eqtSort :: Sort
  - eqtName :: QName
  - eqtParams :: [Arg Term]
  - eqtType :: Arg Term
  - eqtLhs :: Arg Term
  - eqtRhs :: Arg Term
  }
- | OtherType Type
type PatternSubstitution = Substitution' DeBruijnPattern
type Substitution = Substitution' Term
data Substitution' a
- = IdS
- | EmptyS Empty
- | a :# (Substitution' a)
- | Strengthen Empty (Substitution' a)
- | Wk !Int (Substitution' a)
- | Lift !Int (Substitution' a)
class PatternVars a b | b -> a where
data ConPatternInfo = ConPatternInfo {
- conPRecord :: Maybe PatOrigin
- conPType :: Maybe (Arg Type)
- conPLazy :: Bool
}
type DeBruijnPattern = Pattern' DBPatVar
data DBPatVar = DBPatVar {
- dbPatVarName :: PatVarName
- dbPatVarIndex :: Int
}
type Pattern = Pattern' PatVarName
data Pattern' x
- = VarP PatOrigin x
- | DotP PatOrigin Term
- | ConP ConHead ConPatternInfo [NamedArg (Pattern' x)]
- | LitP Literal
- | ProjP ProjOrigin QName
data PatOrigin
- = PatOSystem
- | PatOSplit
- | PatOVar Name
- | PatODot
- | PatOWild
- | PatOCon
- | PatORec
- | PatOLit
- | PatOAbsurd
type PatVarName = ArgName
data Clause = Clause {
- clauseLHSRange :: Range
- clauseFullRange :: Range
- clauseTel :: Telescope
- namedClausePats :: [NamedArg DeBruijnPattern]
- clauseBody :: Maybe Term
- clauseType :: Maybe (Arg Type)
- clauseCatchall :: Bool
- clauseUnreachable :: Maybe Bool
}
type Blocked_ = Blocked ()
data Blocked t
- = Blocked {
  - theBlockingMeta :: MetaId
  - ignoreBlocking :: t
  }
- | NotBlocked {
  - blockingStatus :: NotBlocked
  - ignoreBlocking :: t
  }
data NotBlocked
- = StuckOn Elim
- | Underapplied
- | AbsurdMatch
- | MissingClauses
- | ReallyNotBlocked
data LevelAtom
- = MetaLevel MetaId Elims
- | BlockedLevel MetaId Term
- | NeutralLevel NotBlocked Term
- | UnreducedLevel Term
data PlusLevel
- = ClosedLevel Integer
- | Plus Integer LevelAtom
newtype Level = Max [PlusLevel]
data Sort
- = Type Level
- | Prop
- | Inf
- | SizeUniv
- | PiSort Sort (Abs Sort)
- | UnivSort Sort
- | MetaS !MetaId Elims
type Telescope = Tele (Dom Type)
data Tele a
- = EmptyTel
- | ExtendTel a (Abs (Tele a))
class LensSort a where
type Type = Type' Term
data Type' a = El {
- _getSort :: Sort
- unEl :: a
}
data Abs a
- = Abs {
  - absName :: ArgName
  - unAbs :: a
  }
- | NoAbs {
  - absName :: ArgName
  - unAbs :: a
  }
type ArgName = String
type Elims = [Elim]
type Elim = Elim' Term
data Elim' a
- = Apply (Arg a)
- | Proj ProjOrigin QName
type ConInfo = ConOrigin
data Term
- = Var !Int Elims
- | Lam ArgInfo (Abs Term)
- | Lit Literal
- | Def QName Elims
- | Con ConHead ConInfo Elims
- | Pi (Dom Type) (Abs Type)
- | Sort Sort
- | Level Level
- | MetaV !MetaId Elims
- | DontCare Term
class LensConName a where
data ConHead = ConHead {
- conName :: QName
- conInductive :: Induction
- conFields :: [QName]
}
type NamedArgs = [NamedArg Term]
type Args = [Arg Term]
argNameToString :: ArgName -> String
stringToArgName :: String -> ArgName
appendArgNames :: ArgName -> ArgName -> ArgName
nameToArgName :: Name -> ArgName
stuckOn :: Elim -> NotBlocked -> NotBlocked
clausePats :: Clause -> [Arg DeBruijnPattern]
patVarNameToString :: PatVarName -> String
nameToPatVarName :: Name -> PatVarName
varP :: a -> Pattern' a
dotP :: Term -> Pattern' a
namedVarP :: PatVarName -> Named_ Pattern
namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern
noConPatternInfo :: ConPatternInfo
toConPatternInfo :: ConInfo -> ConPatternInfo
fromConPatternInfo :: ConPatternInfo -> ConInfo
patternOrigin :: Pattern' x -> Maybe PatOrigin
properlyMatching :: DeBruijnPattern -> Bool
isEqualityType :: EqualityView -> Bool
absurdBody :: Abs Term
isAbsurdBody :: Abs Term -> Bool
absurdPatternName :: PatVarName
isAbsurdPatternName :: PatVarName -> Bool
var :: Nat -> Term
dontCare :: Term -> Term
typeDontCare :: Type
topSort :: Type
sort :: Sort -> Type
varSort :: Int -> Sort
levelSuc :: Level -> Level
mkType :: Integer -> Sort
isSort :: Term -> Maybe Sort
impossibleTerm :: String -> Int -> Term
hackReifyToMeta :: Term
isHackReifyToMeta :: Term -> Bool
mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a)
mapAbsNames :: (ArgName -> ArgName) -> Tele a -> Tele a
replaceEmptyName :: ArgName -> Tele a -> Tele a
telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope
telFromList :: ListTel -> Telescope
telToList :: Telescope -> ListTel
blockingMeta :: Blocked t -> Maybe MetaId
blocked :: MetaId -> a -> Blocked a
notBlocked :: a -> Blocked a
stripDontCare :: Term -> Term
arity :: Type -> Nat
notInScopeName :: ArgName -> ArgName
unNotInScopeName :: ArgName -> ArgName
unSpine :: Term -> Term
unSpine' :: (ProjOrigin -> Bool) -> Term -> Term
hasElims :: Term -> Maybe (Elims -> Term, Elims)
argFromElim :: Elim' a -> Arg a
isApplyElim :: Elim' a -> Maybe (Arg a)
isApplyElim' :: Empty -> Elim' a -> Arg a
allApplyElims :: [Elim' a] -> Maybe [Arg a]
splitApplyElims :: [Elim' a] -> ([Arg a], [Elim' a])
dropProjElims :: IsProjElim e => [e] -> [e]
argsFromElims :: Elims -> Args
allProjElims :: Elims -> Maybe [(ProjOrigin, QName)]
pDom :: LensHiding a => a -> Doc -> Doc
module Agda.Syntax.Abstract.Name
newtype MetaId = MetaId {
- metaId :: Nat
}

Documentation

class TermSize a where #

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

Not counting towards the term size are:

sort and color annotations,
projections.

Minimal complete definition

tsize

Methods

termSize :: a -> Int #

tsize :: a -> Sum Int #

Instances

TermSize LevelAtom #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: LevelAtom -> Int # tsize :: LevelAtom -> Sum Int #
TermSize PlusLevel #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: PlusLevel -> Int # tsize :: PlusLevel -> Sum Int #
TermSize Level #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Level -> Int # tsize :: Level -> Sum Int #
TermSize Sort #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Sort -> Int # tsize :: Sort -> Sum Int #
TermSize Term #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Term -> Int # tsize :: Term -> Sum Int #
(Foldable t, TermSize a) => TermSize (t a) #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: t a -> Int # tsize :: t a -> Sum Int #
TermSize a => TermSize (Substitution' a) #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Substitution' a -> Int # tsize :: Substitution' a -> Sum Int #

class IsProjElim e where #

Minimal complete definition

isProjElim

Methods

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

Instances

IsProjElim Elim #
Instance details Defined in Agda.Syntax.Internal Methods isProjElim :: Elim -> Maybe (ProjOrigin, QName) #
IsProjElim e => IsProjElim (MaybeReduced e) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods isProjElim :: MaybeReduced e -> Maybe (ProjOrigin, QName) #

class Suggest a b where #

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

Minimal complete definition

suggest

Methods

suggest :: a -> b -> String #

Instances

Suggest String String #
Instance details Defined in Agda.Syntax.Internal Methods suggest :: String -> String -> String #
Suggest String (Abs b) #
Instance details Defined in Agda.Syntax.Internal Methods suggest :: String -> Abs b -> String #
Suggest Name (Abs b) #
Instance details Defined in Agda.Syntax.Internal Methods suggest :: Name -> Abs b -> String #
Suggest (Abs a) (Abs b) #
Instance details Defined in Agda.Syntax.Internal Methods suggest :: Abs a -> Abs b -> String #

class SgTel a where #

Constructing a singleton telescope.

Minimal complete definition

sgTel

Methods

sgTel :: a -> Telescope #

Instances

SgTel (Dom (ArgName, Type)) #
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom (ArgName, Type) -> Telescope #
SgTel (Dom Type) #
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom Type -> Telescope #
SgTel (ArgName, Dom Type) #
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: (ArgName, Dom Type) -> Telescope #

class TelToArgs a where #

Drop the types from a telescope.

Minimal complete definition

telToArgs

Methods

telToArgs :: a -> [Arg ArgName] #

Instances

TelToArgs ListTel #
Instance details Defined in Agda.Syntax.Internal Methods telToArgs :: ListTel -> [Arg ArgName] #
TelToArgs Telescope #
Instance details Defined in Agda.Syntax.Internal Methods telToArgs :: Telescope -> [Arg ArgName] #

type ListTel = ListTel' ArgName #

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

Telescope as list.

data EqualityView #

View type as equality type.

Constructors

EqualityType
Fields eqtSort :: Sort Sort of this type. eqtName :: QName Builtin EQUALITY. eqtParams :: [Arg Term] Hidden. Empty or `Level`. eqtType :: Arg Term Hidden eqtLhs :: Arg Term NotHidden eqtRhs :: Arg Term NotHidden
OtherType Type	reduced

Instances

Free EqualityView #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => EqualityView -> FreeM c #
TermLike EqualityView #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> EqualityView -> m EqualityView # foldTerm :: Monoid m => (Term -> m) -> EqualityView -> m #
PrettyTCM EqualityView #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: EqualityView -> TCM Doc #
InstantiateFull EqualityView #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: EqualityView -> ReduceM EqualityView #
Normalise EqualityView #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: EqualityView -> ReduceM EqualityView #
Simplify EqualityView #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: EqualityView -> ReduceM EqualityView #
Reduce EqualityView #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: EqualityView -> ReduceM EqualityView # reduceB' :: EqualityView -> ReduceM (Blocked EqualityView) #
Instantiate EqualityView #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: EqualityView -> ReduceM EqualityView #
Subst Term EqualityView #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> EqualityView -> EqualityView #

type PatternSubstitution = Substitution' DeBruijnPattern #

type Substitution = Substitution' Term #

data Substitution' a #

Substitutions.

Constructors

IdS	Identity substitution. `Γ ⊢ IdS : Γ`
EmptyS Empty	Empty substitution, lifts from the empty context. First argument is `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)	Weakning substitution, lifts to an extended context. `Γ ⊢ ρ : Δ ------------------- Γ, Ψ ⊢ Wk \|Ψ\| ρ : Δ`
Lift !Int (Substitution' a)	Lifting substitution. Use this to go under a binder. `Lift 1 ρ == var 0 :# Wk 1 ρ`. `Γ ⊢ ρ : Δ ------------------------- Γ, Ψρ ⊢ Lift \|Ψ\| ρ : Δ, Ψ`

Instances

Functor Substitution' #
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Substitution' a -> Substitution' b # (<$) :: a -> Substitution' b -> Substitution' a #
Foldable Substitution' #
Instance details Defined in Agda.Syntax.Internal Methods fold :: Monoid m => Substitution' m -> m # foldMap :: Monoid m => (a -> m) -> Substitution' a -> m # foldr :: (a -> b -> b) -> b -> Substitution' a -> b # foldr' :: (a -> b -> b) -> b -> Substitution' a -> b # foldl :: (b -> a -> b) -> b -> Substitution' a -> b # foldl' :: (b -> a -> b) -> b -> Substitution' a -> b # foldr1 :: (a -> a -> a) -> Substitution' a -> a # foldl1 :: (a -> a -> a) -> Substitution' a -> a # toList :: Substitution' a -> [a] # null :: Substitution' a -> Bool # length :: Substitution' a -> Int # elem :: Eq a => a -> Substitution' a -> Bool # maximum :: Ord a => Substitution' a -> a # minimum :: Ord a => Substitution' a -> a # sum :: Num a => Substitution' a -> a # product :: Num a => Substitution' a -> a #
Traversable Substitution' #
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 #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Substitution #
InstantiateFull Substitution #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Substitution -> ReduceM Substitution #
Subst a a => Subst a (Substitution' a) #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' a -> Substitution' a -> Substitution' a #
Eq (Substitution' Term) #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Substitution' Term -> Substitution' Term -> Bool # (/=) :: Substitution' Term -> Substitution' Term -> Bool #
Data a => Data (Substitution' a) #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Substitution' a -> c (Substitution' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Substitution' a) # toConstr :: Substitution' a -> Constr # dataTypeOf :: Substitution' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Substitution' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Substitution' a)) # gmapT :: (forall b. Data b => b -> b) -> Substitution' a -> Substitution' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Substitution' a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Substitution' a -> r # gmapQ :: (forall d. Data d => d -> u) -> Substitution' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Substitution' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Substitution' a -> m (Substitution' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Substitution' a -> m (Substitution' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Substitution' a -> m (Substitution' a) #
Ord (Substitution' Term) #
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Substitution' Term -> Substitution' Term -> Ordering # (<) :: Substitution' Term -> Substitution' Term -> Bool # (<=) :: Substitution' Term -> Substitution' Term -> Bool # (>) :: Substitution' Term -> Substitution' Term -> Bool # (>=) :: Substitution' Term -> Substitution' Term -> Bool # max :: Substitution' Term -> Substitution' Term -> Substitution' Term # min :: Substitution' Term -> Substitution' Term -> Substitution' Term #
Show a => Show (Substitution' a) #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Substitution' a -> ShowS # show :: Substitution' a -> String # showList :: [Substitution' a] -> ShowS #
Null (Substitution' a) #
Instance details Defined in Agda.Syntax.Internal Methods empty :: Substitution' a # null :: Substitution' a -> Bool #
Pretty a => Pretty (Substitution' a) #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Substitution' a -> Doc # prettyPrec :: Int -> Substitution' a -> Doc # prettyList :: [Substitution' a] -> Doc #
TermSize a => TermSize (Substitution' a) #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Substitution' a -> Int # tsize :: Substitution' a -> Sum Int #
EmbPrj a => EmbPrj (Substitution' a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Substitution' a -> S Int32 # icod_ :: Substitution' a -> S Int32 # value :: Int32 -> R (Substitution' a) #
(Pretty a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a) #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Substitution' a -> TCM Doc #

class PatternVars a b | b -> a where #

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

Minimal complete definition

patternVars

Methods

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

Instances

PatternVars a b => PatternVars a [b] #
Instance details Defined in Agda.Syntax.Internal Methods patternVars :: [b] -> [Arg (Either a Term)] #
PatternVars a (NamedArg (Pattern' a)) #
Instance details Defined in Agda.Syntax.Internal Methods patternVars :: NamedArg (Pattern' a) -> [Arg (Either a Term)] #
PatternVars a (Arg (Pattern' a)) #
Instance details Defined in Agda.Syntax.Internal Methods patternVars :: Arg (Pattern' a) -> [Arg (Either a Term)] #

data ConPatternInfo #

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

Constructors

ConPatternInfo

Fields

conPRecord :: Maybe PatOrigin
Nothing if data constructor. Just if record constructor.
conPType :: Maybe (Arg Type)
The type of the whole constructor pattern. Should be present (Just) if constructor pattern is is generated ordinarily by type-checking. Could be absent (Nothing) if pattern comes from some plugin (like Agsy). Needed e.g. for with-clause stripping.
conPLazy :: Bool
Lazy patterns are generated by the forcing translation (forcingTranslation) and are dropped by the clause compiler (TODO: not yet) (compileClauses) when the variables they bind are unused. The GHC backend compiles lazy matches to lazy patterns in Haskell (TODO: not yet).

Instances

Data ConPatternInfo #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConPatternInfo -> c ConPatternInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConPatternInfo # toConstr :: ConPatternInfo -> Constr # dataTypeOf :: ConPatternInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConPatternInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConPatternInfo) # gmapT :: (forall b. Data b => b -> b) -> ConPatternInfo -> ConPatternInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConPatternInfo -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConPatternInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> ConPatternInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ConPatternInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConPatternInfo -> m ConPatternInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConPatternInfo -> m ConPatternInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConPatternInfo -> m ConPatternInfo #
Show ConPatternInfo #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> ConPatternInfo -> ShowS # show :: ConPatternInfo -> String # showList :: [ConPatternInfo] -> ShowS #
KillRange ConPatternInfo #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT ConPatternInfo #
EmbPrj ConPatternInfo #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ConPatternInfo -> S Int32 # icod_ :: ConPatternInfo -> S Int32 # value :: Int32 -> R ConPatternInfo #
InstantiateFull ConPatternInfo #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ConPatternInfo -> ReduceM ConPatternInfo #
Normalise ConPatternInfo #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: ConPatternInfo -> ReduceM ConPatternInfo #
Subst Term ConPatternInfo #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> ConPatternInfo -> ConPatternInfo #

type DeBruijnPattern = Pattern' DBPatVar #

data DBPatVar #

Type used when numbering pattern variables.

Constructors

DBPatVar
Fields dbPatVarName :: PatVarName dbPatVarIndex :: Int

Instances

Eq DBPatVar #
Instance details Defined in Agda.Syntax.Internal Methods (==) :: DBPatVar -> DBPatVar -> Bool # (/=) :: DBPatVar -> DBPatVar -> Bool #
Data DBPatVar #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DBPatVar -> c DBPatVar # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DBPatVar # toConstr :: DBPatVar -> Constr # dataTypeOf :: DBPatVar -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DBPatVar) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DBPatVar) # gmapT :: (forall b. Data b => b -> b) -> DBPatVar -> DBPatVar # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DBPatVar -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DBPatVar -> r # gmapQ :: (forall d. Data d => d -> u) -> DBPatVar -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> DBPatVar -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> DBPatVar -> m DBPatVar # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DBPatVar -> m DBPatVar # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DBPatVar -> m DBPatVar #
Show DBPatVar #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> DBPatVar -> ShowS # show :: DBPatVar -> String # showList :: [DBPatVar] -> ShowS #
Pretty DBPatVar #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: DBPatVar -> Doc # prettyPrec :: Int -> DBPatVar -> Doc # prettyList :: [DBPatVar] -> Doc #
KillRange DBPatVar #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT DBPatVar #
DeBruijn DeBruijnPattern #
Instance details Defined in Agda.TypeChecking.Substitute Methods deBruijnVar :: Int -> DeBruijnPattern # debruijnNamedVar :: String -> Int -> DeBruijnPattern # deBruijnView :: DeBruijnPattern -> Maybe Int #
EmbPrj DBPatVar #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DBPatVar -> S Int32 # icod_ :: DBPatVar -> S Int32 # value :: Int32 -> R DBPatVar #
PrettyTCM DBPatVar #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: DBPatVar -> TCM Doc #
InstantiateFull DBPatVar #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: DBPatVar -> ReduceM DBPatVar #
Normalise DBPatVar #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: DBPatVar -> ReduceM DBPatVar #
UsableSizeVars DeBruijnPattern #
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: DeBruijnPattern -> TerM VarSet #
UsableSizeVars MaskedDeBruijnPatterns #
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: MaskedDeBruijnPatterns -> TerM VarSet #
Subst DeBruijnPattern DeBruijnPattern #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' DeBruijnPattern -> DeBruijnPattern -> DeBruijnPattern #
LabelPatVars Pattern DeBruijnPattern Int #
Instance details Defined in Agda.Syntax.Internal.Pattern Methods labelPatVars :: Pattern -> State [Int] DeBruijnPattern # unlabelPatVars :: DeBruijnPattern -> Pattern #
UsableSizeVars [DeBruijnPattern] #
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: [DeBruijnPattern] -> TerM VarSet #
UsableSizeVars (Masked DeBruijnPattern) #
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet #

type Pattern #

Arguments

= Pattern' PatVarName

The PatVarName is a name suggestion.

data Pattern' x #

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

Constructors

VarP PatOrigin x	x
DotP PatOrigin Term	.t
ConP ConHead ConPatternInfo [NamedArg (Pattern' x)]	`c ps` The subpatterns do not contain any projection copatterns.
LitP Literal	E.g. `5`, `"hello"`.
ProjP ProjOrigin QName	Projection copattern. Can only appear by itself.

Instances

Functor Pattern' #
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Pattern' a -> Pattern' b # (<$) :: a -> Pattern' b -> Pattern' a #
Foldable Pattern' #
Instance details Defined in Agda.Syntax.Internal Methods fold :: Monoid m => Pattern' m -> m # foldMap :: Monoid m => (a -> m) -> Pattern' a -> m # foldr :: (a -> b -> b) -> b -> Pattern' a -> b # foldr' :: (a -> b -> b) -> b -> Pattern' a -> b # foldl :: (b -> a -> b) -> b -> Pattern' a -> b # foldl' :: (b -> a -> b) -> b -> Pattern' a -> b # foldr1 :: (a -> a -> a) -> Pattern' a -> a # foldl1 :: (a -> a -> a) -> Pattern' a -> a # toList :: Pattern' a -> [a] # null :: Pattern' a -> Bool # length :: Pattern' a -> Int # elem :: Eq a => a -> Pattern' a -> Bool # maximum :: Ord a => Pattern' a -> a # minimum :: Ord a => Pattern' a -> a # sum :: Num a => Pattern' a -> a # product :: Num a => Pattern' a -> a #
Traversable Pattern' #
Instance details Defined in Agda.Syntax.Internal Methods traverse :: Applicative f => (a -> f b) -> Pattern' a -> f (Pattern' b) # sequenceA :: Applicative f => Pattern' (f a) -> f (Pattern' a) # mapM :: Monad m => (a -> m b) -> Pattern' a -> m (Pattern' b) # sequence :: Monad m => Pattern' (m a) -> m (Pattern' a) #
DeBruijn DeBruijnPattern #
Instance details Defined in Agda.TypeChecking.Substitute Methods deBruijnVar :: Int -> DeBruijnPattern # debruijnNamedVar :: String -> Int -> DeBruijnPattern # deBruijnView :: DeBruijnPattern -> Maybe Int #
DeBruijn SplitPattern #
Instance details Defined in Agda.TypeChecking.Coverage.Match Methods deBruijnVar :: Int -> SplitPattern # debruijnNamedVar :: String -> Int -> SplitPattern # deBruijnView :: SplitPattern -> Maybe Int #
UsableSizeVars DeBruijnPattern #
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: DeBruijnPattern -> TerM VarSet #
UsableSizeVars MaskedDeBruijnPatterns #
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: MaskedDeBruijnPatterns -> TerM VarSet #
UniverseBi Elims Pattern #
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: Elims -> [Pattern] #
UniverseBi Args Pattern #
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: Args -> [Pattern] #
Subst DeBruijnPattern DeBruijnPattern #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' DeBruijnPattern -> DeBruijnPattern -> DeBruijnPattern #
Subst Term Pattern #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Pattern -> Pattern #
Subst SplitPattern SplitPattern #
Instance details Defined in Agda.TypeChecking.Coverage.Match Methods applySubst :: Substitution' SplitPattern -> SplitPattern -> SplitPattern #
LabelPatVars Pattern DeBruijnPattern Int #
Instance details Defined in Agda.Syntax.Internal.Pattern Methods labelPatVars :: Pattern -> State [Int] DeBruijnPattern # unlabelPatVars :: DeBruijnPattern -> Pattern #
PatternVars a (NamedArg (Pattern' a)) #
Instance details Defined in Agda.Syntax.Internal Methods patternVars :: NamedArg (Pattern' a) -> [Arg (Either a Term)] #
PatternVars a (Arg (Pattern' a)) #
Instance details Defined in Agda.Syntax.Internal Methods patternVars :: Arg (Pattern' a) -> [Arg (Either a Term)] #
PatternLike a (Pattern' a) #
Instance details Defined in Agda.Syntax.Internal.Pattern Methods foldrPattern :: Monoid m => (Pattern' a -> m -> m) -> Pattern' a -> m # traversePatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a) #
MapNamedArgPattern a (NamedArg (Pattern' a)) #	Modify the content of `VarP`, and the closest surrounding `NamedArg`. Note: the `mapNamedArg` for `Pattern'` is not expressible simply by `fmap` or `traverse` etc., since `ConP` has `NamedArg` subpatterns, which are taken into account by `mapNamedArg`.
Instance details Defined in Agda.Syntax.Internal.Pattern Methods mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> NamedArg (Pattern' a) -> NamedArg (Pattern' a) #
DeBruijn (Pattern' a) => TermToPattern Term (Pattern' a) #
Instance details Defined in Agda.TypeChecking.Patterns.Internal Methods termToPattern :: Term -> TCM (Pattern' a) #
Conversion TOM (Arg Pattern) (Pat O) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Arg Pattern -> TOM (Pat O) #
Data x => Data (Pattern' x) #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pattern' x -> c (Pattern' x) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Pattern' x) # toConstr :: Pattern' x -> Constr # dataTypeOf :: Pattern' x -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Pattern' x)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Pattern' x)) # gmapT :: (forall b. Data b => b -> b) -> Pattern' x -> Pattern' x # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pattern' x -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pattern' x -> r # gmapQ :: (forall d. Data d => d -> u) -> Pattern' x -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Pattern' x -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pattern' x -> m (Pattern' x) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern' x -> m (Pattern' x) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern' x -> m (Pattern' x) #
Show x => Show (Pattern' x) #
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) #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Pattern' a -> Doc # prettyPrec :: Int -> Pattern' a -> Doc # prettyList :: [Pattern' a] -> Doc #
KillRange a => KillRange (Pattern' a) #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Pattern' a) #
IsProjP (Pattern' a) #
Instance details Defined in Agda.Syntax.Internal Methods isProjP :: Pattern' a -> Maybe (ProjOrigin, AmbiguousQName) #
Apply [NamedArg (Pattern' a)] #	Make sure we only drop variable patterns.
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: [NamedArg (Pattern' a)] -> Args -> [NamedArg (Pattern' a)] # applyE :: [NamedArg (Pattern' a)] -> Elims -> [NamedArg (Pattern' a)] #
CountPatternVars (Pattern' x) #
Instance details Defined in Agda.Syntax.Internal.Pattern Methods countPatternVars :: Pattern' x -> Int #
EmbPrj a => EmbPrj (Pattern' a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Pattern' a -> S Int32 # icod_ :: Pattern' a -> S Int32 # value :: Int32 -> R (Pattern' a) #
PrettyTCM a => PrettyTCM (Pattern' a) #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Pattern' a -> TCM Doc #
NamesIn (Pattern' a) #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Pattern' a -> Set QName #
InstantiateFull a => InstantiateFull (Pattern' a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Pattern' a -> ReduceM (Pattern' a) #
Normalise a => Normalise (Pattern' a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Pattern' a -> ReduceM (Pattern' a) #
NormaliseProjP (Pattern' x) #
Instance details Defined in Agda.TypeChecking.Records Methods normaliseProjP :: HasConstInfo m => Pattern' x -> m (Pattern' x) #
IsFlexiblePattern (Pattern' a) #
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: Pattern' a -> MaybeT TCM FlexibleVarKind # isFlexiblePattern :: Pattern' a -> TCM Bool #
UsableSizeVars [DeBruijnPattern] #
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: [DeBruijnPattern] -> TerM VarSet #
UsableSizeVars (Masked DeBruijnPattern) #
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet #
PatternVarModalities (Pattern' x) x #
Instance details Defined in Agda.Syntax.Internal.Pattern Methods patternVarModalities :: Pattern' x -> [(x, Modality)] #
UniverseBi ([Type], [Clause]) Pattern #
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: ([Type], [Clause]) -> [Pattern] #

data PatOrigin #

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

Constructors

PatOSystem	Pattern inserted by the system
PatOSplit	Pattern generated by case split
PatOVar Name	User wrote a variable pattern
PatODot	User wrote a dot pattern
PatOWild	User wrote a wildcard pattern
PatOCon	User wrote a constructor pattern
PatORec	User wrote a record pattern
PatOLit	User wrote a literal pattern
PatOAbsurd	User wrote an absurd pattern

Instances

Eq PatOrigin #
Instance details Defined in Agda.Syntax.Internal Methods (==) :: PatOrigin -> PatOrigin -> Bool # (/=) :: PatOrigin -> PatOrigin -> Bool #
Data PatOrigin #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PatOrigin -> c PatOrigin # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PatOrigin # toConstr :: PatOrigin -> Constr # dataTypeOf :: PatOrigin -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PatOrigin) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PatOrigin) # gmapT :: (forall b. Data b => b -> b) -> PatOrigin -> PatOrigin # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PatOrigin -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PatOrigin -> r # gmapQ :: (forall d. Data d => d -> u) -> PatOrigin -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> PatOrigin -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> PatOrigin -> m PatOrigin # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PatOrigin -> m PatOrigin # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PatOrigin -> m PatOrigin #
Show PatOrigin #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> PatOrigin -> ShowS # show :: PatOrigin -> String # showList :: [PatOrigin] -> ShowS #
KillRange PatOrigin #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT PatOrigin #
EmbPrj PatOrigin #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: PatOrigin -> S Int32 # icod_ :: PatOrigin -> S Int32 # value :: Int32 -> R PatOrigin #

type PatVarName = ArgName #

Pattern variables.

data Clause #

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

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

clauseTel ~ permute clausePerm (patternVars namedClausePats)

Terms in dot patterns are valid in the clause telescope.

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

Constructors

Clause

Fields

clauseLHSRange :: Range
clauseFullRange :: Range
clauseTel :: Telescope
Δ: The types of the pattern variables in dependency order.
namedClausePats :: [NamedArg DeBruijnPattern]
Δ ⊢ ps. The de Bruijn indices refer to Δ.
clauseBody :: Maybe Term
Just v with Δ ⊢ v for a regular clause, or Nothing for an absurd one.
clauseType :: Maybe (Arg Type)
Δ ⊢ t. The type of the rhs under clauseTel. Used, e.g., by TermCheck. Can be Irrelevant if we encountered an irrelevant projection pattern on the lhs.
clauseCatchall :: Bool
Clause has been labelled as CATCHALL.
clauseUnreachable :: Maybe Bool
Clause has been labelled as unreachable by the coverage checker. Nothing means coverage checker has not run yet (clause may be unreachable). Just False means clause is not unreachable. Just True means clause is unreachable.

Instances

Data Clause #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Clause -> c Clause # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Clause # toConstr :: Clause -> Constr # dataTypeOf :: Clause -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Clause) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Clause) # gmapT :: (forall b. Data b => b -> b) -> Clause -> Clause # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r # gmapQ :: (forall d. Data d => d -> u) -> Clause -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Clause -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Clause -> m Clause # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause -> m Clause # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause -> m Clause #
Show Clause #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Clause -> ShowS # show :: Clause -> String # showList :: [Clause] -> ShowS #
Null Clause #	A `null` clause is one with no patterns and no rhs. Should not exist in practice.
Instance details Defined in Agda.Syntax.Internal Methods empty :: Clause # null :: Clause -> Bool #
Pretty Clause #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Clause -> Doc # prettyPrec :: Int -> Clause -> Doc # prettyList :: [Clause] -> Doc #
KillRange Clause #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Clause #
HasRange Clause #
Instance details Defined in Agda.Syntax.Internal Methods getRange :: Clause -> Range #
Free Clause #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Clause -> FreeM c #
Abstract Clause #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Clause -> Clause #
Abstract FunctionInverse #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> FunctionInverse -> FunctionInverse #
Apply Clause #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Clause -> Args -> Clause # applyE :: Clause -> Elims -> Clause #
Apply FunctionInverse #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: FunctionInverse -> Args -> FunctionInverse # applyE :: FunctionInverse -> Elims -> FunctionInverse #
GetDefs Clause #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Clause -> m () #
FunArity Clause #	Get the number of initial `Apply` patterns in a clause.
Instance details Defined in Agda.Syntax.Internal.Pattern Methods funArity :: Clause -> Int #
Free Clause #
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: Clause -> FreeT
EmbPrj Clause #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Clause -> S Int32 # icod_ :: Clause -> S Int32 # value :: Int32 -> R Clause #
PrettyTCM Clause #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Clause -> TCM Doc #
DropArgs Clause #	NOTE: does not work for recursive functions.
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> Clause -> Clause #
DropArgs FunctionInverse #
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> FunctionInverse -> FunctionInverse #
NamesIn Clause #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Clause -> Set QName #
InstantiateFull Clause #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Clause -> ReduceM Clause #
InstantiateFull FunctionInverse #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: FunctionInverse -> ReduceM FunctionInverse #
NormaliseProjP Clause #
Instance details Defined in Agda.TypeChecking.Records Methods normaliseProjP :: HasConstInfo m => Clause -> m Clause #
ComputeOccurrences Clause #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Clause -> OccM OccurrencesBuilder #
Occurs Clause #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Clause -> TCM Clause # metaOccurs :: MetaId -> Clause -> TCM () #
Conversion TOM Clause (Maybe ([Pat O], MExp O)) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) #
Conversion TOM [Clause] [([Pat O], MExp O)] #
Instance details Defined in Agda.Auto.Convert Methods convert :: [Clause] -> TOM [([Pat O], MExp O)] #
FunArity [Clause] #	Get the number of common initial `Apply` patterns in a list of clauses.
Instance details Defined in Agda.Syntax.Internal.Pattern Methods funArity :: [Clause] -> Int #
PrettyTCM (QNamed Clause) #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: QNamed Clause -> TCM Doc #
Reify (QNamed Clause) Clause #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: QNamed Clause0 -> TCM Clause # reifyWhen :: Bool -> QNamed Clause0 -> TCM Clause #
UniverseBi ([Type], [Clause]) Pattern #
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: ([Type], [Clause]) -> [Pattern] #
UniverseBi ([Type], [Clause]) Term #
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: ([Type], [Clause]) -> [Term] #

type Blocked_ = Blocked () #

Blocked t without the t.

data Blocked t #

Something where a meta variable may block reduction.

Constructors

Blocked
Fields theBlockingMeta :: MetaId ignoreBlocking :: t
NotBlocked
Fields blockingStatus :: NotBlocked ignoreBlocking :: t

Instances

Functor Blocked #
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Blocked a -> Blocked b # (<$) :: a -> Blocked b -> Blocked a #
Applicative Blocked #	Blocking by a meta is dominant.
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 #
Instance details Defined in Agda.Syntax.Internal Methods fold :: Monoid m => Blocked m -> m # foldMap :: Monoid m => (a -> m) -> Blocked a -> m # foldr :: (a -> b -> b) -> b -> Blocked a -> b # foldr' :: (a -> b -> b) -> b -> Blocked a -> b # foldl :: (b -> a -> b) -> b -> Blocked a -> b # foldl' :: (b -> a -> b) -> b -> Blocked a -> b # foldr1 :: (a -> a -> a) -> Blocked a -> a # foldl1 :: (a -> a -> a) -> Blocked a -> a # toList :: Blocked a -> [a] # null :: Blocked a -> Bool # length :: Blocked a -> Int # elem :: Eq a => a -> Blocked a -> Bool # maximum :: Ord a => Blocked a -> a # minimum :: Ord a => Blocked a -> a # sum :: Num a => Blocked a -> a # product :: Num a => Blocked a -> a #
Traversable Blocked #
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_ #
Instance details Defined in Agda.Syntax.Internal Methods (<>) :: Blocked_ -> Blocked_ -> Blocked_ # sconcat :: NonEmpty Blocked_ -> Blocked_ # stimes :: Integral b => b -> Blocked_ -> Blocked_ #
Monoid Blocked_ #
Instance details Defined in Agda.Syntax.Internal Methods mempty :: Blocked_ # mappend :: Blocked_ -> Blocked_ -> Blocked_ # mconcat :: [Blocked_] -> Blocked_ #
Subst t a => Subst t (Blocked a) #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Blocked a -> Blocked a #
Eq t => Eq (Blocked t) #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Blocked t -> Blocked t -> Bool # (/=) :: Blocked t -> Blocked t -> Bool #
Show t => Show (Blocked t) #
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) #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Blocked a) #
Apply t => Apply (Blocked t) #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Blocked t -> Args -> Blocked t # applyE :: Blocked t -> Elims -> Blocked t #
TermLike a => TermLike (Blocked a) #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Blocked a -> m (Blocked a) # foldTerm :: Monoid m => (Term -> m) -> Blocked a -> m #
PrettyTCM a => PrettyTCM (Blocked a) #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Blocked a -> TCM Doc #
Instantiate a => Instantiate (Blocked a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Blocked a -> ReduceM (Blocked a) #

data NotBlocked #

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

Constructors

StuckOn Elim	The `Elim` is neutral and blocks a pattern match.
Underapplied	Not enough arguments were supplied to complete the matching.
AbsurdMatch	We matched an absurd clause, results in a neutral `Def`.
MissingClauses	We ran out of clauses, all considered clauses produced an actual mismatch. This can happen when try to reduce a function application but we are still missing some function clauses. See Agda.TypeChecking.Patterns.Match.
ReallyNotBlocked	Reduction was not blocked, we reached a whnf which can be anything but a stuck `Def`.

Instances

Eq NotBlocked #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: NotBlocked -> NotBlocked -> Bool # (/=) :: NotBlocked -> NotBlocked -> Bool #
Data NotBlocked #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NotBlocked -> c NotBlocked # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NotBlocked # toConstr :: NotBlocked -> Constr # dataTypeOf :: NotBlocked -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NotBlocked) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NotBlocked) # gmapT :: (forall b. Data b => b -> b) -> NotBlocked -> NotBlocked # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NotBlocked -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NotBlocked -> r # gmapQ :: (forall d. Data d => d -> u) -> NotBlocked -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> NotBlocked -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> NotBlocked -> m NotBlocked # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NotBlocked -> m NotBlocked # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NotBlocked -> m NotBlocked #
Show NotBlocked #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> NotBlocked -> ShowS # show :: NotBlocked -> String # showList :: [NotBlocked] -> ShowS #
Semigroup NotBlocked #	`ReallyNotBlocked` is the unit. `MissingClauses` is dominant. `StuckOn{}` should be propagated, if tied, we take the left.
Instance details Defined in Agda.Syntax.Internal Methods (<>) :: NotBlocked -> NotBlocked -> NotBlocked # sconcat :: NonEmpty NotBlocked -> NotBlocked # stimes :: Integral b => b -> NotBlocked -> NotBlocked #
Monoid NotBlocked #
Instance details Defined in Agda.Syntax.Internal Methods mempty :: NotBlocked # mappend :: NotBlocked -> NotBlocked -> NotBlocked # mconcat :: [NotBlocked] -> NotBlocked #

data LevelAtom #

An atomic term of type Level.

Constructors

MetaLevel MetaId Elims	A meta variable targeting `Level` under some eliminations.
BlockedLevel MetaId Term	A term of type `Level` whose reduction is blocked by a meta.
NeutralLevel NotBlocked Term	A neutral term of type `Level`.
UnreducedLevel Term	Introduced by `instantiate`, removed by `reduce`.

Instances

Eq LevelAtom #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: LevelAtom -> LevelAtom -> Bool # (/=) :: LevelAtom -> LevelAtom -> Bool #
Data LevelAtom #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LevelAtom -> c LevelAtom # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LevelAtom # toConstr :: LevelAtom -> Constr # dataTypeOf :: LevelAtom -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LevelAtom) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LevelAtom) # gmapT :: (forall b. Data b => b -> b) -> LevelAtom -> LevelAtom # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LevelAtom -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LevelAtom -> r # gmapQ :: (forall d. Data d => d -> u) -> LevelAtom -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LevelAtom -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LevelAtom -> m LevelAtom # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LevelAtom -> m LevelAtom # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LevelAtom -> m LevelAtom #
Ord LevelAtom #
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: LevelAtom -> LevelAtom -> Ordering # (<) :: LevelAtom -> LevelAtom -> Bool # (<=) :: LevelAtom -> LevelAtom -> Bool # (>) :: LevelAtom -> LevelAtom -> Bool # (>=) :: LevelAtom -> LevelAtom -> Bool # max :: LevelAtom -> LevelAtom -> LevelAtom # min :: LevelAtom -> LevelAtom -> LevelAtom #
Show LevelAtom #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> LevelAtom -> ShowS # show :: LevelAtom -> String # showList :: [LevelAtom] -> ShowS #
NFData LevelAtom #
Instance details Defined in Agda.Syntax.Internal Methods rnf :: LevelAtom -> () #
Pretty LevelAtom #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: LevelAtom -> Doc # prettyPrec :: Int -> LevelAtom -> Doc # prettyList :: [LevelAtom] -> Doc #
KillRange LevelAtom #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT LevelAtom #
TermSize LevelAtom #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: LevelAtom -> Int # tsize :: LevelAtom -> Sum Int #
DeBruijn LevelAtom #
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> LevelAtom # debruijnNamedVar :: String -> Int -> LevelAtom # deBruijnView :: LevelAtom -> Maybe Int #
PrecomputeFreeVars LevelAtom #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: LevelAtom -> FV LevelAtom #
Free LevelAtom #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => LevelAtom -> FreeM c #
TermLike LevelAtom #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> LevelAtom -> m LevelAtom # foldTerm :: Monoid m => (Term -> m) -> LevelAtom -> m #
GetDefs LevelAtom #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => LevelAtom -> m () #
Free LevelAtom #
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: LevelAtom -> FreeT
EmbPrj LevelAtom #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: LevelAtom -> S Int32 # icod_ :: LevelAtom -> S Int32 # value :: Int32 -> R LevelAtom #
NamesIn LevelAtom #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: LevelAtom -> Set QName #
UnFreezeMeta LevelAtom #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: LevelAtom -> TCM () #
IsInstantiatedMeta LevelAtom #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: LevelAtom -> TCM Bool #
MentionsMeta LevelAtom #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> LevelAtom -> Bool #
InstantiateFull LevelAtom #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: LevelAtom -> ReduceM LevelAtom #
Normalise LevelAtom #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: LevelAtom -> ReduceM LevelAtom #
Simplify LevelAtom #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: LevelAtom -> ReduceM LevelAtom #
Reduce LevelAtom #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: LevelAtom -> ReduceM LevelAtom # reduceB' :: LevelAtom -> ReduceM (Blocked LevelAtom) #
Instantiate LevelAtom #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: LevelAtom -> ReduceM LevelAtom #
SynEq LevelAtom #
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: LevelAtom -> LevelAtom -> SynEqM (LevelAtom, LevelAtom) synEq' :: LevelAtom -> LevelAtom -> SynEqM (LevelAtom, LevelAtom)
HasPolarity LevelAtom #
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> LevelAtom -> TCM [Polarity] #
UsableRelevance LevelAtom #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> LevelAtom -> TCM Bool #
ComputeOccurrences LevelAtom #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: LevelAtom -> OccM OccurrencesBuilder #
FoldRigid LevelAtom #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> LevelAtom -> TCM m #
Occurs LevelAtom #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> LevelAtom -> TCM LevelAtom # metaOccurs :: MetaId -> LevelAtom -> TCM () #
AbsTerm LevelAtom #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> LevelAtom -> LevelAtom #
Subst Term LevelAtom #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> LevelAtom -> LevelAtom #

data PlusLevel #

Constructors

ClosedLevel Integer	`n`, to represent `Setₙ`.
Plus Integer LevelAtom	`n + ℓ`.

Instances

Eq PlusLevel #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: PlusLevel -> PlusLevel -> Bool # (/=) :: PlusLevel -> PlusLevel -> Bool #
Data PlusLevel #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PlusLevel -> c PlusLevel # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PlusLevel # toConstr :: PlusLevel -> Constr # dataTypeOf :: PlusLevel -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PlusLevel) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PlusLevel) # gmapT :: (forall b. Data b => b -> b) -> PlusLevel -> PlusLevel # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PlusLevel -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PlusLevel -> r # gmapQ :: (forall d. Data d => d -> u) -> PlusLevel -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> PlusLevel -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> PlusLevel -> m PlusLevel # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PlusLevel -> m PlusLevel # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PlusLevel -> m PlusLevel #
Ord PlusLevel #
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: PlusLevel -> PlusLevel -> Ordering # (<) :: PlusLevel -> PlusLevel -> Bool # (<=) :: PlusLevel -> PlusLevel -> Bool # (>) :: PlusLevel -> PlusLevel -> Bool # (>=) :: PlusLevel -> PlusLevel -> Bool # max :: PlusLevel -> PlusLevel -> PlusLevel # min :: PlusLevel -> PlusLevel -> PlusLevel #
Show PlusLevel #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> PlusLevel -> ShowS # show :: PlusLevel -> String # showList :: [PlusLevel] -> ShowS #
NFData PlusLevel #
Instance details Defined in Agda.Syntax.Internal Methods rnf :: PlusLevel -> () #
Pretty PlusLevel #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: PlusLevel -> Doc # prettyPrec :: Int -> PlusLevel -> Doc # prettyList :: [PlusLevel] -> Doc #
KillRange PlusLevel #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT PlusLevel #
TermSize PlusLevel #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: PlusLevel -> Int # tsize :: PlusLevel -> Sum Int #
DeBruijn PlusLevel #
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> PlusLevel # debruijnNamedVar :: String -> Int -> PlusLevel # deBruijnView :: PlusLevel -> Maybe Int #
PrecomputeFreeVars PlusLevel #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: PlusLevel -> FV PlusLevel #
Free PlusLevel #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => PlusLevel -> FreeM c #
TermLike PlusLevel #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> PlusLevel -> m PlusLevel # foldTerm :: Monoid m => (Term -> m) -> PlusLevel -> m #
GetDefs PlusLevel #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => PlusLevel -> m () #
Free PlusLevel #
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: PlusLevel -> FreeT
EmbPrj PlusLevel #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: PlusLevel -> S Int32 # icod_ :: PlusLevel -> S Int32 # value :: Int32 -> R PlusLevel #
NamesIn PlusLevel #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: PlusLevel -> Set QName #
UnFreezeMeta PlusLevel #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: PlusLevel -> TCM () #
IsInstantiatedMeta PlusLevel #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: PlusLevel -> TCM Bool #
MentionsMeta PlusLevel #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> PlusLevel -> Bool #
InstantiateFull PlusLevel #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: PlusLevel -> ReduceM PlusLevel #
Normalise PlusLevel #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: PlusLevel -> ReduceM PlusLevel #
Simplify PlusLevel #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: PlusLevel -> ReduceM PlusLevel #
Reduce PlusLevel #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: PlusLevel -> ReduceM PlusLevel # reduceB' :: PlusLevel -> ReduceM (Blocked PlusLevel) #
Instantiate PlusLevel #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: PlusLevel -> ReduceM PlusLevel #
SynEq PlusLevel #
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: PlusLevel -> PlusLevel -> SynEqM (PlusLevel, PlusLevel) synEq' :: PlusLevel -> PlusLevel -> SynEqM (PlusLevel, PlusLevel)
HasPolarity PlusLevel #
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> PlusLevel -> TCM [Polarity] #
UsableRelevance PlusLevel #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> PlusLevel -> TCM Bool #
ComputeOccurrences PlusLevel #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: PlusLevel -> OccM OccurrencesBuilder #
FoldRigid PlusLevel #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> PlusLevel -> TCM m #
Occurs PlusLevel #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> PlusLevel -> TCM PlusLevel # metaOccurs :: MetaId -> PlusLevel -> TCM () #
AbsTerm PlusLevel #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> PlusLevel -> PlusLevel #
Subst Term PlusLevel #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> PlusLevel -> PlusLevel #

newtype Level #

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

The empty maximum is the canonical representation for level 0.

Constructors

Max [PlusLevel]

Instances

Eq Level #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Level -> Level -> Bool # (/=) :: Level -> Level -> Bool #
Data Level #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Level -> c Level # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Level # toConstr :: Level -> Constr # dataTypeOf :: Level -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Level) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Level) # gmapT :: (forall b. Data b => b -> b) -> Level -> Level # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Level -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Level -> r # gmapQ :: (forall d. Data d => d -> u) -> Level -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Level -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Level -> m Level # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Level -> m Level # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Level -> m Level #
Ord Level #
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Level -> Level -> Ordering # (<) :: Level -> Level -> Bool # (<=) :: Level -> Level -> Bool # (>) :: Level -> Level -> Bool # (>=) :: Level -> Level -> Bool # max :: Level -> Level -> Level # min :: Level -> Level -> Level #
Show Level #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Level -> ShowS # show :: Level -> String # showList :: [Level] -> ShowS #
NFData Level #
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Level -> () #
Pretty Level #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Level -> Doc # prettyPrec :: Int -> Level -> Doc # prettyList :: [Level] -> Doc #
KillRange Level #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Level #
TermSize Level #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Level -> Int # tsize :: Level -> Sum Int #
DeBruijn Level #
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> Level # debruijnNamedVar :: String -> Int -> Level # deBruijnView :: Level -> Maybe Int #
PrecomputeFreeVars Level #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Level -> FV Level #
Free Level #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Level -> FreeM c #
TermLike Level #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Level -> m Level # foldTerm :: Monoid m => (Term -> m) -> Level -> m #
GetDefs Level #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Level -> m () #
Free Level #
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: Level -> FreeT
EmbPrj Level #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Level -> S Int32 # icod_ :: Level -> S Int32 # value :: Int32 -> R Level #
PrettyTCM Level #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Level -> TCM Doc #
NamesIn Level #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Level -> Set QName #
UnFreezeMeta Level #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: Level -> TCM () #
IsInstantiatedMeta Level #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: Level -> TCM Bool #
MentionsMeta Level #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Level -> Bool #
InstantiateFull Level #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Level -> ReduceM Level #
Normalise Level #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Level -> ReduceM Level #
Simplify Level #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Level -> ReduceM Level #
Reduce Level #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Level -> ReduceM Level # reduceB' :: Level -> ReduceM (Blocked Level) #
Instantiate Level #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Level -> ReduceM Level #
SynEq Level #
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Level -> Level -> SynEqM (Level, Level) synEq' :: Level -> Level -> SynEqM (Level, Level)
Match Level #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods match :: Level -> Level -> MaybeT TCM [WithOrigin Term] #
HasPolarity Level #
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Level -> TCM [Polarity] #
UsableRelevance Level #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Level -> TCM Bool #
ComputeOccurrences Level #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Level -> OccM OccurrencesBuilder #
FoldRigid Level #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Level -> TCM m #
Occurs Level #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Level -> TCM Level # metaOccurs :: MetaId -> Level -> TCM () #
AbsTerm Level #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Level -> Level #
Subst Term Level #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Level -> Level #
Reify Level Expr #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Level -> TCM Expr # reifyWhen :: Bool -> Level -> TCM Expr #
Match NLPat Level #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> NLPat -> Level -> NLM () #

data Sort #

Sorts.

Constructors

Type Level	`Set ℓ`.
Prop	Dummy sort.
Inf	`Setω`.
SizeUniv	`SizeUniv`, a sort inhabited by type `Size`.
PiSort Sort (Abs Sort)	Sort of the pi type.
UnivSort Sort	Sort of another sort.
MetaS !MetaId Elims

Instances

Eq Sort #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Sort -> Sort -> Bool # (/=) :: Sort -> Sort -> Bool #
Data Sort #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sort -> c Sort # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sort # toConstr :: Sort -> Constr # dataTypeOf :: Sort -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Sort) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sort) # gmapT :: (forall b. Data b => b -> b) -> Sort -> Sort # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r # gmapQ :: (forall d. Data d => d -> u) -> Sort -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Sort -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sort -> m Sort # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sort -> m Sort # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sort -> m Sort #
Ord Sort #
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Sort -> Sort -> Ordering # (<) :: Sort -> Sort -> Bool # (<=) :: Sort -> Sort -> Bool # (>) :: Sort -> Sort -> Bool # (>=) :: Sort -> Sort -> Bool # max :: Sort -> Sort -> Sort # min :: Sort -> Sort -> Sort #
Show Sort #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Sort -> ShowS # show :: Sort -> String # showList :: [Sort] -> ShowS #
NFData Sort #
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Sort -> () #
Pretty Sort #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Sort -> Doc # prettyPrec :: Int -> Sort -> Doc # prettyList :: [Sort] -> Doc #
KillRange Sort #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Sort #
TermSize Sort #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Sort -> Int # tsize :: Sort -> Sum Int #
PrecomputeFreeVars Sort #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Sort -> FV Sort #
Free Sort #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Sort -> FreeM c #
Abstract Sort #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Sort -> Sort #
Apply Sort #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Sort -> Args -> Sort # applyE :: Sort -> Elims -> Sort #
GetDefs Sort #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Sort -> m () #
Free Sort #
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: Sort -> FreeT
EmbPrj Sort #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Sort -> S Int32 # icod_ :: Sort -> S Int32 # value :: Int32 -> R Sort #
PrettyTCM Sort #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Sort -> TCM Doc #
NamesIn Sort #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Sort -> Set QName #
UnFreezeMeta Sort #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: Sort -> TCM () #
MentionsMeta Sort #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Sort -> Bool #
InstantiateFull Sort #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Sort -> ReduceM Sort #
Normalise Sort #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Sort -> ReduceM Sort #
Simplify Sort #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Sort -> ReduceM Sort #
Reduce Sort #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Sort -> ReduceM Sort # reduceB' :: Sort -> ReduceM (Blocked Sort) #
Instantiate Sort #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Sort -> ReduceM Sort #
SynEq Sort #
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Sort -> Sort -> SynEqM (Sort, Sort) synEq' :: Sort -> Sort -> SynEqM (Sort, Sort)
Match Sort #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods match :: Sort -> Sort -> MaybeT TCM [WithOrigin Term] #
UsableRelevance Sort #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Sort -> TCM Bool #
FoldRigid Sort #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Sort -> TCM m #
Occurs Sort #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Sort -> TCM Sort # metaOccurs :: MetaId -> Sort -> TCM () #
AbsTerm Sort #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Sort -> Sort #
Subst Term Sort #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Sort -> Sort #
Reify Sort Expr #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Sort -> TCM Expr # reifyWhen :: Bool -> Sort -> TCM Expr #
Match NLPat Sort #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> NLPat -> Sort -> NLM () #
PatternFrom Sort NLPat #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> Sort -> TCM NLPat #

type Telescope = Tele (Dom Type) #

data Tele a #

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

Constructors

EmptyTel
ExtendTel a (Abs (Tele a))	`Abs` is never `NoAbs`.

Instances

Functor Tele #
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Tele a -> Tele b # (<$) :: a -> Tele b -> Tele a #
Foldable Tele #
Instance details Defined in Agda.Syntax.Internal Methods fold :: Monoid m => Tele m -> m # foldMap :: Monoid m => (a -> m) -> Tele a -> m # foldr :: (a -> b -> b) -> b -> Tele a -> b # foldr' :: (a -> b -> b) -> b -> Tele a -> b # foldl :: (b -> a -> b) -> b -> Tele a -> b # foldl' :: (b -> a -> b) -> b -> Tele a -> b # foldr1 :: (a -> a -> a) -> Tele a -> a # foldl1 :: (a -> a -> a) -> Tele a -> a # toList :: Tele a -> [a] # null :: Tele a -> Bool # length :: Tele a -> Int # elem :: Eq a => a -> Tele a -> Bool # maximum :: Ord a => Tele a -> a # minimum :: Ord a => Tele a -> a # sum :: Num a => Tele a -> a # product :: Num a => Tele a -> a #
Traversable Tele #
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 #
Instance details Defined in Agda.Syntax.Internal Methods telToArgs :: Telescope -> [Arg ArgName] #
Abstract Telescope #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Telescope -> Telescope #
TeleNoAbs Telescope #
Instance details Defined in Agda.TypeChecking.Substitute Methods teleNoAbs :: Telescope -> Term -> Term #
PrettyTCM Telescope #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Telescope -> TCM Doc #
DropArgs Telescope #	NOTE: This creates telescopes with unbound de Bruijn indices.
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> Telescope -> Telescope #
AddContext Telescope #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Telescope -> tcm a -> tcm a # contextSize :: Telescope -> Nat #
Reduce Telescope #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Telescope -> ReduceM Telescope # reduceB' :: Telescope -> ReduceM (Blocked Telescope) #
Instantiate Telescope #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Telescope -> ReduceM Telescope #
Reify Telescope Telescope #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Telescope0 -> TCM Telescope # reifyWhen :: Bool -> Telescope0 -> TCM Telescope #
Subst t a => Subst t (Tele a) #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Tele a -> Tele a #
(Subst t a, Eq a) => Eq (Tele a) #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Tele a -> Tele a -> Bool # (/=) :: Tele a -> Tele a -> Bool #
Data a => Data (Tele a) #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Tele a -> c (Tele a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Tele a) # toConstr :: Tele a -> Constr # dataTypeOf :: Tele a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Tele a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Tele a)) # gmapT :: (forall b. Data b => b -> b) -> Tele a -> Tele a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Tele a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Tele a -> r # gmapQ :: (forall d. Data d => d -> u) -> Tele a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Tele a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Tele a -> m (Tele a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Tele a -> m (Tele a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Tele a -> m (Tele a) #
(Subst t a, Ord a) => Ord (Tele a) #
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) #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Tele a -> ShowS # show :: Tele a -> String # showList :: [Tele a] -> ShowS #
Null (Tele a) #
Instance details Defined in Agda.Syntax.Internal Methods empty :: Tele a # null :: Tele a -> Bool #
Pretty a => Pretty (Tele (Dom a)) #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Tele (Dom a) -> Doc # prettyPrec :: Int -> Tele (Dom a) -> Doc # prettyList :: [Tele (Dom a)] -> Doc #
Sized (Tele a) #	The size of a telescope is its length (as a list).
Instance details Defined in Agda.Syntax.Internal Methods size :: Tele a -> Int #
KillRange a => KillRange (Tele a) #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Tele a) #
Free a => Free (Tele a) #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Tele a -> FreeM c #
Subst Term a => Apply (Tele a) #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Tele a -> Args -> Tele a # applyE :: Tele a -> Elims -> Tele a #
Free a => Free (Tele a) #
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: Tele a -> FreeT
EmbPrj a => EmbPrj (Tele a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Tele a -> S Int32 # icod_ :: Tele a -> S Int32 # value :: Int32 -> R (Tele a) #
NamesIn a => NamesIn (Tele a) #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Tele a -> Set QName #
AddContext (KeepNames Telescope) #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => KeepNames Telescope -> tcm a -> tcm a # contextSize :: KeepNames Telescope -> Nat #
MentionsMeta a => MentionsMeta (Tele a) #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Tele a -> Bool #
(Subst t a, InstantiateFull a) => InstantiateFull (Tele a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Tele a -> ReduceM (Tele a) #
(Subst t a, Normalise a) => Normalise (Tele a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Tele a -> ReduceM (Tele a) #
(Subst t a, Simplify a) => Simplify (Tele a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Tele a -> ReduceM (Tele a) #
ComputeOccurrences a => ComputeOccurrences (Tele a) #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Tele a -> OccM OccurrencesBuilder #

class LensSort a where #

Minimal complete definition

lensSort

Methods

lensSort :: Lens' Sort a #

getSort :: a -> Sort #

Instances

LensSort a => LensSort (Dom a) #
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' Sort (Dom a) # getSort :: Dom a -> Sort #
LensSort (Type' a) #
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' Sort (Type' a) # getSort :: Type' a -> Sort #
LensSort a => LensSort (Abs a) #
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' Sort (Abs a) # getSort :: Abs a -> Sort #

type Type = Type' Term #

data Type' a #

Types are terms with a sort annotation.

Constructors

El
Fields _getSort :: Sort unEl :: a

Instances

Functor Type' #
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Type' a -> Type' b # (<$) :: a -> Type' b -> Type' a #
Foldable Type' #
Instance details Defined in Agda.Syntax.Internal Methods fold :: Monoid m => Type' m -> m # foldMap :: Monoid m => (a -> m) -> Type' a -> m # foldr :: (a -> b -> b) -> b -> Type' a -> b # foldr' :: (a -> b -> b) -> b -> Type' a -> b # foldl :: (b -> a -> b) -> b -> Type' a -> b # foldl' :: (b -> a -> b) -> b -> Type' a -> b # foldr1 :: (a -> a -> a) -> Type' a -> a # foldl1 :: (a -> a -> a) -> Type' a -> a # toList :: Type' a -> [a] # null :: Type' a -> Bool # length :: Type' a -> Int # elem :: Eq a => a -> Type' a -> Bool # maximum :: Ord a => Type' a -> a # minimum :: Ord a => Type' a -> a # sum :: Num a => Type' a -> a # product :: Num a => Type' a -> a #
Traversable Type' #
Instance details Defined in Agda.Syntax.Internal Methods traverse :: Applicative f => (a -> f b) -> Type' a -> f (Type' b) # sequenceA :: Applicative f => Type' (f a) -> f (Type' a) # mapM :: Monad m => (a -> m b) -> Type' a -> m (Type' b) # sequence :: Monad m => Type' (m a) -> m (Type' a) #
NFData Type #
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Type -> () #
Decoration Type' #
Instance details Defined in Agda.Syntax.Internal Methods traverseF :: Functor m => (a -> m b) -> Type' a -> m (Type' b) # distributeF :: Functor m => Type' (m a) -> m (Type' a) #
Pretty Type #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Type -> Doc # prettyPrec :: Int -> Type -> Doc # prettyList :: [Type] -> Doc #
TelToArgs ListTel #
Instance details Defined in Agda.Syntax.Internal Methods telToArgs :: ListTel -> [Arg ArgName] #
TelToArgs Telescope #
Instance details Defined in Agda.Syntax.Internal Methods telToArgs :: Telescope -> [Arg ArgName] #
PrecomputeFreeVars Type #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Type -> FV Type #
Abstract Telescope #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Telescope -> Telescope #
Abstract Type #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Type -> Type #
TermLike Type #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Type -> m Type # foldTerm :: Monoid m => (Term -> m) -> Type -> m #
GetDefs Type #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Type -> m () #
Free Type #
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: Type -> FreeT
TeleNoAbs ListTel #
Instance details Defined in Agda.TypeChecking.Substitute Methods teleNoAbs :: ListTel -> Term -> Term #
TeleNoAbs Telescope #
Instance details Defined in Agda.TypeChecking.Substitute Methods teleNoAbs :: Telescope -> Term -> Term #
PrettyTCM Telescope #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Telescope -> TCM Doc #
PrettyTCM Type #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Type -> TCM Doc #
DropArgs Telescope #	NOTE: This creates telescopes with unbound de Bruijn indices.
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> Telescope -> Telescope #
AddContext Telescope #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Telescope -> tcm a -> tcm a # contextSize :: Telescope -> Nat #
UnFreezeMeta Type #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: Type -> TCM () #
MentionsMeta Type #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Type -> Bool #
Normalise Type #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Type -> ReduceM Type #
Simplify Type #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Type -> ReduceM Type #
Reduce Telescope #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Telescope -> ReduceM Telescope # reduceB' :: Telescope -> ReduceM (Blocked Telescope) #
Reduce Type #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Type -> ReduceM Type # reduceB' :: Type -> ReduceM (Blocked Type) #
Instantiate Telescope #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Telescope -> ReduceM Telescope #
Instantiate Type #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Type -> ReduceM Type #
SynEq Type #	Syntactic equality ignores sorts.
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Type -> Type -> SynEqM (Type, Type) synEq' :: Type -> Type -> SynEqM (Type, Type)
HasPolarity Type #
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Type -> TCM [Polarity] #
ComputeOccurrences Type #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Type -> OccM OccurrencesBuilder #
ToTerm Type #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Type -> Term) # toTermR :: TCM (Type -> ReduceM Term) #
PrimTerm Type #
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Type -> TCM Term #
FoldRigid Type #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Type -> TCM m #
Occurs Type #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Type -> TCM Type # metaOccurs :: MetaId -> Type -> TCM () #
AbsTerm Type #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Type -> Type #
Reify Telescope Telescope #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Telescope0 -> TCM Telescope # reifyWhen :: Bool -> Telescope0 -> TCM Telescope #
Reify Type Expr #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Type -> TCM Expr # reifyWhen :: Bool -> Type -> TCM Expr #
Match NLPType Type #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> NLPType -> Type -> NLM () #
PatternFrom Type NLPType #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> Type -> TCM NLPType #
Conversion TOM Type (MExp O) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Type -> TOM (MExp O) #
Subst Term a => Subst Term (Type' a) #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Type' a -> Type' a #
Conversion MOT (Exp O) Type #
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Type #
Eq a => Eq (Type' a) #	Syntactic `Type` equality, ignores sort annotations.
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Type' a -> Type' a -> Bool # (/=) :: Type' a -> Type' a -> Bool #
Data a => Data (Type' a) #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Type' a -> c (Type' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Type' a) # toConstr :: Type' a -> Constr # dataTypeOf :: Type' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Type' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Type' a)) # gmapT :: (forall b. Data b => b -> b) -> Type' a -> Type' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type' a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type' a -> r # gmapQ :: (forall d. Data d => d -> u) -> Type' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Type' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Type' a -> m (Type' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Type' a -> m (Type' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Type' a -> m (Type' a) #
Ord a => Ord (Type' a) #
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Type' a -> Type' a -> Ordering # (<) :: Type' a -> Type' a -> Bool # (<=) :: Type' a -> Type' a -> Bool # (>) :: Type' a -> Type' a -> Bool # (>=) :: Type' a -> Type' a -> Bool # max :: Type' a -> Type' a -> Type' a # min :: Type' a -> Type' a -> Type' a #
Show a => Show (Type' a) #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Type' a -> ShowS # show :: Type' a -> String # showList :: [Type' a] -> ShowS #
KillRange a => KillRange (Type' a) #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Type' a) #
SgTel (Dom (ArgName, Type)) #
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom (ArgName, Type) -> Telescope #
SgTel (Dom Type) #
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom Type -> Telescope #
LensSort (Type' a) #
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' Sort (Type' a) # getSort :: Type' a -> Sort #
Free a => Free (Type' a) #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Type' a -> FreeM c #
EmbPrj a => EmbPrj (Type' a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Type' a -> S Int32 # icod_ :: Type' a -> S Int32 # value :: Int32 -> R (Type' a) #
PrettyTCM (Type' NLPat) #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Type' NLPat -> TCM Doc #
NamesIn a => NamesIn (Type' a) #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Type' a -> Set QName #
IsSizeType a => IsSizeType (Type' a) #
Instance details Defined in Agda.TypeChecking.Monad.SizedTypes Methods isSizeType :: Type' a -> TCM (Maybe BoundedSize) #
AddContext (Dom (String, Type)) #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom (String, Type) -> tcm a -> tcm a # contextSize :: Dom (String, Type) -> Nat #
AddContext (Dom (Name, Type)) #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom (Name, Type) -> tcm a -> tcm a # contextSize :: Dom (Name, Type) -> Nat #
AddContext (Dom Type) #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom Type -> tcm a -> tcm a # contextSize :: Dom Type -> Nat #
AddContext (KeepNames Telescope) #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => KeepNames Telescope -> tcm a -> tcm a # contextSize :: KeepNames Telescope -> Nat #
InstantiateFull a => InstantiateFull (Type' a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Type' a -> ReduceM (Type' a) #
UsableRelevance a => UsableRelevance (Type' a) #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Type' a -> TCM Bool #
SgTel (ArgName, Dom Type) #
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: (ArgName, Dom Type) -> Telescope #
AddContext ([WithHiding Name], Dom Type) #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([WithHiding Name], Dom Type) -> tcm a -> tcm a # contextSize :: ([WithHiding Name], Dom Type) -> Nat #
AddContext ([Name], Dom Type) #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([Name], Dom Type) -> tcm a -> tcm a # contextSize :: ([Name], Dom Type) -> Nat #
AddContext (String, Dom Type) #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => (String, Dom Type) -> tcm a -> tcm a # contextSize :: (String, Dom Type) -> Nat #
AddContext (Name, Dom Type) #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => (Name, Dom Type) -> tcm a -> tcm a # contextSize :: (Name, Dom Type) -> Nat #
AddContext (KeepNames String, Dom Type) #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => (KeepNames String, Dom Type) -> tcm a -> tcm a # contextSize :: (KeepNames String, Dom Type) -> Nat #
UniverseBi ([Type], [Clause]) Pattern #
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: ([Type], [Clause]) -> [Pattern] #
UniverseBi ([Type], [Clause]) Term #
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: ([Type], [Clause]) -> [Term] #

data Abs a #

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

Constructors

Abs	The body has (at least) one free variable. Danger: `unAbs` doesn't shift variables properly
Fields absName :: ArgName unAbs :: a
NoAbs
Fields absName :: ArgName unAbs :: a

Instances

Functor Abs #
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Abs a -> Abs b # (<$) :: a -> Abs b -> Abs a #
Foldable Abs #
Instance details Defined in Agda.Syntax.Internal Methods fold :: Monoid m => Abs m -> m # foldMap :: Monoid m => (a -> m) -> Abs a -> m # foldr :: (a -> b -> b) -> b -> Abs a -> b # foldr' :: (a -> b -> b) -> b -> Abs a -> b # foldl :: (b -> a -> b) -> b -> Abs a -> b # foldl' :: (b -> a -> b) -> b -> Abs a -> b # foldr1 :: (a -> a -> a) -> Abs a -> a # foldl1 :: (a -> a -> a) -> Abs a -> a # toList :: Abs a -> [a] # null :: Abs a -> Bool # length :: Abs a -> Int # elem :: Eq a => a -> Abs a -> Bool # maximum :: Ord a => Abs a -> a # minimum :: Ord a => Abs a -> a # sum :: Num a => Abs a -> a # product :: Num a => Abs a -> a #
Traversable Abs #
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 #
Instance details Defined in Agda.Syntax.Internal Methods traverseF :: Functor m => (a -> m b) -> Abs a -> m (Abs b) # distributeF :: Functor m => Abs (m a) -> m (Abs a) #
Suggest String (Abs b) #
Instance details Defined in Agda.Syntax.Internal Methods suggest :: String -> Abs b -> String #
Suggest Name (Abs b) #
Instance details Defined in Agda.Syntax.Internal Methods suggest :: Name -> Abs b -> String #
Subst t a => Subst t (Abs a) #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Abs a -> Abs a #
Conversion MOT a b => Conversion MOT (Abs a) (Abs b) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Abs0 a -> MOT (Abs b) #
(Subst t a, Eq a) => Eq (Abs a) #	Equality of binders relies on weakening which is a special case of renaming which is a special case of substitution.
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Abs a -> Abs a -> Bool # (/=) :: Abs a -> Abs a -> Bool #
Data a => Data (Abs a) #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Abs a -> c (Abs a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Abs a) # toConstr :: Abs a -> Constr # dataTypeOf :: Abs a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Abs a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Abs a)) # gmapT :: (forall b. Data b => b -> b) -> Abs a -> Abs a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Abs a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Abs a -> r # gmapQ :: (forall d. Data d => d -> u) -> Abs a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Abs a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Abs a -> m (Abs a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Abs a -> m (Abs a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Abs a -> m (Abs a) #
(Subst t a, Ord a) => Ord (Abs a) #
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) #
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) #
Instance details Defined in Agda.Syntax.Internal Methods size :: Abs a -> Int #
KillRange a => KillRange (Abs a) #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Abs a) #
LensSort a => LensSort (Abs a) #
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' Sort (Abs a) # getSort :: Abs a -> Sort #
PrecomputeFreeVars a => PrecomputeFreeVars (Abs a) #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Abs a -> FV (Abs a) #
Free a => Free (Abs a) #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Abs a -> FreeM c #
TermLike a => TermLike (Abs a) #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Abs a -> m (Abs a) # foldTerm :: Monoid m => (Term -> m) -> Abs a -> m #
GetDefs a => GetDefs (Abs a) #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Abs a -> m () #
Free a => Free (Abs a) #
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: Abs a -> FreeT
EmbPrj a => EmbPrj (Abs a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Abs a -> S Int32 # icod_ :: Abs a -> S Int32 # value :: Int32 -> R (Abs a) #
NamesIn a => NamesIn (Abs a) #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Abs a -> Set QName #
UnFreezeMeta a => UnFreezeMeta (Abs a) #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: Abs a -> TCM () #
IsInstantiatedMeta a => IsInstantiatedMeta (Abs a) #	Does not worry about raising.
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: Abs a -> TCM Bool #
MentionsMeta t => MentionsMeta (Abs t) #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Abs t -> Bool #
(Subst t a, InstantiateFull a) => InstantiateFull (Abs a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Abs a -> ReduceM (Abs a) #
(Subst t a, Normalise a) => Normalise (Abs a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Abs a -> ReduceM (Abs a) #
(Subst t a, Simplify a) => Simplify (Abs a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Abs a -> ReduceM (Abs a) #
(Subst t a, Reduce a) => Reduce (Abs a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Abs a -> ReduceM (Abs a) # reduceB' :: Abs a -> ReduceM (Blocked (Abs a)) #
Instantiate t => Instantiate (Abs t) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Abs t -> ReduceM (Abs t) #
(Subst t a, SynEq a) => SynEq (Abs a) #
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)
HasPolarity a => HasPolarity (Abs a) #
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Abs a -> TCM [Polarity] #
(Subst t a, UsableRelevance a) => UsableRelevance (Abs a) #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Abs a -> TCM Bool #
ComputeOccurrences a => ComputeOccurrences (Abs a) #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Abs a -> OccM OccurrencesBuilder #
(Subst t a, FoldRigid a) => FoldRigid (Abs a) #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Abs a -> TCM m #
(Occurs a, Subst t a) => Occurs (Abs a) #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Abs a -> TCM (Abs a) # metaOccurs :: MetaId -> Abs a -> TCM () #
(Subst Term a, AbsTerm a) => AbsTerm (Abs a) #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Abs a -> Abs a #
Suggest (Abs a) (Abs b) #
Instance details Defined in Agda.Syntax.Internal Methods suggest :: Abs a -> Abs b -> String #
(Match a b, Subst t1 a, Subst t2 b) => Match (Abs a) (Abs b) #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> Abs a -> Abs b -> NLM () #
PatternFrom a b => PatternFrom (Abs a) (Abs b) #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> Abs a -> TCM (Abs b) #
(Free i, Reify i a) => Reify (Abs i) (Name, a) #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Abs i -> TCM (Name, a) # reifyWhen :: Bool -> Abs i -> TCM (Name, a) #

type ArgName = String #

Names in binders and arguments.

type Elims #

Arguments

= [Elim]

eliminations ordered left-to-right.

type Elim = Elim' Term #

data Elim' a #

Eliminations, subsuming applications and projections.

Constructors

Apply (Arg a)	Application.
Proj ProjOrigin QName	Projection. `QName` is name of a record projection.

Instances

Functor Elim' #
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Elim' a -> Elim' b # (<$) :: a -> Elim' b -> Elim' a #
Foldable Elim' #
Instance details Defined in Agda.Syntax.Internal Methods fold :: Monoid m => Elim' m -> m # foldMap :: Monoid m => (a -> m) -> Elim' a -> m # foldr :: (a -> b -> b) -> b -> Elim' a -> b # foldr' :: (a -> b -> b) -> b -> Elim' a -> b # foldl :: (b -> a -> b) -> b -> Elim' a -> b # foldl' :: (b -> a -> b) -> b -> Elim' a -> b # foldr1 :: (a -> a -> a) -> Elim' a -> a # foldl1 :: (a -> a -> a) -> Elim' a -> a # toList :: Elim' a -> [a] # null :: Elim' a -> Bool # length :: Elim' a -> Int # elem :: Eq a => a -> Elim' a -> Bool # maximum :: Ord a => Elim' a -> a # minimum :: Ord a => Elim' a -> a # sum :: Num a => Elim' a -> a # product :: Num a => Elim' a -> a #
Traversable Elim' #
Instance details Defined in Agda.Syntax.Internal Methods traverse :: Applicative f => (a -> f b) -> Elim' a -> f (Elim' b) # sequenceA :: Applicative f => Elim' (f a) -> f (Elim' a) # mapM :: Monad m => (a -> m b) -> Elim' a -> m (Elim' b) # sequence :: Monad m => Elim' (m a) -> m (Elim' a) #
IsProjElim Elim #
Instance details Defined in Agda.Syntax.Internal Methods isProjElim :: Elim -> Maybe (ProjOrigin, QName) #
PrettyTCM Elim #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Elim -> TCM Doc #
MentionsMeta Elim #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Elim -> Bool #
Normalise Elim #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Elim -> ReduceM Elim #
Simplify Elim #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Elim -> ReduceM Elim #
Reduce Elim #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Elim -> ReduceM Elim # reduceB' :: Elim -> ReduceM (Blocked Elim) #
Instantiate Elim #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Elim -> ReduceM Elim #
IsPrefixOf Elims #
Instance details Defined in Agda.TypeChecking.Abstract Methods isPrefixOf :: Elims -> Elims -> Maybe Elims #
UniverseBi Elims Pattern #
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: Elims -> [Pattern] #
UniverseBi Elims Term #
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: Elims -> [Term] #
Subst t a => Subst t (Elim' a) #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Elim' a -> Elim' a #
(Subst t a, Eq a) => Eq (Elim' a) #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Elim' a -> Elim' a -> Bool # (/=) :: Elim' a -> Elim' a -> Bool #
Data a => Data (Elim' a) #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Elim' a -> c (Elim' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Elim' a) # toConstr :: Elim' a -> Constr # dataTypeOf :: Elim' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Elim' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Elim' a)) # gmapT :: (forall b. Data b => b -> b) -> Elim' a -> Elim' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Elim' a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Elim' a -> r # gmapQ :: (forall d. Data d => d -> u) -> Elim' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Elim' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a) #
(Subst t a, Ord a) => Ord (Elim' a) #
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) #
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) #
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Elim' a -> () #
Pretty tm => Pretty (Elim' tm) #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Elim' tm -> Doc # prettyPrec :: Int -> Elim' tm -> Doc # prettyList :: [Elim' tm] -> Doc #
KillRange a => KillRange (Elim' a) #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Elim' a) #
LensOrigin (Elim' a) #	This instance cheats on `Proj`, use with care. `Proj`s are always assumed to be `UserWritten`, since they have no `ArgInfo`.
Instance details Defined in Agda.Syntax.Internal Methods getOrigin :: Elim' a -> Origin # setOrigin :: Origin -> Elim' a -> Elim' a # mapOrigin :: (Origin -> Origin) -> Elim' a -> Elim' a #
PrecomputeFreeVars a => PrecomputeFreeVars (Elim' a) #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Elim' a -> FV (Elim' a) #
Free a => Free (Elim' a) #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Elim' a -> FreeM c #
TermLike a => TermLike (Elim' a) #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Elim' a -> m (Elim' a) # foldTerm :: Monoid m => (Term -> m) -> Elim' a -> m #
GetDefs a => GetDefs (Elim' a) #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Elim' a -> m () #
Free a => Free (Elim' a) #
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: Elim' a -> FreeT
EmbPrj a => EmbPrj (Elim' a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Elim' a -> S Int32 # icod_ :: Elim' a -> S Int32 # value :: Int32 -> R (Elim' a) #
PrettyTCM (Elim' NLPat) #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Elim' NLPat -> TCM Doc #
PrettyTCM (Elim' DisplayTerm) #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Elim' DisplayTerm -> TCM Doc #
NamesIn a => NamesIn (Elim' a) #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Elim' a -> Set QName #
InstantiateFull a => InstantiateFull (Elim' a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Elim' a -> ReduceM (Elim' a) #
SynEq a => SynEq (Elim' a) #
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)
SubstWithOrigin (Arg a) => SubstWithOrigin (Elim' a) #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods substWithOrigin :: Substitution -> [WithOrigin Term] -> Elim' a -> Elim' a #
Match a => Match (Elim' a) #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods match :: Elim' a -> Elim' a -> MaybeT TCM [WithOrigin Term] #
HasPolarity a => HasPolarity (Elim' a) #
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Elim' a -> TCM [Polarity] #
UsableRelevance a => UsableRelevance (Elim' a) #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Elim' a -> TCM Bool #
ForcedVariables a => ForcedVariables (Elim' a) #
Instance details Defined in Agda.TypeChecking.Forcing Methods forcedVariables :: Elim' a -> [(Modality, Nat)] #
ComputeOccurrences a => ComputeOccurrences (Elim' a) #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Elim' a -> OccM OccurrencesBuilder #
FoldRigid a => FoldRigid (Elim' a) #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Elim' a -> TCM m #
Occurs a => Occurs (Elim' a) #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Elim' a -> TCM (Elim' a) # metaOccurs :: MetaId -> Elim' a -> TCM () #
AbsTerm a => AbsTerm (Elim' a) #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Elim' a -> Elim' a #
PatternVarModalities a x => PatternVarModalities (Elim' a) x #
Instance details Defined in Agda.Syntax.Internal.Pattern Methods patternVarModalities :: Elim' a -> [(x, Modality)] #
Reify i a => Reify (Elim' i) (Elim' a) #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Elim' i -> TCM (Elim' a) # reifyWhen :: Bool -> Elim' i -> TCM (Elim' a) #
Match a b => Match (Elim' a) (Elim' b) #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> Elim' a -> Elim' b -> NLM () #
PatternFrom a NLPat => PatternFrom (Elim' a) (Elim' NLPat) #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> Elim' a -> TCM (Elim' NLPat) #

type ConInfo = ConOrigin #

data Term #

Raw values.

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

Constructors

Var !Int Elims	`x es` neutral
Lam ArgInfo (Abs Term)	Terms are beta normal. Relevance is ignored
Lit Literal
Def QName Elims	`f es`, possibly a delta/iota-redex
Con ConHead ConInfo Elims	`c es` or `record { fs = es }` `es` allows only Apply and IApply eliminations, and IApply only for data constructors.
Pi (Dom Type) (Abs Type)	dependent or non-dependent function space
Sort Sort
Level Level
MetaV !MetaId Elims
DontCare Term	Irrelevant stuff in relevant position, but created in an irrelevant context. Basically, an internal version of the irrelevance axiom `.irrAx : .A -> A`.

Instances

Eq Term #	Syntactic `Term` equality, ignores stuff below `DontCare` and sharing.
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Term -> Term -> Bool # (/=) :: Term -> Term -> Bool #
Data Term #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Term -> c Term # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Term # toConstr :: Term -> Constr # dataTypeOf :: Term -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Term) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term) # gmapT :: (forall b. Data b => b -> b) -> Term -> Term # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r # gmapQ :: (forall d. Data d => d -> u) -> Term -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Term -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Term -> m Term # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term #
Ord Term #
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 #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Term -> ShowS # show :: Term -> String # showList :: [Term] -> ShowS #
NFData Type #
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Type -> () #
NFData Term #
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Term -> () #
Pretty Type #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Type -> Doc # prettyPrec :: Int -> Type -> Doc # prettyList :: [Type] -> Doc #
Pretty Term #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Term -> Doc # prettyPrec :: Int -> Term -> Doc # prettyList :: [Term] -> Doc #
Pretty CompiledClauses #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods pretty :: CompiledClauses -> Doc # prettyPrec :: Int -> CompiledClauses -> Doc # prettyList :: [CompiledClauses] -> Doc #
KillRange Substitution #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Substitution #
KillRange Term #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Term #
KillRange CompiledClauses #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods killRange :: KillRangeT CompiledClauses #
TermSize Term #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Term -> Int # tsize :: Term -> Sum Int #
IsProjElim Elim #
Instance details Defined in Agda.Syntax.Internal Methods isProjElim :: Elim -> Maybe (ProjOrigin, QName) #
TelToArgs ListTel #
Instance details Defined in Agda.Syntax.Internal Methods telToArgs :: ListTel -> [Arg ArgName] #
TelToArgs Telescope #
Instance details Defined in Agda.Syntax.Internal Methods telToArgs :: Telescope -> [Arg ArgName] #
DeBruijn Term #	We can substitute `Term`s for variables.
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> Term # debruijnNamedVar :: String -> Int -> Term # deBruijnView :: Term -> Maybe Int #
PrecomputeFreeVars Type #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Type -> FV Type #
PrecomputeFreeVars Term #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Term -> FV Term #
Free Term #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Term -> FreeM c #
Abstract Telescope #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Telescope -> Telescope #
Abstract Type #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Type -> Type #
Abstract Term #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Term -> Term #
Abstract CompiledClauses #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> CompiledClauses -> CompiledClauses #
Apply Term #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Term -> Args -> Term # applyE :: Term -> Elims -> Term #
Apply CompiledClauses #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: CompiledClauses -> Args -> CompiledClauses # applyE :: CompiledClauses -> Elims -> CompiledClauses #
TermLike Type #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Type -> m Type # foldTerm :: Monoid m => (Term -> m) -> Type -> m #
TermLike Term #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Term -> m Term # foldTerm :: Monoid m => (Term -> m) -> Term -> m #
GetDefs Type #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Type -> m () #
GetDefs Term #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Term -> m () #
Free Type #
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: Type -> FreeT
Free Term #
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: Term -> FreeT
TeleNoAbs ListTel #
Instance details Defined in Agda.TypeChecking.Substitute Methods teleNoAbs :: ListTel -> Term -> Term #
TeleNoAbs Telescope #
Instance details Defined in Agda.TypeChecking.Substitute Methods teleNoAbs :: Telescope -> Term -> Term #
EmbPrj Term #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Term -> S Int32 # icod_ :: Term -> S Int32 # value :: Int32 -> R Term #
EmbPrj CompiledClauses #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: CompiledClauses -> S Int32 # icod_ :: CompiledClauses -> S Int32 # value :: Int32 -> R CompiledClauses #
PrettyTCM Telescope #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Telescope -> TCM Doc #
PrettyTCM Type #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Type -> TCM Doc #
PrettyTCM Elim #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Elim -> TCM Doc #
PrettyTCM Term #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Term -> TCM Doc #
DropArgs Telescope #	NOTE: This creates telescopes with unbound de Bruijn indices.
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> Telescope -> Telescope #
DropArgs Term #	Use for dropping initial lambdas in clause bodies. NOTE: does not reduce term, need lambdas to be present.
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> Term -> Term #
DropArgs CompiledClauses #	To drop the first `n` arguments in a compiled clause, we reduce the split argument indices by `n` and drop `n` arguments from the bodies. NOTE: this only works for non-recursive functions, we are not dropping arguments to recursive calls in bodies.
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> CompiledClauses -> CompiledClauses #
NamesIn Term #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Term -> Set QName #
NamesIn CompiledClauses #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: CompiledClauses -> Set QName #
IsSizeType Term #
Instance details Defined in Agda.TypeChecking.Monad.SizedTypes Methods isSizeType :: Term -> TCM (Maybe BoundedSize) #
AddContext Telescope #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Telescope -> tcm a -> tcm a # contextSize :: Telescope -> Nat #
UnFreezeMeta Type #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: Type -> TCM () #
UnFreezeMeta Term #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: Term -> TCM () #
IsInstantiatedMeta Term #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: Term -> TCM Bool #
MentionsMeta Type #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Type -> Bool #
MentionsMeta Elim #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Elim -> Bool #
MentionsMeta Term #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Term -> Bool #
InstantiateFull Substitution #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Substitution -> ReduceM Substitution #
InstantiateFull Term #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Term -> ReduceM Term #
InstantiateFull CompiledClauses #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: CompiledClauses -> ReduceM CompiledClauses #
Normalise Type #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Type -> ReduceM Type #
Normalise Elim #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Elim -> ReduceM Elim #
Normalise Term #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Term -> ReduceM Term #
Simplify Type #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Type -> ReduceM Type #
Simplify Elim #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Elim -> ReduceM Elim #
Simplify Term #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Term -> ReduceM Term #
Reduce Telescope #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Telescope -> ReduceM Telescope # reduceB' :: Telescope -> ReduceM (Blocked Telescope) #
Reduce Type #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Type -> ReduceM Type # reduceB' :: Type -> ReduceM (Blocked Type) #
Reduce Elim #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Elim -> ReduceM Elim # reduceB' :: Elim -> ReduceM (Blocked Elim) #
Reduce Term #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Term -> ReduceM Term # reduceB' :: Term -> ReduceM (Blocked Term) #
Instantiate Telescope #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Telescope -> ReduceM Telescope #
Instantiate Type #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Type -> ReduceM Type #
Instantiate Elim #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Elim -> ReduceM Elim #
Instantiate Term #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Term -> ReduceM Term #
SynEq Type #	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 #	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)
SubstWithOrigin Term #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods substWithOrigin :: Substitution -> [WithOrigin Term] -> Term -> Term #
Match Term #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods match :: Term -> Term -> MaybeT TCM [WithOrigin Term] #
HasPolarity Type #
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Type -> TCM [Polarity] #
HasPolarity Term #
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Term -> TCM [Polarity] #
UsableRelevance Term #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Term -> TCM Bool #
ForcedVariables Term #	Assumes that the term is in normal form.
Instance details Defined in Agda.TypeChecking.Forcing Methods forcedVariables :: Term -> [(Modality, Nat)] #
ComputeOccurrences Type #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Type -> OccM OccurrencesBuilder #
ComputeOccurrences Term #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Term -> OccM OccurrencesBuilder #
ToTerm Type #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Type -> Term) # toTermR :: TCM (Type -> ReduceM Term) #
ToTerm Term #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Term -> Term) # toTermR :: TCM (Term -> ReduceM Term) #
PrimTerm Type #
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Type -> TCM Term #
FoldRigid Type #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Type -> TCM m #
FoldRigid Term #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Term -> TCM m #
Occurs Type #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Type -> TCM Type # metaOccurs :: MetaId -> Type -> TCM () #
Occurs Term #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Term -> TCM Term # metaOccurs :: MetaId -> Term -> TCM () #
ReduceAndEtaContract Term #
Instance details Defined in Agda.TypeChecking.MetaVars Methods reduceAndEtaContract :: Term -> TCM Term #
NoProjectedVar Term #
Instance details Defined in Agda.TypeChecking.MetaVars Methods noProjectedVar :: Term -> Either ProjVarExc () #
AbsTerm Type #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Type -> Type #
AbsTerm Term #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Term -> Term #
IsPrefixOf Elims #
Instance details Defined in Agda.TypeChecking.Abstract Methods isPrefixOf :: Elims -> Elims -> Maybe Elims #
IsPrefixOf Term #
Instance details Defined in Agda.TypeChecking.Abstract Methods isPrefixOf :: Term -> Term -> Maybe Elims #
IsPrefixOf Args #
Instance details Defined in Agda.TypeChecking.Abstract Methods isPrefixOf :: Args -> Args -> Maybe Elims #
UniverseBi Elims Pattern #
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: Elims -> [Pattern] #
UniverseBi Elims Term #
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: Elims -> [Term] #
UniverseBi Args Pattern #
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: Args -> [Pattern] #
UniverseBi Args Term #
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: Args -> [Term] #
Subst Term () #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> () -> () #
Subst Term String #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> String -> String #
Subst Term Range #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Range -> Range #
Subst Term QName #
Instance details Defined in Agda.TypeChecking.Substitute.Class Methods applySubst :: Substitution' Term -> QName -> QName #
Subst Term Name #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Name -> Name #
Subst Term EqualityView #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> EqualityView -> EqualityView #
Subst Term ConPatternInfo #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> ConPatternInfo -> ConPatternInfo #
Subst Term Pattern #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Pattern -> Pattern #
Subst Term LevelAtom #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> LevelAtom -> LevelAtom #
Subst Term PlusLevel #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> PlusLevel -> PlusLevel #
Subst Term Level #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Level -> Level #
Subst Term Sort #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Sort -> Sort #
Subst Term Term #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Term -> Term #
Subst Term ProblemEq #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> ProblemEq -> ProblemEq #
Subst Term Candidate #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Candidate -> Candidate #
Subst Term DisplayTerm #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> DisplayTerm -> DisplayTerm #
Subst Term DisplayForm #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> DisplayForm -> DisplayForm #
Subst Term Constraint #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Constraint -> Constraint #
Subst Term AbsurdPattern #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods applySubst :: Substitution' Term -> AbsurdPattern -> AbsurdPattern #
Subst Term DotPattern #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods applySubst :: Substitution' Term -> DotPattern -> DotPattern #
Subst Term AsBinding #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods applySubst :: Substitution' Term -> AsBinding -> AsBinding #
Subst Term SizeConstraint #
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods applySubst :: Substitution' Term -> SizeConstraint -> SizeConstraint #
Subst Term SizeMeta #
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods applySubst :: Substitution' Term -> SizeMeta -> SizeMeta #
Reify Telescope Telescope #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Telescope0 -> TCM Telescope # reifyWhen :: Bool -> Telescope0 -> TCM Telescope #
Reify Type Expr #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Type -> TCM Expr # reifyWhen :: Bool -> Type -> TCM Expr #
Reify Term Expr #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Term -> TCM Expr # reifyWhen :: Bool -> Term -> TCM Expr #
Match NLPType Type #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> NLPType -> Type -> NLM () #
Match NLPat Term #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> NLPat -> Term -> NLM () #
PatternFrom Type NLPType #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> Type -> TCM NLPType #
PatternFrom Term NLPat #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> Term -> TCM NLPat #
Conversion TOM Type (MExp O) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Type -> TOM (MExp O) #
Conversion TOM Term (MExp O) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Term -> TOM (MExp O) #
Conversion TOM Args (MM (ArgList O) (RefInfo O)) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) #
Subst Term a => Subst Term (Type' a) #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Type' a -> Type' a #
Subst Term (Problem a) #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods applySubst :: Substitution' Term -> Problem a -> Problem a #
DeBruijn (Pattern' a) => TermToPattern Term (Pattern' a) #
Instance details Defined in Agda.TypeChecking.Patterns.Internal Methods termToPattern :: Term -> TCM (Pattern' a) #
Conversion MOT (Exp O) Type #
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Type #
Conversion MOT (Exp O) Term #
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Term #
Subst Term (SizeExpr' NamedRigid SizeMeta) #	Only for `raise`.
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods applySubst :: Substitution' Term -> SizeExpr' NamedRigid SizeMeta -> SizeExpr' NamedRigid SizeMeta #
Eq (Substitution' Term) #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Substitution' Term -> Substitution' Term -> Bool # (/=) :: Substitution' Term -> Substitution' Term -> Bool #
Ord (Substitution' Term) #
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Substitution' Term -> Substitution' Term -> Ordering # (<) :: Substitution' Term -> Substitution' Term -> Bool # (<=) :: Substitution' Term -> Substitution' Term -> Bool # (>) :: Substitution' Term -> Substitution' Term -> Bool # (>=) :: Substitution' Term -> Substitution' Term -> Bool # max :: Substitution' Term -> Substitution' Term -> Substitution' Term # min :: Substitution' Term -> Substitution' Term -> Substitution' Term #
SgTel (Dom (ArgName, Type)) #
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom (ArgName, Type) -> Telescope #
SgTel (Dom Type) #
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom Type -> Telescope #
AddContext (Dom (String, Type)) #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom (String, Type) -> tcm a -> tcm a # contextSize :: Dom (String, Type) -> Nat #
AddContext (Dom (Name, Type)) #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom (Name, Type) -> tcm a -> tcm a # contextSize :: Dom (Name, Type) -> Nat #
AddContext (Dom Type) #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom Type -> tcm a -> tcm a # contextSize :: Dom Type -> Nat #
AddContext (KeepNames Telescope) #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => KeepNames Telescope -> tcm a -> tcm a # contextSize :: KeepNames Telescope -> Nat #
SubstWithOrigin (Arg Term) #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods substWithOrigin :: Substitution -> [WithOrigin Term] -> Arg Term -> Arg Term #
UniverseBi [Term] Term #
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: [Term] -> [Term] #
SgTel (ArgName, Dom Type) #
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: (ArgName, Dom Type) -> Telescope #
AddContext ([WithHiding Name], Dom Type) #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([WithHiding Name], Dom Type) -> tcm a -> tcm a # contextSize :: ([WithHiding Name], Dom Type) -> Nat #
AddContext ([Name], Dom Type) #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([Name], Dom Type) -> tcm a -> tcm a # contextSize :: ([Name], Dom Type) -> Nat #
AddContext (String, Dom Type) #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => (String, Dom Type) -> tcm a -> tcm a # contextSize :: (String, Dom Type) -> Nat #
AddContext (Name, Dom Type) #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => (Name, Dom Type) -> tcm a -> tcm a # contextSize :: (Name, Dom Type) -> Nat #
AddContext (KeepNames String, Dom Type) #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => (KeepNames String, Dom Type) -> tcm a -> tcm a # contextSize :: (KeepNames String, Dom Type) -> Nat #
UniverseBi ([Type], [Clause]) Pattern #
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: ([Type], [Clause]) -> [Pattern] #
UniverseBi ([Type], [Clause]) Term #
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: ([Type], [Clause]) -> [Term] #

class LensConName a where #

Minimal complete definition

getConName

Methods

getConName :: a -> QName #

setConName :: QName -> a -> a #

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

Instances

LensConName ConHead #
Instance details Defined in Agda.Syntax.Internal Methods getConName :: ConHead -> QName # setConName :: QName -> ConHead -> ConHead # mapConName :: (QName -> QName) -> ConHead -> ConHead #

data ConHead #

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

Constructors

ConHead
Fields conName :: QName The name of the constructor. conInductive :: Induction Record constructors can be coinductive. conFields :: [QName] The name of the record fields. Empty list for data constructors. `Arg` is not needed here since it is stored in the constructor args.

Instances

Eq ConHead #
Instance details Defined in Agda.Syntax.Internal Methods (==) :: ConHead -> ConHead -> Bool # (/=) :: ConHead -> ConHead -> Bool #
Data ConHead #
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 :: (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 #
Instance details Defined in Agda.Syntax.Internal Methods compare :: ConHead -> ConHead -> Ordering # (<) :: ConHead -> ConHead -> Bool # (<=) :: ConHead -> ConHead -> Bool # (>) :: ConHead -> ConHead -> Bool # (>=) :: ConHead -> ConHead -> Bool # max :: ConHead -> ConHead -> ConHead # min :: ConHead -> ConHead -> ConHead #
Show ConHead #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> ConHead -> ShowS # show :: ConHead -> String # showList :: [ConHead] -> ShowS #
Pretty ConHead #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: ConHead -> Doc # prettyPrec :: Int -> ConHead -> Doc # prettyList :: [ConHead] -> Doc #
KillRange ConHead #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT ConHead #
SetRange ConHead #
Instance details Defined in Agda.Syntax.Internal Methods setRange :: Range -> ConHead -> ConHead #
HasRange ConHead #
Instance details Defined in Agda.Syntax.Internal Methods getRange :: ConHead -> Range #
LensConName ConHead #
Instance details Defined in Agda.Syntax.Internal Methods getConName :: ConHead -> QName # setConName :: QName -> ConHead -> ConHead # mapConName :: (QName -> QName) -> ConHead -> ConHead #
EmbPrj ConHead #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ConHead -> S Int32 # icod_ :: ConHead -> S Int32 # value :: Int32 -> R ConHead #
PrettyTCM ConHead #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: ConHead -> TCM Doc #
NamesIn ConHead #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: ConHead -> Set QName #
InstantiateFull ConHead #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ConHead -> ReduceM ConHead #

type NamedArgs = [NamedArg Term] #

type Args = [Arg Term] #

Type of argument lists.

argNameToString :: ArgName -> String #

stringToArgName :: String -> ArgName #

appendArgNames :: ArgName -> ArgName -> ArgName #

nameToArgName :: Name -> ArgName #

stuckOn :: Elim -> NotBlocked -> NotBlocked #

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

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

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

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

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

clausePats :: Clause -> [Arg DeBruijnPattern] #

patVarNameToString :: PatVarName -> String #

nameToPatVarName :: Name -> PatVarName #

varP :: a -> Pattern' a #

dotP :: Term -> Pattern' a #

namedVarP :: PatVarName -> Named_ Pattern #

namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern #

noConPatternInfo :: ConPatternInfo #

toConPatternInfo :: ConInfo -> ConPatternInfo #

Build partial ConPatternInfo from ConInfo

fromConPatternInfo :: ConPatternInfo -> ConInfo #

Build ConInfo from ConPatternInfo.

patternOrigin :: Pattern' x -> Maybe PatOrigin #

Retrieve the origin of a pattern

properlyMatching :: DeBruijnPattern -> Bool #

Does the pattern perform a match that could fail?

isEqualityType :: EqualityView -> Bool #

absurdBody :: Abs Term #

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

isAbsurdBody :: Abs Term -> Bool #

absurdPatternName :: PatVarName #

isAbsurdPatternName :: PatVarName -> Bool #

var :: Nat -> Term #

An unapplied variable.

dontCare :: Term -> Term #

Add DontCare is it is not already a DontCare.

typeDontCare :: Type #

A dummy type.

topSort :: Type #

Top sort (Setomega).

sort :: Sort -> Type #

varSort :: Int -> Sort #

levelSuc :: Level -> Level #

mkType :: Integer -> Sort #

isSort :: Term -> Maybe Sort #

impossibleTerm :: String -> Int -> Term #

hackReifyToMeta :: Term #

isHackReifyToMeta :: Term -> Bool #

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

A traversal for the names in a telescope.

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

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

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

telFromList :: ListTel -> Telescope #

Convert a list telescope to a telescope.

telToList :: Telescope -> ListTel #

Convert a telescope to its list form.

blockingMeta :: Blocked t -> Maybe MetaId #

blocked :: MetaId -> a -> Blocked a #

notBlocked :: a -> Blocked a #

stripDontCare :: Term -> Term #

Removing a topmost DontCare constructor.

arity :: Type -> Nat #

Doesn't do any reduction.

notInScopeName :: ArgName -> ArgName #

Make a name that is not in scope.

unNotInScopeName :: ArgName -> ArgName #

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

unSpine :: Term -> Term #

Convert top-level postfix projections into prefix projections.

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

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

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

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

argFromElim :: Elim' a -> Arg a #

Drop Apply constructor. (Unsafe!)

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

Drop Apply constructor. (Safe)

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

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

Drop Apply constructors. (Safe)

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

Split at first non-Apply

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

Discard Proj f entries.

argsFromElims :: Elims -> Args #

Discards Proj f entries.

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

Drop Proj constructors. (Safe)

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

module Agda.Syntax.Abstract.Name

newtype MetaId #

A meta variable identifier is just a natural number.

Constructors

MetaId
Fields metaId :: Nat

Instances

Enum MetaId #
Instance details Defined in Agda.Syntax.Common Methods succ :: MetaId -> MetaId # pred :: MetaId -> MetaId # toEnum :: Int -> MetaId # fromEnum :: MetaId -> Int # enumFrom :: MetaId -> [MetaId] # enumFromThen :: MetaId -> MetaId -> [MetaId] # enumFromTo :: MetaId -> MetaId -> [MetaId] # enumFromThenTo :: MetaId -> MetaId -> MetaId -> [MetaId] #
Eq MetaId #
Instance details Defined in Agda.Syntax.Common Methods (==) :: MetaId -> MetaId -> Bool # (/=) :: MetaId -> MetaId -> Bool #
Integral MetaId #
Instance details Defined in Agda.Syntax.Common Methods quot :: MetaId -> MetaId -> MetaId # rem :: MetaId -> MetaId -> MetaId # div :: MetaId -> MetaId -> MetaId # mod :: MetaId -> MetaId -> MetaId # quotRem :: MetaId -> MetaId -> (MetaId, MetaId) # divMod :: MetaId -> MetaId -> (MetaId, MetaId) # toInteger :: MetaId -> Integer #
Data MetaId #
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 :: (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 #
Instance details Defined in Agda.Syntax.Common Methods (+) :: MetaId -> MetaId -> MetaId # (-) :: MetaId -> MetaId -> MetaId # (*) :: MetaId -> MetaId -> MetaId # negate :: MetaId -> MetaId # abs :: MetaId -> MetaId # signum :: MetaId -> MetaId # fromInteger :: Integer -> MetaId #
Ord MetaId #
Instance details Defined in Agda.Syntax.Common Methods compare :: MetaId -> MetaId -> Ordering # (<) :: MetaId -> MetaId -> Bool # (<=) :: MetaId -> MetaId -> Bool # (>) :: MetaId -> MetaId -> Bool # (>=) :: MetaId -> MetaId -> Bool # max :: MetaId -> MetaId -> MetaId # min :: MetaId -> MetaId -> MetaId #
Real MetaId #
Instance details Defined in Agda.Syntax.Common Methods toRational :: MetaId -> Rational #
Show MetaId #	Show non-record version of this newtype.
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> MetaId -> ShowS # show :: MetaId -> String # showList :: [MetaId] -> ShowS #
NFData MetaId #
Instance details Defined in Agda.Syntax.Common Methods rnf :: MetaId -> () #
Pretty MetaId #
Instance details Defined in Agda.Syntax.Common Methods pretty :: MetaId -> Doc # prettyPrec :: Int -> MetaId -> Doc # prettyList :: [MetaId] -> Doc #
GetDefs MetaId #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => MetaId -> m () #
HasFresh MetaId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' MetaId TCState # nextFresh' :: MetaId -> MetaId #
EmbPrj MetaId #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: MetaId -> S Int32 # icod_ :: MetaId -> S Int32 # value :: Int32 -> R MetaId #
PrettyTCM MetaId #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MetaId -> TCM Doc #
UnFreezeMeta MetaId #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MetaId -> TCM () #
IsInstantiatedMeta MetaId #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: MetaId -> TCM Bool #
FromTerm MetaId #
Instance details Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction MetaId) #
ToTerm MetaId #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (MetaId -> Term) # toTermR :: TCM (MetaId -> ReduceM Term) #
PrimTerm MetaId #
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: MetaId -> TCM Term #
Unquote MetaId #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM MetaId #
Reify MetaId Expr #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MetaId -> TCM Expr # reifyWhen :: Bool -> MetaId -> TCM Expr #