Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Internal

Synopsis

class TermSize a where
- termSize :: a -> Int
- tsize :: a -> Sum Int
class IsProjElim e where
- isProjElim :: e -> Maybe (ProjOrigin, QName)
data Suggestion = forall a.Suggest a => Suggestion a
class Suggest a where
- suggestName :: a -> Maybe String
class SgTel a where
- sgTel :: a -> Telescope
class TelToArgs a where
- telToArgs :: a -> [Arg ArgName]
type ListTel = ListTel' ArgName
type ListTel' a = [Dom (a, Type)]
data IntervalView
- = IZero
- | IOne
- | IMin (Arg Term) (Arg Term)
- | IMax (Arg Term) (Arg Term)
- | INeg (Arg Term)
- | OTerm Term
data PathView
- = PathType {
  - pathSort :: Sort
  - pathName :: QName
  - pathLevel :: Arg Term
  - pathType :: Arg Term
  - pathLhs :: Arg Term
  - pathRhs :: Arg Term
  }
- | OType 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
- patternVars :: b -> [Arg (Either a Term)]
data ConPatternInfo = ConPatternInfo {
- conPInfo :: PatternInfo
- conPRecord :: Bool
- conPFallThrough :: Bool
- 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 PatternInfo x
- | DotP PatternInfo Term
- | ConP ConHead ConPatternInfo [NamedArg (Pattern' x)]
- | LitP PatternInfo Literal
- | ProjP ProjOrigin QName
- | IApplyP PatternInfo Term Term x
- | DefP PatternInfo QName [NamedArg (Pattern' x)]
data PatOrigin
- = PatOSystem
- | PatOSplit
- | PatOVar Name
- | PatODot
- | PatOWild
- | PatOCon
- | PatORec
- | PatOLit
- | PatOAbsurd
data PatternInfo = PatternInfo {
- patOrigin :: PatOrigin
- patAsNames :: [Name]
}
type PatVarName = ArgName
data Clause = Clause {
- clauseLHSRange :: Range
- clauseFullRange :: Range
- clauseTel :: Telescope
- namedClausePats :: NAPs
- clauseBody :: Maybe Term
- clauseType :: Maybe (Arg Type)
- clauseCatchall :: Bool
- clauseRecursive :: Maybe Bool
- clauseUnreachable :: Maybe Bool
- clauseEllipsis :: ExpandedEllipsis
}
type NAPs = [NamedArg DeBruijnPattern]
type Blocked_ = Blocked ()
data Blocked t
- = Blocked {
  - theBlockingMeta :: MetaId
  - ignoreBlocking :: t
  }
- | NotBlocked {
  - blockingStatus :: NotBlocked
  - ignoreBlocking :: t
  }
data NotBlocked
- = StuckOn Elim
- | Underapplied
- | AbsurdMatch
- | MissingClauses
- | ReallyNotBlocked
newtype BraveTerm = BraveTerm {
- unBrave :: Term
}
type LevelAtom = LevelAtom' Term
data LevelAtom' t
- = MetaLevel MetaId [Elim' t]
- | BlockedLevel MetaId t
- | NeutralLevel NotBlocked t
- | UnreducedLevel t
type PlusLevel = PlusLevel' Term
data PlusLevel' t = Plus Integer (LevelAtom' t)
type Level = Level' Term
data Level' t = Max Integer [PlusLevel' t]
type Sort = Sort' Term
data Sort' t
- = Type (Level' t)
- | Prop (Level' t)
- | Inf
- | SizeUniv
- | PiSort (Dom' t (Type'' t t)) (Abs (Sort' t))
- | FunSort (Sort' t) (Sort' t)
- | UnivSort (Sort' t)
- | MetaS !MetaId [Elim' t]
- | DefS QName [Elim' t]
- | DummyS String
type Telescope = Tele (Dom Type)
data Tele a
- = EmptyTel
- | ExtendTel a (Abs (Tele a))
class LensSort a where
- lensSort :: Lens' Sort a
- getSort :: a -> Sort
type Type = Type' Term
type Type' a = Type'' Term a
data Type'' t a = El {
- _getSort :: Sort' t
- unEl :: a
}
data Abs a
- = Abs {
  - absName :: ArgName
  - unAbs :: a
  }
- | NoAbs {
  - absName :: ArgName
  - unAbs :: a
  }
type Elims = [Elim]
type Elim = Elim' Term
data Elim' a
- = Apply (Arg a)
- | Proj ProjOrigin QName
- | IApply a a a
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
- | Dummy String Elims
class LensConName a where
- getConName :: a -> QName
- setConName :: QName -> a -> a
- mapConName :: (QName -> QName) -> a -> a
data ConHead = ConHead {
- conName :: QName
- conInductive :: Induction
- conFields :: [Arg QName]
}
type NamedArgs = [NamedArg Term]
type Args = [Arg Term]
type Dom = Dom' Term
data Dom' t e = Dom {
- domInfo :: ArgInfo
- domFinite :: !Bool
- domName :: Maybe NamedName
- domTactic :: Maybe t
- unDom :: e
}
pattern ClosedLevel :: Integer -> Level
argFromDom :: Dom' t a -> Arg a
namedArgFromDom :: Dom' t a -> NamedArg a
domFromArg :: Arg a -> Dom a
domFromNamedArg :: NamedArg a -> Dom a
defaultDom :: a -> Dom a
defaultArgDom :: ArgInfo -> a -> Dom a
defaultNamedArgDom :: ArgInfo -> String -> a -> Dom a
stuckOn :: Elim -> NotBlocked -> NotBlocked
clausePats :: Clause -> [Arg DeBruijnPattern]
patVarNameToString :: PatVarName -> String
nameToPatVarName :: Name -> PatVarName
defaultPatternInfo :: PatternInfo
varP :: a -> Pattern' a
dotP :: Term -> Pattern' a
litP :: Literal -> Pattern' a
namedVarP :: PatVarName -> Named_ Pattern
namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern
absurdP :: Int -> DeBruijnPattern
noConPatternInfo :: ConPatternInfo
toConPatternInfo :: ConInfo -> ConPatternInfo
fromConPatternInfo :: ConPatternInfo -> ConInfo
patternInfo :: Pattern' x -> Maybe PatternInfo
patternOrigin :: Pattern' x -> Maybe PatOrigin
properlyMatching :: Pattern' a -> Bool
properlyMatching' :: Bool -> Bool -> Pattern' a -> Bool
isEqualityType :: EqualityView -> Bool
isPathType :: PathView -> Bool
isIOne :: IntervalView -> Bool
absurdBody :: Abs Term
isAbsurdBody :: Abs Term -> Bool
absurdPatternName :: PatVarName
isAbsurdPatternName :: PatVarName -> Bool
var :: Nat -> Term
dontCare :: Term -> Term
dummyTerm' :: String -> Int -> Term
dummyLevel' :: String -> Int -> Level
dummyTerm :: String -> Int -> Term
__DUMMY_TERM__ :: HasCallStack => Term
dummyLevel :: String -> Int -> Level
__DUMMY_LEVEL__ :: HasCallStack => Level
dummySort :: String -> Int -> Sort
__DUMMY_SORT__ :: HasCallStack => Sort
dummyType :: String -> Int -> Type
__DUMMY_TYPE__ :: HasCallStack => Type
dummyDom :: String -> Int -> Dom Type
__DUMMY_DOM__ :: HasCallStack => Dom Type
atomicLevel :: LevelAtom -> Level
unreducedLevel :: Term -> Level
topSort :: Type
sort :: Sort -> Type
varSort :: Int -> Sort
tmSort :: Term -> Sort
levelPlus :: Integer -> Level -> Level
levelSuc :: Level -> Level
mkType :: Integer -> Sort
mkProp :: Integer -> Sort
isSort :: Term -> Maybe Sort
impossibleTerm :: String -> Int -> Term
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 :: Tele (Dom t) -> [Dom (ArgName, t)]
listTel :: Lens' ListTel Telescope
blockingMeta :: Blocked t -> Maybe MetaId
blocked :: MetaId -> a -> Blocked a
notBlocked :: a -> Blocked a
blocked_ :: MetaId -> Blocked_
notBlocked_ :: Blocked_
stripDontCare :: Term -> Term
arity :: Type -> Nat
suggests :: [Suggestion] -> String
unSpine :: Term -> Term
unSpine' :: (ProjOrigin -> Bool) -> Term -> Term
hasElims :: Term -> Maybe (Elims -> Term, Elims)
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])
argsFromElims :: Elims -> Args
allProjElims :: Elims -> Maybe [(ProjOrigin, QName)]
pDom :: LensHiding a => a -> Doc -> Doc
prettyPrecLevelSucs :: Int -> Integer -> (Int -> Doc) -> Doc
module Agda.Syntax.Abstract.Name
newtype MetaId = MetaId {
- metaId :: Nat
}

Documentation

class TermSize a where Source #

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

Not counting towards the term size are:

sort and color annotations,
projections.

Minimal complete definition

tsize

Methods

termSize :: a -> Int Source #

tsize :: a -> Sum Int Source #

Instances

Instances details

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

class IsProjElim e where Source #

Methods

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

Instances

Instances details

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

data Suggestion Source #

Constructors

forall a.Suggest a => Suggestion a

class Suggest a where Source #

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

Methods

suggestName :: a -> Maybe String Source #

Instances

Instances details

Suggest String Source #
Instance details Defined in Agda.Syntax.Internal Methods suggestName :: String -> Maybe String Source #
Suggest Name Source #
Instance details Defined in Agda.Syntax.Internal Methods suggestName :: Name -> Maybe String Source #
Suggest Term Source #
Instance details Defined in Agda.Syntax.Internal Methods suggestName :: Term -> Maybe String Source #
Suggest (Abs b) Source #
Instance details Defined in Agda.Syntax.Internal Methods suggestName :: Abs b -> Maybe String Source #

class SgTel a where Source #

Constructing a singleton telescope.

Methods

sgTel :: a -> Telescope Source #

Instances

Instances details

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

class TelToArgs a where Source #

Drop the types from a telescope.

Methods

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

Instances

Instances details

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

type ListTel = ListTel' ArgName Source #

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

Telescope as list.

data IntervalView Source #

Constructors

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

Instances

Instances details

Show IntervalView Source #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> IntervalView -> ShowS # show :: IntervalView -> String # showList :: [IntervalView] -> ShowS #

data PathView Source #

View type as path type.

Constructors

PathType
Fields pathSort :: Sort Sort of this type. pathName :: QName Builtin PATH. pathLevel :: Arg Term Hidden pathType :: Arg Term Hidden pathLhs :: Arg Term NotHidden pathRhs :: Arg Term NotHidden
OType Type	reduced

data EqualityView Source #

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

Instances details

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

type PatternSubstitution = Substitution' DeBruijnPattern Source #

type Substitution = Substitution' Term Source #

data Substitution' a Source #

Substitutions.

Constructors

IdS	Identity substitution. `Γ ⊢ IdS : Γ`
EmptyS Empty	Empty substitution, lifts from the empty context. First argument is `IMPOSSIBLE`. Apply this to closed terms you want to use in a non-empty context. `Γ ⊢ EmptyS : ()`
a :# (Substitution' a) infixr 4	Substitution extension, ``cons'`. `Γ ⊢ u : Aρ Γ ⊢ ρ : Δ ---------------------- Γ ⊢ u :# ρ : Δ, A`
Strengthen Empty (Substitution' a)	Strengthening substitution. First argument is `IMPOSSIBLE`. Apply this to a term which does not contain variable 0 to lower all de Bruijn indices by one. `Γ ⊢ ρ : Δ --------------------------- Γ ⊢ Strengthen ρ : Δ, A`
Wk !Int (Substitution' a)	Weakening substitution, lifts to an extended context. `Γ ⊢ ρ : Δ ------------------- Γ, Ψ ⊢ Wk \|Ψ\| ρ : Δ`
Lift !Int (Substitution' a)	Lifting substitution. Use this to go under a binder. `Lift 1 ρ == var 0 :# Wk 1 ρ`. `Γ ⊢ ρ : Δ ------------------------- Γ, Ψρ ⊢ Lift \|Ψ\| ρ : Δ, Ψ`

Instances

Instances details

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

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

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

Methods

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

Instances

Instances details

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

data ConPatternInfo Source #

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

Constructors

ConPatternInfo

Fields

conPInfo :: PatternInfo
Information on the origin of the pattern.
conPRecord :: Bool
False if data constructor. True if record constructor.
conPFallThrough :: Bool
Should the match block on non-canonical terms or can it proceed to the catch-all clause?
conPType :: Maybe (Arg Type)
The type of the whole constructor pattern. Should be present (Just) if constructor pattern is is generated ordinarily by type-checking. Could be absent (Nothing) if pattern comes from some plugin (like Agsy). Needed e.g. for with-clause stripping.
conPLazy :: Bool
Lazy patterns are generated by the forcing translation in the unifier (unifyStep) and are dropped by the clause compiler (TODO: not yet) (compileClauses) when the variables they bind are unused. The GHC backend compiles lazy matches to lazy patterns in Haskell (TODO: not yet).

Instances

Instances details

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

type DeBruijnPattern = Pattern' DBPatVar Source #

data DBPatVar Source #

Type used when numbering pattern variables.

Constructors

DBPatVar
Fields dbPatVarName :: PatVarName dbPatVarIndex :: Int

Instances

Instances details

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

type Pattern Source #

Arguments

= Pattern' PatVarName

The PatVarName is a name suggestion.

data Pattern' x Source #

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

Constructors

VarP PatternInfo x	x
DotP PatternInfo Term	.t
ConP ConHead ConPatternInfo [NamedArg (Pattern' x)]	`c ps` The subpatterns do not contain any projection copatterns.
LitP PatternInfo Literal	E.g. `5`, `"hello"`.
ProjP ProjOrigin QName	Projection copattern. Can only appear by itself.
IApplyP PatternInfo Term Term x	Path elimination pattern, like `VarP` but keeps track of endpoints.
DefP PatternInfo QName [NamedArg (Pattern' x)]	Used for HITs, the QName should be the one from primHComp.

Instances

Instances details

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

data PatOrigin Source #

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

Constructors

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

Instances

Instances details

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

data PatternInfo Source #

Constructors

PatternInfo
Fields patOrigin :: PatOrigin patAsNames :: [Name]

Instances

Instances details

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

type PatVarName = ArgName Source #

Pattern variables.

data Clause Source #

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

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

clauseTel ~ permute clausePerm (patternVars namedClausePats)

Terms in dot patterns are valid in the clause telescope.

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

Constructors

Clause

Fields

clauseLHSRange :: Range
clauseFullRange :: Range
clauseTel :: Telescope
Δ: The types of the pattern variables in dependency order.
namedClausePats :: NAPs
Δ ⊢ ps. The de Bruijn indices refer to Δ.
clauseBody :: Maybe Term
Just v with Δ ⊢ v for a regular clause, or Nothing for an absurd one.
clauseType :: Maybe (Arg Type)
Δ ⊢ t. The type of the rhs under clauseTel. Used, e.g., by TermCheck. Can be Irrelevant if we encountered an irrelevant projection pattern on the lhs.
clauseCatchall :: Bool
Clause has been labelled as CATCHALL.
clauseRecursive :: Maybe Bool
clauseBody contains recursive calls; computed by termination checker. Nothing means that termination checker has not run yet, or that clauseBody contains meta-variables; these could be filled with recursive calls later! Just False means definitely no recursive call. Just True means definitely a recursive call.
clauseUnreachable :: Maybe Bool
Clause has been labelled as unreachable by the coverage checker. Nothing means coverage checker has not run yet (clause may be unreachable). Just False means clause is not unreachable. Just True means clause is unreachable.
clauseEllipsis :: ExpandedEllipsis
Was this clause created by expansion of an ellipsis?

Instances

Instances details

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

type NAPs = [NamedArg DeBruijnPattern] Source #

Named pattern arguments.

type Blocked_ = Blocked () Source #

Blocked t without the t.

data Blocked t Source #

Something where a meta variable may block reduction.

Constructors

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

Instances

Instances details

Functor Blocked Source #
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Blocked a -> Blocked b # (<$) :: a -> Blocked b -> Blocked a #
Applicative Blocked Source #	Blocking by a meta is dominant.
Instance details Defined in Agda.Syntax.Internal Methods pure :: a -> Blocked a # (<>) :: Blocked (a -> b) -> Blocked a -> Blocked b # liftA2 :: (a -> b -> c) -> Blocked a -> Blocked b -> Blocked c # (>) :: Blocked a -> Blocked b -> Blocked b # (<*) :: Blocked a -> Blocked b -> Blocked a #
Foldable Blocked Source #
Instance details Defined in Agda.Syntax.Internal Methods fold :: Monoid m => Blocked m -> m # foldMap :: Monoid m => (a -> m) -> Blocked a -> m # foldMap' :: Monoid m => (a -> m) -> Blocked a -> m # foldr :: (a -> b -> b) -> b -> Blocked a -> b # foldr' :: (a -> b -> b) -> b -> Blocked a -> b # foldl :: (b -> a -> b) -> b -> Blocked a -> b # foldl' :: (b -> a -> b) -> b -> Blocked a -> b # foldr1 :: (a -> a -> a) -> Blocked a -> a # foldl1 :: (a -> a -> a) -> Blocked a -> a # toList :: Blocked a -> [a] # null :: Blocked a -> Bool # length :: Blocked a -> Int # elem :: Eq a => a -> Blocked a -> Bool # maximum :: Ord a => Blocked a -> a # minimum :: Ord a => Blocked a -> a # sum :: Num a => Blocked a -> a # product :: Num a => Blocked a -> a #
Traversable Blocked Source #
Instance details Defined in Agda.Syntax.Internal Methods traverse :: Applicative f => (a -> f b) -> Blocked a -> f (Blocked b) # sequenceA :: Applicative f => Blocked (f a) -> f (Blocked a) # mapM :: Monad m => (a -> m b) -> Blocked a -> m (Blocked b) # sequence :: Monad m => Blocked (m a) -> m (Blocked a) #
Semigroup Blocked_ Source #
Instance details Defined in Agda.Syntax.Internal Methods (<>) :: Blocked_ -> Blocked_ -> Blocked_ # sconcat :: NonEmpty Blocked_ -> Blocked_ # stimes :: Integral b => b -> Blocked_ -> Blocked_ #
Monoid Blocked_ Source #
Instance details Defined in Agda.Syntax.Internal Methods mempty :: Blocked_ # mappend :: Blocked_ -> Blocked_ -> Blocked_ # mconcat :: [Blocked_] -> Blocked_ #
EmbPrj Blocked_ Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Blocked_ -> S Int32 Source # icod_ :: Blocked_ -> S Int32 Source # value :: Int32 -> R Blocked_ Source #
Subst t a => Subst t (Blocked a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Blocked a -> Blocked a Source #
Eq t => Eq (Blocked t) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Blocked t -> Blocked t -> Bool # (/=) :: Blocked t -> Blocked t -> Bool #
Data t => Data (Blocked t) Source #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Blocked t -> c (Blocked t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Blocked t) # toConstr :: Blocked t -> Constr # dataTypeOf :: Blocked t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (Blocked t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (Blocked t)) # gmapT :: (forall b. Data b => b -> b) -> Blocked t -> Blocked t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Blocked t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Blocked t -> r # gmapQ :: (forall d. Data d => d -> u) -> Blocked t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Blocked t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Blocked t -> m (Blocked t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Blocked t -> m (Blocked t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Blocked t -> m (Blocked t) #
Show t => Show (Blocked t) Source #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Blocked t -> ShowS # show :: Blocked t -> String # showList :: [Blocked t] -> ShowS #
KillRange a => KillRange (Blocked a) Source #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Blocked a) Source #
Apply t => Apply (Blocked t) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Blocked t -> Args -> Blocked t Source # applyE :: Blocked t -> Elims -> Blocked t Source #
TermLike a => TermLike (Blocked a) Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Blocked a -> m (Blocked a) Source # foldTerm :: Monoid m => (Term -> m) -> Blocked a -> m Source #
PrettyTCM a => PrettyTCM (Blocked a) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Blocked a -> m Doc Source #
Instantiate a => Instantiate (Blocked a) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Blocked a -> ReduceM (Blocked a) Source #

data NotBlocked Source #

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

Constructors

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

Instances

Instances details

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

newtype BraveTerm Source #

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

Constructors

BraveTerm
Fields unBrave :: Term

Instances

Instances details

Data BraveTerm Source #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BraveTerm -> c BraveTerm # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BraveTerm # toConstr :: BraveTerm -> Constr # dataTypeOf :: BraveTerm -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BraveTerm) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BraveTerm) # gmapT :: (forall b. Data b => b -> b) -> BraveTerm -> BraveTerm # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BraveTerm -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BraveTerm -> r # gmapQ :: (forall d. Data d => d -> u) -> BraveTerm -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> BraveTerm -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> BraveTerm -> m BraveTerm # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BraveTerm -> m BraveTerm # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BraveTerm -> m BraveTerm #
Show BraveTerm Source #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> BraveTerm -> ShowS # show :: BraveTerm -> String # showList :: [BraveTerm] -> ShowS #
DeBruijn BraveTerm Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods deBruijnVar :: Int -> BraveTerm Source # debruijnNamedVar :: String -> Int -> BraveTerm Source # deBruijnView :: BraveTerm -> Maybe Int Source #
Apply BraveTerm Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: BraveTerm -> Args -> BraveTerm Source # applyE :: BraveTerm -> Elims -> BraveTerm Source #
Subst BraveTerm BraveTerm Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' BraveTerm -> BraveTerm -> BraveTerm Source #

type LevelAtom = LevelAtom' Term Source #

data LevelAtom' t Source #

An atomic term of type Level.

Constructors

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

Instances

Instances details

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

type PlusLevel = PlusLevel' Term Source #

data PlusLevel' t Source #

Constructors

Plus Integer (LevelAtom' t)

n + ℓ.

Instances

Instances details

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

type Level = Level' Term Source #

data Level' t Source #

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

Constructors

Max Integer [PlusLevel' t]

Instances

Instances details

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

type Sort = Sort' Term Source #

data Sort' t Source #

Sorts.

Constructors

Type (Level' t)	`Set ℓ`.
Prop (Level' t)	`Prop ℓ`.
Inf	`Setω`.
SizeUniv	`SizeUniv`, a sort inhabited by type `Size`.
PiSort (Dom' t (Type'' t t)) (Abs (Sort' t))	Sort of the pi type.
FunSort (Sort' t) (Sort' t)	Sort of a (non-dependent) function type.
UnivSort (Sort' t)	Sort of another sort.
MetaS !MetaId [Elim' t]
DefS QName [Elim' t]	A postulated sort.
DummyS String	A (part of a) term or type which is only used for internal purposes. Replaces the abuse of `Prop` for a dummy sort. The `String` typically describes the location where we create this dummy, but can contain other information as well.

Instances

Instances details

Eq Sort Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Sort -> Sort -> Bool # (/=) :: Sort -> Sort -> Bool #
Ord Sort Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Sort -> Sort -> Ordering # (<) :: Sort -> Sort -> Bool # (<=) :: Sort -> Sort -> Bool # (>) :: Sort -> Sort -> Bool # (>=) :: Sort -> Sort -> Bool # max :: Sort -> Sort -> Sort # min :: Sort -> Sort -> Sort #
NFData Sort Source #
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Sort -> () #
Pretty Sort Source #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Sort -> Doc Source # prettyPrec :: Int -> Sort -> Doc Source # prettyList :: [Sort] -> Doc Source #
KillRange Sort Source #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Sort Source #
TermSize Sort Source #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Sort -> Int Source # tsize :: Sort -> Sum Int Source #
PrecomputeFreeVars Sort Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Sort -> FV Sort Source #
Free Sort Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Sort -> FreeM a c Source #
Abstract Sort Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Sort -> Sort Source #
Apply Sort Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Sort -> Args -> Sort Source # applyE :: Sort -> Elims -> Sort Source #
TermLike Sort Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Sort -> m Sort Source # foldTerm :: Monoid m => (Term -> m) -> Sort -> m Source #
GetDefs Sort Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Sort -> m () Source #
EmbPrj Sort Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Sort -> S Int32 Source # icod_ :: Sort -> S Int32 Source # value :: Int32 -> R Sort Source #
PrettyTCM Sort Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Sort -> m Doc Source #
NamesIn Sort Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Sort -> Set QName Source #
UnFreezeMeta Sort Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Sort -> m () Source #
MentionsMeta Sort Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Sort -> Bool Source #
InstantiateFull Sort Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Sort -> ReduceM Sort Source #
Normalise Sort Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Sort -> ReduceM Sort Source #
Simplify Sort Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Sort -> ReduceM Sort Source #
Reduce Sort Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Sort -> ReduceM Sort Source # reduceB' :: Sort -> ReduceM (Blocked Sort) Source #
IsMeta Sort Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods isMeta :: HasBuiltins m => Sort -> m (Maybe MetaId) Source #
Instantiate Sort Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Sort -> ReduceM Sort Source #
SynEq Sort Source #
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Sort -> Sort -> SynEqM (Sort, Sort) synEq' :: Sort -> Sort -> SynEqM (Sort, Sort)
ForceNotFree Sort Source #
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Sort -> m Sort
Match Sort Source #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods match :: forall (m :: Type -> Type). MonadDisplayForm m => Sort -> Sort -> MaybeT m [WithOrigin Term] Source #
UsableModality Sort Source #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Sort -> TCM Bool Source #
UsableRelevance Sort Source #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Sort -> TCM Bool Source #
AnyRigid Sort Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat -> tcm Bool) -> Sort -> tcm Bool Source #
Occurs Sort Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Sort -> OccursM Sort Source # metaOccurs :: MetaId -> Sort -> TCM () Source #
EqualSy Sort Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Sort -> Sort -> Bool Source #
AbsTerm Sort Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Sort -> Sort Source #
Reify Sort Expr Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MonadReify m => Sort -> m Expr Source # reifyWhen :: MonadReify m => Bool -> Sort -> m Expr Source #
NLPatToTerm NLPSort Sort Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: (MonadReduce m, HasBuiltins m, HasConstInfo m, MonadDebug m) => NLPSort -> m Sort Source #
PatternFrom () Sort NLPSort Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> () -> Sort -> TCM NLPSort Source #
Match () NLPSort Sort Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> () -> NLPSort -> Sort -> NLM () Source #
(Coercible a Term, Subst t a) => Subst t (Sort' a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Sort' a -> Sort' a Source #
Data t => Data (Sort' t) Source #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sort' t -> c (Sort' t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Sort' t) # toConstr :: Sort' t -> Constr # dataTypeOf :: Sort' t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (Sort' t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (Sort' t)) # gmapT :: (forall b. Data b => b -> b) -> Sort' t -> Sort' t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sort' t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sort' t -> r # gmapQ :: (forall d. Data d => d -> u) -> Sort' t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Sort' t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sort' t -> m (Sort' t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sort' t -> m (Sort' t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sort' t -> m (Sort' t) #
Show t => Show (Sort' t) Source #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Sort' t -> ShowS # show :: Sort' t -> String # showList :: [Sort' t] -> ShowS #

type Telescope = Tele (Dom Type) Source #

data Tele a Source #

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

Constructors

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

Instances

Instances details

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

class LensSort a where Source #

Minimal complete definition

lensSort

Methods

lensSort :: Lens' Sort a Source #

getSort :: a -> Sort Source #

Instances

Instances details

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

type Type = Type' Term Source #

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

data Type'' t a Source #

Types are terms with a sort annotation.

Constructors

El
Fields _getSort :: Sort' t unEl :: a

Instances

Instances details

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

data Abs a Source #

Binder.

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

Constructors

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

Instances

Instances details

Functor Abs Source #
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Abs a -> Abs b # (<$) :: a -> Abs b -> Abs a #
Foldable Abs Source #
Instance details Defined in Agda.Syntax.Internal Methods fold :: Monoid m => Abs m -> m # foldMap :: Monoid m => (a -> m) -> Abs a -> m # foldMap' :: Monoid m => (a -> m) -> Abs a -> m # foldr :: (a -> b -> b) -> b -> Abs a -> b # foldr' :: (a -> b -> b) -> b -> Abs a -> b # foldl :: (b -> a -> b) -> b -> Abs a -> b # foldl' :: (b -> a -> b) -> b -> Abs a -> b # foldr1 :: (a -> a -> a) -> Abs a -> a # foldl1 :: (a -> a -> a) -> Abs a -> a # toList :: Abs a -> [a] # null :: Abs a -> Bool # length :: Abs a -> Int # elem :: Eq a => a -> Abs a -> Bool # maximum :: Ord a => Abs a -> a # minimum :: Ord a => Abs a -> a # sum :: Num a => Abs a -> a # product :: Num a => Abs a -> a #
Traversable Abs Source #
Instance details Defined in Agda.Syntax.Internal Methods traverse :: Applicative f => (a -> f b) -> Abs a -> f (Abs b) # sequenceA :: Applicative f => Abs (f a) -> f (Abs a) # mapM :: Monad m => (a -> m b) -> Abs a -> m (Abs b) # sequence :: Monad m => Abs (m a) -> m (Abs a) #
Decoration Abs Source #
Instance details Defined in Agda.Syntax.Internal Methods traverseF :: Functor m => (a -> m b) -> Abs a -> m (Abs b) Source # distributeF :: Functor m => Abs (m a) -> m (Abs a) Source #
Subst t a => Subst t (Abs a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Abs a -> Abs a Source #
Conversion MOT a b => Conversion MOT (Abs a) (Abs b) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Abs0 a -> MOT (Abs b) Source #
(Subst t a, Eq a) => Eq (Abs a) Source #	Equality of binders relies on weakening which is a special case of renaming which is a special case of substitution.
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Abs a -> Abs a -> Bool # (/=) :: Abs a -> Abs a -> Bool #
Data a => Data (Abs a) Source #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Abs a -> c (Abs a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Abs a) # toConstr :: Abs a -> Constr # dataTypeOf :: Abs a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Abs a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Abs a)) # gmapT :: (forall b. Data b => b -> b) -> Abs a -> Abs a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Abs a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Abs a -> r # gmapQ :: (forall d. Data d => d -> u) -> Abs a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Abs a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Abs a -> m (Abs a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Abs a -> m (Abs a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Abs a -> m (Abs a) #
(Subst t a, Ord a) => Ord (Abs a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Abs a -> Abs a -> Ordering # (<) :: Abs a -> Abs a -> Bool # (<=) :: Abs a -> Abs a -> Bool # (>) :: Abs a -> Abs a -> Bool # (>=) :: Abs a -> Abs a -> Bool # max :: Abs a -> Abs a -> Abs a # min :: Abs a -> Abs a -> Abs a #
Show a => Show (Abs a) Source #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Abs a -> ShowS # show :: Abs a -> String # showList :: [Abs a] -> ShowS #
Sized a => Sized (Abs a) Source #
Instance details Defined in Agda.Syntax.Internal Methods size :: Abs a -> Int Source #
KillRange a => KillRange (Abs a) Source #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Abs a) Source #
Suggest (Abs b) Source #
Instance details Defined in Agda.Syntax.Internal Methods suggestName :: Abs b -> Maybe String Source #
PrecomputeFreeVars a => PrecomputeFreeVars (Abs a) Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Abs a -> FV (Abs a) Source #
Free t => Free (Abs t) Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Abs t -> FreeM a c Source #
TermLike a => TermLike (Abs a) Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Abs a -> m (Abs a) Source # foldTerm :: Monoid m => (Term -> m) -> Abs a -> m Source #
GetDefs a => GetDefs (Abs a) Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Abs a -> m () Source #
EmbPrj a => EmbPrj (Abs a) Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Abs a -> S Int32 Source # icod_ :: Abs a -> S Int32 Source # value :: Int32 -> R (Abs a) Source #
NamesIn a => NamesIn (Abs a) Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Abs a -> Set QName Source #
UnFreezeMeta a => UnFreezeMeta (Abs a) Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Abs a -> m () Source #
IsInstantiatedMeta a => IsInstantiatedMeta (Abs a) Source #	Does not worry about raising.
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Abs a -> m Bool Source #
MentionsMeta t => MentionsMeta (Abs t) Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Abs t -> Bool Source #
(Subst t a, InstantiateFull a) => InstantiateFull (Abs a) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Abs a -> ReduceM (Abs a) Source #
(Subst t a, Normalise a) => Normalise (Abs a) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Abs a -> ReduceM (Abs a) Source #
(Subst t a, Simplify a) => Simplify (Abs a) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Abs a -> ReduceM (Abs a) Source #
(Subst t a, Reduce a) => Reduce (Abs a) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Abs a -> ReduceM (Abs a) Source # reduceB' :: Abs a -> ReduceM (Blocked (Abs a)) Source #
Instantiate t => Instantiate (Abs t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Abs t -> ReduceM (Abs t) Source #
(Subst t a, SynEq a) => SynEq (Abs a) Source #
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Abs a -> Abs a -> SynEqM (Abs a, Abs a) synEq' :: Abs a -> Abs a -> SynEqM (Abs a, Abs a)
(Reduce a, ForceNotFree a) => ForceNotFree (Abs a) Source #
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Abs a -> m (Abs a)
(Subst t a, UsableModality a) => UsableModality (Abs a) Source #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Abs a -> TCM Bool Source #
(Subst t a, UsableRelevance a) => UsableRelevance (Abs a) Source #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Abs a -> TCM Bool Source #
GetMatchables a => GetMatchables (Abs a) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: Abs a -> [QName] Source #
NLPatVars a => NLPatVars (Abs a) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatVarsUnder :: Int -> Abs a -> IntSet Source # nlPatVars :: Abs a -> IntSet Source #
ComputeOccurrences a => ComputeOccurrences (Abs a) Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Abs a -> OccM OccurrencesBuilder Source #
HasPolarity a => HasPolarity (Abs a) Source #
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Abs a -> TCM [Polarity] Source #
(Subst t a, AnyRigid a) => AnyRigid (Abs a) Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat -> tcm Bool) -> Abs a -> tcm Bool Source #
(Occurs a, Subst t a) => Occurs (Abs a) Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Abs a -> OccursM (Abs a) Source # metaOccurs :: MetaId -> Abs a -> TCM () Source #
(Subst t a, EqualSy a) => EqualSy (Abs a) Source #	Ignores `absName`.
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Abs a -> Abs a -> Bool Source #
(Subst Term a, AbsTerm a) => AbsTerm (Abs a) Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Abs a -> Abs a Source #
ToNLPat a b => ToNLPat (Abs a) (Abs b) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: Abs a -> Abs b Source #
NLPatToTerm p a => NLPatToTerm (Abs p) (Abs a) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: (MonadReduce m, HasBuiltins m, HasConstInfo m, MonadDebug m) => Abs p -> m (Abs a) Source #
(Free i, Reify i a) => Reify (Abs i) (Name, a) Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MonadReify m => Abs i -> m (Name, a) Source # reifyWhen :: MonadReify m => Bool -> Abs i -> m (Name, a) Source #

type Elims Source #

Arguments

= [Elim]

eliminations ordered left-to-right.

type Elim = Elim' Term Source #

data Elim' a Source #

Eliminations, subsuming applications and projections.

Constructors

Apply (Arg a)	Application.
Proj ProjOrigin QName	Projection. `QName` is name of a record projection.
IApply a a a	IApply x y r, x and y are the endpoints

Instances

Instances details

Functor Elim' Source #
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Elim' a -> Elim' b # (<$) :: a -> Elim' b -> Elim' a #
Foldable Elim' Source #
Instance details Defined in Agda.Syntax.Internal Methods fold :: Monoid m => Elim' m -> m # foldMap :: Monoid m => (a -> m) -> Elim' a -> m # foldMap' :: Monoid m => (a -> m) -> Elim' a -> m # foldr :: (a -> b -> b) -> b -> Elim' a -> b # foldr' :: (a -> b -> b) -> b -> Elim' a -> b # foldl :: (b -> a -> b) -> b -> Elim' a -> b # foldl' :: (b -> a -> b) -> b -> Elim' a -> b # foldr1 :: (a -> a -> a) -> Elim' a -> a # foldl1 :: (a -> a -> a) -> Elim' a -> a # toList :: Elim' a -> [a] # null :: Elim' a -> Bool # length :: Elim' a -> Int # elem :: Eq a => a -> Elim' a -> Bool # maximum :: Ord a => Elim' a -> a # minimum :: Ord a => Elim' a -> a # sum :: Num a => Elim' a -> a # product :: Num a => Elim' a -> a #
Traversable Elim' Source #
Instance details Defined in Agda.Syntax.Internal Methods traverse :: Applicative f => (a -> f b) -> Elim' a -> f (Elim' b) # sequenceA :: Applicative f => Elim' (f a) -> f (Elim' a) # mapM :: Monad m => (a -> m b) -> Elim' a -> m (Elim' b) # sequence :: Monad m => Elim' (m a) -> m (Elim' a) #
PrettyTCM Elim Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Elim -> m Doc Source #
MentionsMeta Elim Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Elim -> Bool Source #
Reduce Elim Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Elim -> ReduceM Elim Source # reduceB' :: Elim -> ReduceM (Blocked Elim) Source #
IsPrefixOf Elims Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods isPrefixOf :: Elims -> Elims -> Maybe Elims Source #
Subst t a => Subst t (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Elim' a -> Elim' a Source #
(Subst t a, Eq a) => Eq (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Elim' a -> Elim' a -> Bool # (/=) :: Elim' a -> Elim' a -> Bool #
Data a => Data (Elim' a) Source #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Elim' a -> c (Elim' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Elim' a) # toConstr :: Elim' a -> Constr # dataTypeOf :: Elim' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Elim' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Elim' a)) # gmapT :: (forall b. Data b => b -> b) -> Elim' a -> Elim' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Elim' a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Elim' a -> r # gmapQ :: (forall d. Data d => d -> u) -> Elim' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Elim' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a) #
(Subst t a, Ord a) => Ord (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Elim' a -> Elim' a -> Ordering # (<) :: Elim' a -> Elim' a -> Bool # (<=) :: Elim' a -> Elim' a -> Bool # (>) :: Elim' a -> Elim' a -> Bool # (>=) :: Elim' a -> Elim' a -> Bool # max :: Elim' a -> Elim' a -> Elim' a # min :: Elim' a -> Elim' a -> Elim' a #
Show a => Show (Elim' a) Source #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Elim' a -> ShowS # show :: Elim' a -> String # showList :: [Elim' a] -> ShowS #
NFData a => NFData (Elim' a) Source #
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Elim' a -> () #
Pretty tm => Pretty (Elim' tm) Source #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Elim' tm -> Doc Source # prettyPrec :: Int -> Elim' tm -> Doc Source # prettyList :: [Elim' tm] -> Doc Source #
KillRange a => KillRange (Elim' a) Source #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Elim' a) Source #
LensOrigin (Elim' a) Source #	This instance cheats on `Proj`, use with care. `Proj`s are always assumed to be `UserWritten`, since they have no `ArgInfo`. Same for IApply
Instance details Defined in Agda.Syntax.Internal Methods getOrigin :: Elim' a -> Origin Source # setOrigin :: Origin -> Elim' a -> Elim' a Source # mapOrigin :: (Origin -> Origin) -> Elim' a -> Elim' a Source #
IsProjElim (Elim' a) Source #
Instance details Defined in Agda.Syntax.Internal Methods isProjElim :: Elim' a -> Maybe (ProjOrigin, QName) Source #
PrecomputeFreeVars a => PrecomputeFreeVars (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Elim' a -> FV (Elim' a) Source #
Free t => Free (Elim' t) Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Elim' t -> FreeM a c Source #
TermLike a => TermLike (Elim' a) Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Elim' a -> m (Elim' a) Source # foldTerm :: Monoid m => (Term -> m) -> Elim' a -> m Source #
GetDefs a => GetDefs (Elim' a) Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Elim' a -> m () Source #
EmbPrj a => EmbPrj (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Elim' a -> S Int32 Source # icod_ :: Elim' a -> S Int32 Source # value :: Int32 -> R (Elim' a) Source #
PrettyTCM (Elim' NLPat) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Elim' NLPat -> m Doc Source #
PrettyTCM (Elim' DisplayTerm) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Elim' DisplayTerm -> m Doc Source #
NamesIn a => NamesIn (Elim' a) Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Elim' a -> Set QName Source #
InstantiateFull t => InstantiateFull (Elim' t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Elim' t -> ReduceM (Elim' t) Source #
Normalise t => Normalise (Elim' t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Elim' t -> ReduceM (Elim' t) Source #
Simplify t => Simplify (Elim' t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Elim' t -> ReduceM (Elim' t) Source #
Instantiate t => Instantiate (Elim' t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Elim' t -> ReduceM (Elim' t) Source #
SynEq a => SynEq (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Elim' a -> Elim' a -> SynEqM (Elim' a, Elim' a) synEq' :: Elim' a -> Elim' a -> SynEqM (Elim' a, Elim' a)
(Reduce a, ForceNotFree a) => ForceNotFree (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Elim' a -> m (Elim' a)
(SubstWithOrigin a, SubstWithOrigin (Arg a)) => SubstWithOrigin (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods substWithOrigin :: Substitution -> [WithOrigin Term] -> Elim' a -> Elim' a Source #
Match a => Match (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods match :: forall (m :: Type -> Type). MonadDisplayForm m => Elim' a -> Elim' a -> MaybeT m [WithOrigin Term] Source #
UsableModality a => UsableModality (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Elim' a -> TCM Bool Source #
UsableRelevance a => UsableRelevance (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Elim' a -> TCM Bool Source #
GetMatchables a => GetMatchables (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: Elim' a -> [QName] Source #
ComputeOccurrences a => ComputeOccurrences (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Elim' a -> OccM OccurrencesBuilder Source #
HasPolarity a => HasPolarity (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Elim' a -> TCM [Polarity] Source #
AnyRigid a => AnyRigid (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat -> tcm Bool) -> Elim' a -> tcm Bool Source #
Occurs a => Occurs (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Elim' a -> OccursM (Elim' a) Source # metaOccurs :: MetaId -> Elim' a -> TCM () Source #
EqualSy a => EqualSy (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Elim' a -> Elim' a -> Bool Source #
AbsTerm a => AbsTerm (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Elim' a -> Elim' a Source #
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: NamedArg DeBruijnPattern -> Elim' NLPat Source #
ToNLPat (Arg DeBruijnPattern) (Elim' NLPat) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: Arg DeBruijnPattern -> Elim' NLPat Source #
ToNLPat a b => ToNLPat (Elim' a) (Elim' b) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: Elim' a -> Elim' b Source #
Reify i a => Reify (Elim' i) (Elim' a) Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MonadReify m => Elim' i -> m (Elim' a) Source # reifyWhen :: MonadReify m => Bool -> Elim' i -> m (Elim' a) Source #
NLPatToTerm p a => NLPatToTerm (Elim' p) (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: (MonadReduce m, HasBuiltins m, HasConstInfo m, MonadDebug m) => Elim' p -> m (Elim' a) Source #
PatternFrom (Type, Term) Elims [Elim' NLPat] Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat] Source #
Match (Type, Term) [Elim' NLPat] Elims Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> (Type, Term) -> [Elim' NLPat] -> Elims -> NLM () Source #

type ConInfo = ConOrigin Source #

data Term Source #

Raw values.

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

Constructors

Var !Int Elims	`x es` neutral
Lam ArgInfo (Abs Term)	Terms are beta normal. Relevance is ignored
Lit Literal
Def QName Elims	`f es`, possibly a delta/iota-redex
Con ConHead ConInfo Elims	`c es` or `record { fs = es }` `es` allows only Apply and IApply eliminations, and IApply only for data constructors.
Pi (Dom Type) (Abs Type)	dependent or non-dependent function space
Sort Sort
Level Level
MetaV !MetaId Elims
DontCare Term	Irrelevant stuff in relevant position, but created in an irrelevant context. Basically, an internal version of the irrelevance axiom `.irrAx : .A -> A`.
Dummy String Elims	A (part of a) term or type which is only used for internal purposes. Replaces the `Sort Prop` hack. The `String` typically describes the location where we create this dummy, but can contain other information as well. The second field accumulates eliminations in case we apply a dummy term to more of them.

Instances

Instances details

Eq Substitution Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Substitution -> Substitution -> Bool # (/=) :: Substitution -> Substitution -> Bool #
Eq LevelAtom Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: LevelAtom -> LevelAtom -> Bool # (/=) :: LevelAtom -> LevelAtom -> Bool #
Eq PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: PlusLevel -> PlusLevel -> Bool # (/=) :: PlusLevel -> PlusLevel -> Bool #
Eq Level Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Level -> Level -> Bool # (/=) :: Level -> Level -> Bool #
Eq Sort Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Sort -> Sort -> Bool # (/=) :: Sort -> Sort -> Bool #
Eq Term Source #	Syntactic `Term` equality, ignores stuff below `DontCare` and sharing.
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Term -> Term -> Bool # (/=) :: Term -> Term -> Bool #
Data Term Source #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Term -> c Term # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Term # toConstr :: Term -> Constr # dataTypeOf :: Term -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Term) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term) # gmapT :: (forall b. Data b => b -> b) -> Term -> Term # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r # gmapQ :: (forall d. Data d => d -> u) -> Term -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Term -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Term -> m Term # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term #
Ord Substitution Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Substitution -> Substitution -> Ordering # (<) :: Substitution -> Substitution -> Bool # (<=) :: Substitution -> Substitution -> Bool # (>) :: Substitution -> Substitution -> Bool # (>=) :: Substitution -> Substitution -> Bool # max :: Substitution -> Substitution -> Substitution # min :: Substitution -> Substitution -> Substitution #
Ord LevelAtom Source #
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 #
Ord PlusLevel Source #
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 #
Ord Level Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Level -> Level -> Ordering # (<) :: Level -> Level -> Bool # (<=) :: Level -> Level -> Bool # (>) :: Level -> Level -> Bool # (>=) :: Level -> Level -> Bool # max :: Level -> Level -> Level # min :: Level -> Level -> Level #
Ord Sort Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Sort -> Sort -> Ordering # (<) :: Sort -> Sort -> Bool # (<=) :: Sort -> Sort -> Bool # (>) :: Sort -> Sort -> Bool # (>=) :: Sort -> Sort -> Bool # max :: Sort -> Sort -> Sort # min :: Sort -> Sort -> Sort #
Ord Term Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Term -> Term -> Ordering # (<) :: Term -> Term -> Bool # (<=) :: Term -> Term -> Bool # (>) :: Term -> Term -> Bool # (>=) :: Term -> Term -> Bool # max :: Term -> Term -> Term # min :: Term -> Term -> Term #
Show Term Source #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Term -> ShowS # show :: Term -> String # showList :: [Term] -> ShowS #
NFData LevelAtom Source #
Instance details Defined in Agda.Syntax.Internal Methods rnf :: LevelAtom -> () #
NFData PlusLevel Source #
Instance details Defined in Agda.Syntax.Internal Methods rnf :: PlusLevel -> () #
NFData Level Source #
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Level -> () #
NFData Sort Source #
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Sort -> () #
NFData Type Source #
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Type -> () #
NFData Term Source #
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Term -> () #
Pretty LevelAtom Source #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: LevelAtom -> Doc Source # prettyPrec :: Int -> LevelAtom -> Doc Source # prettyList :: [LevelAtom] -> Doc Source #
Pretty PlusLevel Source #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: PlusLevel -> Doc Source # prettyPrec :: Int -> PlusLevel -> Doc Source # prettyList :: [PlusLevel] -> Doc Source #
Pretty Level Source #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Level -> Doc Source # prettyPrec :: Int -> Level -> Doc Source # prettyList :: [Level] -> Doc Source #
Pretty Sort Source #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Sort -> Doc Source # prettyPrec :: Int -> Sort -> Doc Source # prettyList :: [Sort] -> Doc Source #
Pretty Type Source #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Type -> Doc Source # prettyPrec :: Int -> Type -> Doc Source # prettyList :: [Type] -> Doc Source #
Pretty Term Source #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Term -> Doc Source # prettyPrec :: Int -> Term -> Doc Source # prettyList :: [Term] -> Doc Source #
Pretty CompiledClauses Source #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods pretty :: CompiledClauses -> Doc Source # prettyPrec :: Int -> CompiledClauses -> Doc Source # prettyList :: [CompiledClauses] -> Doc Source #
KillRange Substitution Source #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Substitution Source #
KillRange LevelAtom Source #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT LevelAtom Source #
KillRange PlusLevel Source #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT PlusLevel Source #
KillRange Level Source #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Level Source #
KillRange Sort Source #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Sort Source #
KillRange Term Source #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Term Source #
KillRange CompiledClauses Source #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods killRange :: KillRangeT CompiledClauses Source #
TermSize LevelAtom Source #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: LevelAtom -> Int Source # tsize :: LevelAtom -> Sum Int Source #
TermSize PlusLevel Source #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: PlusLevel -> Int Source # tsize :: PlusLevel -> Sum Int Source #
TermSize Level Source #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Level -> Int Source # tsize :: Level -> Sum Int Source #
TermSize Sort Source #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Sort -> Int Source # tsize :: Sort -> Sum Int Source #
TermSize Term Source #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Term -> Int Source # tsize :: Term -> Sum Int Source #
Suggest Term Source #
Instance details Defined in Agda.Syntax.Internal Methods suggestName :: Term -> Maybe String Source #
TelToArgs ListTel Source #
Instance details Defined in Agda.Syntax.Internal Methods telToArgs :: ListTel -> [Arg ArgName] Source #
TelToArgs Telescope Source #
Instance details Defined in Agda.Syntax.Internal Methods telToArgs :: Telescope -> [Arg ArgName] Source #
DeBruijn LevelAtom Source #
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> LevelAtom Source # debruijnNamedVar :: String -> Int -> LevelAtom Source # deBruijnView :: LevelAtom -> Maybe Int Source #
DeBruijn PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> PlusLevel Source # debruijnNamedVar :: String -> Int -> PlusLevel Source # deBruijnView :: PlusLevel -> Maybe Int Source #
DeBruijn Level Source #
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> Level Source # debruijnNamedVar :: String -> Int -> Level Source # deBruijnView :: Level -> Maybe Int Source #
DeBruijn Term Source #	We can substitute `Term`s for variables.
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> Term Source # debruijnNamedVar :: String -> Int -> Term Source # deBruijnView :: Term -> Maybe Int Source #
PrecomputeFreeVars LevelAtom Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: LevelAtom -> FV LevelAtom Source #
PrecomputeFreeVars PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: PlusLevel -> FV PlusLevel Source #
PrecomputeFreeVars Level Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Level -> FV Level Source #
PrecomputeFreeVars Sort Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Sort -> FV Sort Source #
PrecomputeFreeVars Type Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Type -> FV Type Source #
PrecomputeFreeVars Term Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Term -> FV Term Source #
Free LevelAtom Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => LevelAtom -> FreeM a c Source #
Free PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => PlusLevel -> FreeM a c Source #
Free Level Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Level -> FreeM a c Source #
Free Sort Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Sort -> FreeM a c Source #
Free Term Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Term -> FreeM a c Source #
Abstract Sort Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Sort -> Sort Source #
Abstract Telescope Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Telescope -> Telescope Source #
Abstract Type Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Type -> Type Source #
Abstract Term Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Term -> Term Source #
Abstract CompiledClauses Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> CompiledClauses -> CompiledClauses Source #
Apply Sort Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Sort -> Args -> Sort Source # applyE :: Sort -> Elims -> Sort Source #
Apply Term Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Term -> Args -> Term Source # applyE :: Term -> Elims -> Term Source #
Apply CompiledClauses Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: CompiledClauses -> Args -> CompiledClauses Source # applyE :: CompiledClauses -> Elims -> CompiledClauses Source #
TermLike LevelAtom Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> LevelAtom -> m LevelAtom Source # foldTerm :: Monoid m => (Term -> m) -> LevelAtom -> m Source #
TermLike PlusLevel Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> PlusLevel -> m PlusLevel Source # foldTerm :: Monoid m => (Term -> m) -> PlusLevel -> m Source #
TermLike Level Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Level -> m Level Source # foldTerm :: Monoid m => (Term -> m) -> Level -> m Source #
TermLike Sort Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Sort -> m Sort Source # foldTerm :: Monoid m => (Term -> m) -> Sort -> m Source #
TermLike Type Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Type -> m Type Source # foldTerm :: Monoid m => (Term -> m) -> Type -> m Source #
TermLike Term Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Term -> m Term Source # foldTerm :: Monoid m => (Term -> m) -> Term -> m Source #
GetDefs LevelAtom Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => LevelAtom -> m () Source #
GetDefs PlusLevel Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => PlusLevel -> m () Source #
GetDefs Level Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Level -> m () Source #
GetDefs Sort Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Sort -> m () Source #
GetDefs Type Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Type -> m () Source #
GetDefs Term Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Term -> m () Source #
EmbPrj LevelAtom Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: LevelAtom -> S Int32 Source # icod_ :: LevelAtom -> S Int32 Source # value :: Int32 -> R LevelAtom Source #
EmbPrj PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: PlusLevel -> S Int32 Source # icod_ :: PlusLevel -> S Int32 Source # value :: Int32 -> R PlusLevel Source #
EmbPrj Level Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Level -> S Int32 Source # icod_ :: Level -> S Int32 Source # value :: Int32 -> R Level Source #
EmbPrj Sort Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Sort -> S Int32 Source # icod_ :: Sort -> S Int32 Source # value :: Int32 -> R Sort Source #
EmbPrj Term Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Term -> S Int32 Source # icod_ :: Term -> S Int32 Source # value :: Int32 -> R Term Source #
EmbPrj CompiledClauses Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: CompiledClauses -> S Int32 Source # icod_ :: CompiledClauses -> S Int32 Source # value :: Int32 -> R CompiledClauses Source #
PrettyTCM Level Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Level -> m Doc Source #
PrettyTCM Sort Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Sort -> m Doc Source #
PrettyTCM Telescope Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Telescope -> m Doc Source #
PrettyTCM Type Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Type -> m Doc Source #
PrettyTCM Elim Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Elim -> m Doc Source #
PrettyTCM Term Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Term -> m Doc Source #
NamesIn LevelAtom Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: LevelAtom -> Set QName Source #
NamesIn PlusLevel Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: PlusLevel -> Set QName Source #
NamesIn Level Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Level -> Set QName Source #
NamesIn Sort Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Sort -> Set QName Source #
NamesIn Term Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Term -> Set QName Source #
NamesIn CompiledClauses Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: CompiledClauses -> Set QName Source #
TeleNoAbs ListTel Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods teleNoAbs :: ListTel -> Term -> Term Source #
TeleNoAbs Telescope Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods teleNoAbs :: Telescope -> Term -> Term Source #
AddContext Telescope Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Telescope -> m a -> m a Source # contextSize :: Telescope -> Nat Source #
PiApplyM Term Source #
Instance details Defined in Agda.TypeChecking.Telescope Methods piApplyM :: MonadReduce m => Type -> Term -> m Type Source #
IsSizeType Term Source #
Instance details Defined in Agda.TypeChecking.Monad.SizedTypes Methods isSizeType :: (HasOptions m, HasBuiltins m) => Term -> m (Maybe BoundedSize) Source #
DropArgs Telescope Source #	NOTE: This creates telescopes with unbound de Bruijn indices.
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> Telescope -> Telescope Source #
DropArgs Term Source #	Use for dropping initial lambdas in clause bodies. NOTE: does not reduce term, need lambdas to be present.
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> Term -> Term Source #
DropArgs CompiledClauses Source #	To drop the first `n` arguments in a compiled clause, we reduce the split argument indices by `n` and drop `n` arguments from the bodies. NOTE: this only works for non-recursive functions, we are not dropping arguments to recursive calls in bodies.
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> CompiledClauses -> CompiledClauses Source #
UnFreezeMeta LevelAtom Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => LevelAtom -> m () Source #
UnFreezeMeta PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => PlusLevel -> m () Source #
UnFreezeMeta Level Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Level -> m () Source #
UnFreezeMeta Sort Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Sort -> m () Source #
UnFreezeMeta Type Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Type -> m () Source #
UnFreezeMeta Term Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Term -> m () Source #
IsInstantiatedMeta LevelAtom Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => LevelAtom -> m Bool Source #
IsInstantiatedMeta PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => PlusLevel -> m Bool Source #
IsInstantiatedMeta Level Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Level -> m Bool Source #
IsInstantiatedMeta Term Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Term -> m Bool Source #
MentionsMeta LevelAtom Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> LevelAtom -> Bool Source #
MentionsMeta PlusLevel Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> PlusLevel -> Bool Source #
MentionsMeta Level Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Level -> Bool Source #
MentionsMeta Sort Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Sort -> Bool Source #
MentionsMeta Type Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Type -> Bool Source #
MentionsMeta Elim Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Elim -> Bool Source #
MentionsMeta Term Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Term -> Bool Source #
InstantiateFull Substitution Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Substitution -> ReduceM Substitution Source #
InstantiateFull LevelAtom Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: LevelAtom -> ReduceM LevelAtom Source #
InstantiateFull PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: PlusLevel -> ReduceM PlusLevel Source #
InstantiateFull Level Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Level -> ReduceM Level Source #
InstantiateFull Sort Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Sort -> ReduceM Sort Source #
InstantiateFull Term Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Term -> ReduceM Term Source #
InstantiateFull CompiledClauses Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: CompiledClauses -> ReduceM CompiledClauses Source #
Normalise LevelAtom Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: LevelAtom -> ReduceM LevelAtom Source #
Normalise PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: PlusLevel -> ReduceM PlusLevel Source #
Normalise Level Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Level -> ReduceM Level Source #
Normalise Sort Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Sort -> ReduceM Sort Source #
Normalise Term Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Term -> ReduceM Term Source #
Simplify LevelAtom Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: LevelAtom -> ReduceM LevelAtom Source #
Simplify PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: PlusLevel -> ReduceM PlusLevel Source #
Simplify Level Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Level -> ReduceM Level Source #
Simplify Sort Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Sort -> ReduceM Sort Source #
Simplify Term Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Term -> ReduceM Term Source #
Reduce LevelAtom Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: LevelAtom -> ReduceM LevelAtom Source # reduceB' :: LevelAtom -> ReduceM (Blocked LevelAtom) Source #
Reduce PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: PlusLevel -> ReduceM PlusLevel Source # reduceB' :: PlusLevel -> ReduceM (Blocked PlusLevel) Source #
Reduce Level Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Level -> ReduceM Level Source # reduceB' :: Level -> ReduceM (Blocked Level) Source #
Reduce Sort Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Sort -> ReduceM Sort Source # reduceB' :: Sort -> ReduceM (Blocked Sort) Source #
Reduce Telescope Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Telescope -> ReduceM Telescope Source # reduceB' :: Telescope -> ReduceM (Blocked Telescope) Source #
Reduce Type Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Type -> ReduceM Type Source # reduceB' :: Type -> ReduceM (Blocked Type) Source #
Reduce Elim Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Elim -> ReduceM Elim Source # reduceB' :: Elim -> ReduceM (Blocked Elim) Source #
Reduce Term Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Term -> ReduceM Term Source # reduceB' :: Term -> ReduceM (Blocked Term) Source #
IsMeta Level Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods isMeta :: HasBuiltins m => Level -> m (Maybe MetaId) Source #
IsMeta Sort Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods isMeta :: HasBuiltins m => Sort -> m (Maybe MetaId) Source #
IsMeta Type Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods isMeta :: HasBuiltins m => Type -> m (Maybe MetaId) Source #
IsMeta Term Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods isMeta :: HasBuiltins m => Term -> m (Maybe MetaId) Source #
Instantiate LevelAtom Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: LevelAtom -> ReduceM LevelAtom Source #
Instantiate PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: PlusLevel -> ReduceM PlusLevel Source #
Instantiate Level Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Level -> ReduceM Level Source #
Instantiate Sort Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Sort -> ReduceM Sort Source #
Instantiate Term Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Term -> ReduceM Term Source #
SynEq LevelAtom Source #
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: LevelAtom -> LevelAtom -> SynEqM (LevelAtom, LevelAtom) synEq' :: LevelAtom -> LevelAtom -> SynEqM (LevelAtom, LevelAtom)
SynEq PlusLevel Source #
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: PlusLevel -> PlusLevel -> SynEqM (PlusLevel, PlusLevel) synEq' :: PlusLevel -> PlusLevel -> SynEqM (PlusLevel, PlusLevel)
SynEq Level Source #
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Level -> Level -> SynEqM (Level, Level) synEq' :: Level -> Level -> SynEqM (Level, Level)
SynEq Sort Source #
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Sort -> Sort -> SynEqM (Sort, Sort) synEq' :: Sort -> Sort -> SynEqM (Sort, Sort)
SynEq Type Source #	Syntactic equality ignores sorts.
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Type -> Type -> SynEqM (Type, Type) synEq' :: Type -> Type -> SynEqM (Type, Type)
SynEq Term Source #	Syntactic term equality ignores `DontCare` stuff.
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Term -> Term -> SynEqM (Term, Term) synEq' :: Term -> Term -> SynEqM (Term, Term)
ToTerm Type Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Type -> Term) Source # toTermR :: TCM (Type -> ReduceM Term) Source #
ToTerm Term Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Term -> Term) Source # toTermR :: TCM (Term -> ReduceM Term) Source #
PrimTerm Type Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Type -> TCM Term Source #
ForceNotFree LevelAtom Source #
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => LevelAtom -> m LevelAtom
ForceNotFree PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => PlusLevel -> m PlusLevel
ForceNotFree Level Source #
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Level -> m Level
ForceNotFree Sort Source #
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Sort -> m Sort
ForceNotFree Type Source #
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Type -> m Type
ForceNotFree Term Source #
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Term -> m Term
SubstWithOrigin Term Source #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods substWithOrigin :: Substitution -> [WithOrigin Term] -> Term -> Term Source #
Match Level Source #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods match :: forall (m :: Type -> Type). MonadDisplayForm m => Level -> Level -> MaybeT m [WithOrigin Term] Source #
Match Sort Source #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods match :: forall (m :: Type -> Type). MonadDisplayForm m => Sort -> Sort -> MaybeT m [WithOrigin Term] Source #
Match Term Source #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods match :: forall (m :: Type -> Type). MonadDisplayForm m => Term -> Term -> MaybeT m [WithOrigin Term] Source #
UsableModality Level Source #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Level -> TCM Bool Source #
UsableModality Sort Source #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Sort -> TCM Bool Source #
UsableModality Term Source #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Term -> TCM Bool Source #
UsableRelevance LevelAtom Source #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> LevelAtom -> TCM Bool Source #
UsableRelevance PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> PlusLevel -> TCM Bool Source #
UsableRelevance Level Source #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Level -> TCM Bool Source #
UsableRelevance Sort Source #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Sort -> TCM Bool Source #
UsableRelevance Term Source #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Term -> TCM Bool Source #
GetMatchables Term Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: Term -> [QName] Source #
ComputeOccurrences LevelAtom Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: LevelAtom -> OccM OccurrencesBuilder Source #
ComputeOccurrences PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: PlusLevel -> OccM OccurrencesBuilder Source #
ComputeOccurrences Level Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Level -> OccM OccurrencesBuilder Source #
ComputeOccurrences Type Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Type -> OccM OccurrencesBuilder Source #
ComputeOccurrences Term Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Term -> OccM OccurrencesBuilder Source #
HasPolarity LevelAtom Source #
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> LevelAtom -> TCM [Polarity] Source #
HasPolarity PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> PlusLevel -> TCM [Polarity] Source #
HasPolarity Level Source #
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Level -> TCM [Polarity] Source #
HasPolarity Type Source #
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Type -> TCM [Polarity] Source #
HasPolarity Term Source #
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Term -> TCM [Polarity] Source #
AnyRigid LevelAtom Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat -> tcm Bool) -> LevelAtom -> tcm Bool Source #
AnyRigid PlusLevel Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat -> tcm Bool) -> PlusLevel -> tcm Bool Source #
AnyRigid Level Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat -> tcm Bool) -> Level -> tcm Bool Source #
AnyRigid Sort Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat -> tcm Bool) -> Sort -> tcm Bool Source #
AnyRigid Type Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat -> tcm Bool) -> Type -> tcm Bool Source #
AnyRigid Term Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat -> tcm Bool) -> Term -> tcm Bool Source #
Occurs LevelAtom Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: LevelAtom -> OccursM LevelAtom Source # metaOccurs :: MetaId -> LevelAtom -> TCM () Source #
Occurs PlusLevel Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: PlusLevel -> OccursM PlusLevel Source # metaOccurs :: MetaId -> PlusLevel -> TCM () Source #
Occurs Level Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Level -> OccursM Level Source # metaOccurs :: MetaId -> Level -> TCM () Source #
Occurs Sort Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Sort -> OccursM Sort Source # metaOccurs :: MetaId -> Sort -> TCM () Source #
Occurs Type Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Type -> OccursM Type Source # metaOccurs :: MetaId -> Type -> TCM () Source #
Occurs Term Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Term -> OccursM Term Source # metaOccurs :: MetaId -> Term -> TCM () Source #
ReduceAndEtaContract Term Source #
Instance details Defined in Agda.TypeChecking.MetaVars Methods reduceAndEtaContract :: Term -> TCM Term Source #
NoProjectedVar Term Source #
Instance details Defined in Agda.TypeChecking.MetaVars Methods noProjectedVar :: Term -> Either ProjVarExc () Source #
EqualSy LevelAtom Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: LevelAtom -> LevelAtom -> Bool Source #
EqualSy PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: PlusLevel -> PlusLevel -> Bool Source #
EqualSy Level Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Level -> Level -> Bool Source #
EqualSy Sort Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Sort -> Sort -> Bool Source #
EqualSy Type Source #	Ignores sorts.
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Type -> Type -> Bool Source #
EqualSy Term Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Term -> Term -> Bool Source #
AbsTerm LevelAtom Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> LevelAtom -> LevelAtom Source #
AbsTerm PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> PlusLevel -> PlusLevel Source #
AbsTerm Level Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Level -> Level Source #
AbsTerm Sort Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Sort -> Sort Source #
AbsTerm Type Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Type -> Type Source #
AbsTerm Term Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Term -> Term Source #
IsPrefixOf Elims Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods isPrefixOf :: Elims -> Elims -> Maybe Elims Source #
IsPrefixOf Term Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods isPrefixOf :: Term -> Term -> Maybe Elims Source #
IsPrefixOf Args Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods isPrefixOf :: Args -> Args -> Maybe Elims Source #
Subst Term () Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> () -> () Source #
Subst Term String Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> String -> String Source #
Subst Term Range Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Range -> Range Source #
Subst Term QName Source #
Instance details Defined in Agda.TypeChecking.Substitute.Class Methods applySubst :: Substitution' Term -> QName -> QName Source #
Subst Term Name Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Name -> Name Source #
Subst Term EqualityView Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> EqualityView -> EqualityView Source #
Subst Term ConPatternInfo Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> ConPatternInfo -> ConPatternInfo Source #
Subst Term Pattern Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Pattern -> Pattern Source #
Subst Term Term Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Term -> Term Source #
Subst Term ProblemEq Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> ProblemEq -> ProblemEq Source #
Subst Term Candidate Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Candidate -> Candidate Source #
Subst Term DisplayTerm Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> DisplayTerm -> DisplayTerm Source #
Subst Term DisplayForm Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> DisplayForm -> DisplayForm Source #
Subst Term CompareAs Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> CompareAs -> CompareAs Source #
Subst Term Constraint Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Constraint -> Constraint Source #
Subst Term SingleLevel Source #
Instance details Defined in Agda.TypeChecking.Level Methods applySubst :: Substitution' Term -> SingleLevel -> SingleLevel Source #
Subst Term AbsurdPattern Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods applySubst :: Substitution' Term -> AbsurdPattern -> AbsurdPattern Source #
Subst Term DotPattern Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods applySubst :: Substitution' Term -> DotPattern -> DotPattern Source #
Subst Term AsBinding Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods applySubst :: Substitution' Term -> AsBinding -> AsBinding Source #
Subst Term SizeConstraint Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods applySubst :: Substitution' Term -> SizeConstraint -> SizeConstraint Source #
Subst Term SizeMeta Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods applySubst :: Substitution' Term -> SizeMeta -> SizeMeta Source #
Subst Term CType Source #
Instance details Defined in Agda.TypeChecking.Rules.Data Methods applySubst :: Substitution' Term -> CType -> CType Source #
Subst Term LType Source #
Instance details Defined in Agda.TypeChecking.Rules.Data Methods applySubst :: Substitution' Term -> LType -> LType Source #
Reify Level Expr Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MonadReify m => Level -> m Expr Source # reifyWhen :: MonadReify m => Bool -> Level -> m Expr Source #
Reify Sort Expr Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MonadReify m => Sort -> m Expr Source # reifyWhen :: MonadReify m => Bool -> Sort -> m Expr Source #
Reify Telescope Telescope Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MonadReify m => Telescope0 -> m Telescope Source # reifyWhen :: MonadReify m => Bool -> Telescope0 -> m Telescope Source #
Reify Type Expr Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MonadReify m => Type -> m Expr Source # reifyWhen :: MonadReify m => Bool -> Type -> m Expr Source #
Reify Term Expr Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MonadReify m => Term -> m Expr Source # reifyWhen :: MonadReify m => Bool -> Term -> m Expr Source #
NLPatToTerm Nat Term Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: (MonadReduce m, HasBuiltins m, HasConstInfo m, MonadDebug m) => Nat -> m Term Source #
NLPatToTerm NLPSort Sort Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: (MonadReduce m, HasBuiltins m, HasConstInfo m, MonadDebug m) => NLPSort -> m Sort Source #
NLPatToTerm NLPType Type Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: (MonadReduce m, HasBuiltins m, HasConstInfo m, MonadDebug m) => NLPType -> m Type Source #
NLPatToTerm NLPat Level Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: (MonadReduce m, HasBuiltins m, HasConstInfo m, MonadDebug m) => NLPat -> m Level Source #
NLPatToTerm NLPat Term Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: (MonadReduce m, HasBuiltins m, HasConstInfo m, MonadDebug m) => NLPat -> m Term Source #
PatternFrom () Level NLPat Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> () -> Level -> TCM NLPat Source #
PatternFrom () Sort NLPSort Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> () -> Sort -> TCM NLPSort Source #
PatternFrom () Type NLPType Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> () -> Type -> TCM NLPType Source #
PatternFrom Type Term NLPat Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> Type -> Term -> TCM NLPat Source #
Match () NLPSort Sort Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> () -> NLPSort -> Sort -> NLM () Source #
Match () NLPType Type Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> () -> NLPType -> Type -> NLM () Source #
Match () NLPat Level Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> () -> NLPat -> Level -> NLM () Source #
Match Type NLPat Term Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM () Source #
Conversion TOM Type (MExp O) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Type -> TOM (MExp O) Source #
Conversion TOM Term (MExp O) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Term -> TOM (MExp O) Source #
Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) Source #
Subst Term (Problem a) Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods applySubst :: Substitution' Term -> Problem a -> Problem a Source #
DeBruijn (Pattern' a) => TermToPattern Term (Pattern' a) Source #
Instance details Defined in Agda.TypeChecking.Patterns.Internal Methods termToPattern :: Term -> TCM (Pattern' a) Source #
Conversion MOT (Exp O) Type Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Type Source #
Conversion MOT (Exp O) Term Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Term Source #
PatternFrom t a b => PatternFrom t (Dom a) (Dom b) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> t -> Dom a -> TCM (Dom b) Source #
Match t a b => Match t (Dom a) (Dom b) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> t -> Dom a -> Dom b -> NLM () Source #
Subst Term (SizeExpr' NamedRigid SizeMeta) Source #	Only for `raise`.
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods applySubst :: Substitution' Term -> SizeExpr' NamedRigid SizeMeta -> SizeExpr' NamedRigid SizeMeta Source #
Eq a => Eq (Type' a) Source #	Syntactic `Type` equality, ignores sort annotations.
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Type' a -> Type' a -> Bool # (/=) :: Type' a -> Type' a -> Bool #
Ord a => Ord (Type' a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Type' a -> Type' a -> Ordering # (<) :: Type' a -> Type' a -> Bool # (<=) :: Type' a -> Type' a -> Bool # (>) :: Type' a -> Type' a -> Bool # (>=) :: Type' a -> Type' a -> Bool # max :: Type' a -> Type' a -> Type' a # min :: Type' a -> Type' a -> Type' a #
Ord a => Ord (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Dom a -> Dom a -> Ordering # (<) :: Dom a -> Dom a -> Bool # (<=) :: Dom a -> Dom a -> Bool # (>) :: Dom a -> Dom a -> Bool # (>=) :: Dom a -> Dom a -> Bool # max :: Dom a -> Dom a -> Dom a # min :: Dom a -> Dom a -> Dom a #
NFData e => NFData (Dom e) Source #
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Dom e -> () #
Pretty a => Pretty (Tele (Dom a)) Source #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Tele (Dom a) -> Doc Source # prettyPrec :: Int -> Tele (Dom a) -> Doc Source # prettyList :: [Tele (Dom a)] -> Doc Source #
KillRange a => KillRange (Type' a) Source #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Type' a) Source #
SgTel (Dom (ArgName, Type)) Source #
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom (ArgName, Type) -> Telescope Source #
SgTel (Dom Type) Source #
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom Type -> Telescope Source #
LensSort (Type' a) Source #
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' Sort (Type' a) Source # getSort :: Type' a -> Sort Source #
LensSort a => LensSort (Dom a) Source #
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' Sort (Dom a) Source # getSort :: Dom a -> Sort Source #
PrecomputeFreeVars a => PrecomputeFreeVars (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Dom a -> FV (Dom a) Source #
Free t => Free (Type' t) Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Type' t -> FreeM a c Source #
Free t => Free (Dom t) Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Dom t -> FreeM a c Source #
TermLike a => TermLike (Dom a) Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Dom a -> m (Dom a) Source # foldTerm :: Monoid m => (Term -> m) -> Dom a -> m Source #
GetDefs a => GetDefs (Dom a) Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Dom a -> m () Source #
EmbPrj a => EmbPrj (Type' a) Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Type' a -> S Int32 Source # icod_ :: Type' a -> S Int32 Source # value :: Int32 -> R (Type' a) Source #
EmbPrj a => EmbPrj (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Dom a -> S Int32 Source # icod_ :: Dom a -> S Int32 Source # value :: Int32 -> R (Dom a) Source #
PrettyTCM (Type' NLPat) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Type' NLPat -> m Doc Source #
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Dom a -> m Doc Source #
NamesIn a => NamesIn (Type' a) Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Type' a -> Set QName Source #
NamesIn a => NamesIn (Dom a) Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Dom a -> Set QName Source #
AddContext (Dom (String, Type)) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Dom (String, Type) -> m a -> m a Source # contextSize :: Dom (String, Type) -> Nat Source #
AddContext (Dom (Name, Type)) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Dom (Name, Type) -> m a -> m a Source # contextSize :: Dom (Name, Type) -> Nat Source #
AddContext (Dom Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Dom Type -> m a -> m a Source # contextSize :: Dom Type -> Nat Source #
AddContext (KeepNames Telescope) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => KeepNames Telescope -> m a -> m a Source # contextSize :: KeepNames Telescope -> Nat Source #
IsSizeType a => IsSizeType (Type' a) Source #
Instance details Defined in Agda.TypeChecking.Monad.SizedTypes Methods isSizeType :: (HasOptions m, HasBuiltins m) => Type' a -> m (Maybe BoundedSize) Source #
IsSizeType a => IsSizeType (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Monad.SizedTypes Methods isSizeType :: (HasOptions m, HasBuiltins m) => Dom a -> m (Maybe BoundedSize) Source #
MentionsMeta t => MentionsMeta (Dom t) Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Dom t -> Bool Source #
InstantiateFull t => InstantiateFull (Type' t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Type' t -> ReduceM (Type' t) Source #
Normalise t => Normalise (Type' t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Type' t -> ReduceM (Type' t) Source #
Normalise t => Normalise (Dom t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Dom t -> ReduceM (Dom t) Source #
Simplify t => Simplify (Type' t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Type' t -> ReduceM (Type' t) Source #
Simplify t => Simplify (Dom t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Dom t -> ReduceM (Dom t) Source #
Reduce t => Reduce (Dom t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Dom t -> ReduceM (Dom t) Source # reduceB' :: Dom t -> ReduceM (Blocked (Dom t)) Source #
Instantiate t => Instantiate (Type' t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Type' t -> ReduceM (Type' t) Source #
SynEq a => SynEq (Dom a) Source #
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Dom a -> Dom a -> SynEqM (Dom a, Dom a) synEq' :: Dom a -> Dom a -> SynEqM (Dom a, Dom a)
(Reduce a, ForceNotFree a) => ForceNotFree (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Dom a -> m (Dom a)
SubstWithOrigin (Arg Term) Source #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods substWithOrigin :: Substitution -> [WithOrigin Term] -> Arg Term -> Arg Term Source #
UsableRelevance a => UsableModality (Type' a) Source #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Type' a -> TCM Bool Source #
UsableModality a => UsableModality (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Dom a -> TCM Bool Source #
UsableRelevance a => UsableRelevance (Type' a) Source #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Type' a -> TCM Bool Source #
UsableRelevance a => UsableRelevance (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Dom a -> TCM Bool Source #
GetMatchables a => GetMatchables (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: Dom a -> [QName] Source #
ComputeOccurrences a => ComputeOccurrences (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Dom a -> OccM OccurrencesBuilder Source #
HasPolarity a => HasPolarity (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Dom a -> TCM [Polarity] Source #
AnyRigid a => AnyRigid (Dom a) Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat -> tcm Bool) -> Dom a -> tcm Bool Source #
Occurs a => Occurs (Dom a) Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Dom a -> OccursM (Dom a) Source # metaOccurs :: MetaId -> Dom a -> TCM () Source #
Unquote a => Unquote (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM (Dom a) Source #
EqualSy a => EqualSy (Dom a) Source #	Ignore the tactic.
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Dom a -> Dom a -> Bool Source #
AbsTerm a => AbsTerm (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Dom a -> Dom a Source #
ToNLPat a b => ToNLPat (Dom a) (Dom b) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: Dom a -> Dom b Source #
Reify i a => Reify (Dom i) (Arg a) Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MonadReify m => Dom i -> m (Arg a) Source # reifyWhen :: MonadReify m => Bool -> Dom i -> m (Arg a) Source #
NLPatToTerm p a => NLPatToTerm (Dom p) (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: (MonadReduce m, HasBuiltins m, HasConstInfo m, MonadDebug m) => Dom p -> m (Dom a) Source #
PatternFrom t a b => PatternFrom (Dom t) (Arg a) (Arg b) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> Dom t -> Arg a -> TCM (Arg b) Source #
Match t a b => Match (Dom t) (Arg a) (Arg b) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> Dom t -> Arg a -> Arg b -> NLM () Source #
SgTel (ArgName, Dom Type) Source #
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: (ArgName, Dom Type) -> Telescope Source #
AddContext ([NamedArg Name], Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # contextSize :: ([NamedArg Name], Type) -> Nat Source #
AddContext ([Arg Name], Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([Arg Name], Type) -> m a -> m a Source # contextSize :: ([Arg Name], Type) -> Nat Source #
AddContext ([WithHiding Name], Dom Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([WithHiding Name], Dom Type) -> m a -> m a Source # contextSize :: ([WithHiding Name], Dom Type) -> Nat Source #
AddContext ([Name], Dom Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([Name], Dom Type) -> m a -> m a Source # contextSize :: ([Name], Dom Type) -> Nat Source #
AddContext (String, Dom Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (String, Dom Type) -> m a -> m a Source # contextSize :: (String, Dom Type) -> Nat Source #
AddContext (Name, Dom Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (Name, Dom Type) -> m a -> m a Source # contextSize :: (Name, Dom Type) -> Nat Source #
AddContext (KeepNames String, Dom Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (KeepNames String, Dom Type) -> m a -> m a Source # contextSize :: (KeepNames String, Dom Type) -> Nat Source #
ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBinding Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => (Dom r, Name) -> m TypedBinding Source #
PatternFrom (Type, Term) Elims [Elim' NLPat] Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat] Source #
Match (Type, Term) [Elim' NLPat] Elims Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> (Type, Term) -> [Elim' NLPat] -> Elims -> NLM () Source #

class LensConName a where Source #

Minimal complete definition

getConName

Methods

getConName :: a -> QName Source #

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

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

Instances

Instances details

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

data ConHead Source #

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

Constructors

ConHead
Fields conName :: QName The name of the constructor. conInductive :: Induction Record constructors can be coinductive. conFields :: [Arg QName] The name of the record fields. Empty list for data constructors. `Arg` is stored since the info in the constructor args might not be accurate because of subtyping (issue #2170).

Instances

Instances details

Eq ConHead Source #
Instance details Defined in Agda.Syntax.Internal Methods (==) :: ConHead -> ConHead -> Bool # (/=) :: ConHead -> ConHead -> Bool #
Data ConHead Source #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConHead -> c ConHead # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConHead # toConstr :: ConHead -> Constr # dataTypeOf :: ConHead -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConHead) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConHead) # gmapT :: (forall b. Data b => b -> b) -> ConHead -> ConHead # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConHead -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConHead -> r # gmapQ :: (forall d. Data d => d -> u) -> ConHead -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ConHead -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConHead -> m ConHead # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConHead -> m ConHead # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConHead -> m ConHead #
Ord ConHead Source #
Instance details Defined in Agda.Syntax.Internal 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 Source #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> ConHead -> ShowS # show :: ConHead -> String # showList :: [ConHead] -> ShowS #
Pretty ConHead Source #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: ConHead -> Doc Source # prettyPrec :: Int -> ConHead -> Doc Source # prettyList :: [ConHead] -> Doc Source #
KillRange ConHead Source #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT ConHead Source #
SetRange ConHead Source #
Instance details Defined in Agda.Syntax.Internal Methods setRange :: Range -> ConHead -> ConHead Source #
HasRange ConHead Source #
Instance details Defined in Agda.Syntax.Internal Methods getRange :: ConHead -> Range Source #
LensConName ConHead Source #
Instance details Defined in Agda.Syntax.Internal Methods getConName :: ConHead -> QName Source # setConName :: QName -> ConHead -> ConHead Source # mapConName :: (QName -> QName) -> ConHead -> ConHead Source #
EmbPrj ConHead Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ConHead -> S Int32 Source # icod_ :: ConHead -> S Int32 Source # value :: Int32 -> R ConHead Source #
PrettyTCM ConHead Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ConHead -> m Doc Source #
NamesIn ConHead Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: ConHead -> Set QName Source #
InstantiateFull ConHead Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ConHead -> ReduceM ConHead Source #

type NamedArgs = [NamedArg Term] Source #

type Args = [Arg Term] Source #

Type of argument lists.

type Dom = Dom' Term Source #

data Dom' t e Source #

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

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

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

Constructors

Dom
Fields domInfo :: ArgInfo domFinite :: !Bool domName :: Maybe NamedName e.g. `x` in `{x = y : A} -> B`. domTactic :: Maybe t "@tactic e". unDom :: e

Instances

Instances details

TelToArgs ListTel Source #
Instance details Defined in Agda.Syntax.Internal Methods telToArgs :: ListTel -> [Arg ArgName] Source #
TelToArgs Telescope Source #
Instance details Defined in Agda.Syntax.Internal Methods telToArgs :: Telescope -> [Arg ArgName] Source #
Abstract Telescope Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Telescope -> Telescope Source #
PrettyTCM Telescope Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Telescope -> m Doc Source #
TeleNoAbs ListTel Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods teleNoAbs :: ListTel -> Term -> Term Source #
TeleNoAbs Telescope Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods teleNoAbs :: Telescope -> Term -> Term Source #
AddContext Telescope Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Telescope -> m a -> m a Source # contextSize :: Telescope -> Nat Source #
DropArgs Telescope Source #	NOTE: This creates telescopes with unbound de Bruijn indices.
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> Telescope -> Telescope Source #
Reduce Telescope Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Telescope -> ReduceM Telescope Source # reduceB' :: Telescope -> ReduceM (Blocked Telescope) Source #
Reify Telescope Telescope Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MonadReify m => Telescope0 -> m Telescope Source # reifyWhen :: MonadReify m => Bool -> Telescope0 -> m Telescope Source #
PatternFrom t a b => PatternFrom t (Dom a) (Dom b) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> t -> Dom a -> TCM (Dom b) Source #
Match t a b => Match t (Dom a) (Dom b) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> t -> Dom a -> Dom b -> NLM () Source #
LensNamed NamedName (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods lensNamed :: Lens' (Maybe NamedName) (Dom' t e) Source #
(Subst t a, Subst t b) => Subst t (Dom' a b) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Dom' a b -> Dom' a b Source #
Functor (Dom' t) Source #
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Dom' t a -> Dom' t b # (<$) :: a -> Dom' t b -> Dom' t a #
Ord a => Ord (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Dom a -> Dom a -> Ordering # (<) :: Dom a -> Dom a -> Bool # (<=) :: Dom a -> Dom a -> Bool # (>) :: Dom a -> Dom a -> Bool # (>=) :: Dom a -> Dom a -> Bool # max :: Dom a -> Dom a -> Dom a # min :: Dom a -> Dom a -> Dom a #
Foldable (Dom' t) Source #
Instance details Defined in Agda.Syntax.Internal Methods fold :: Monoid m => Dom' t m -> m # foldMap :: Monoid m => (a -> m) -> Dom' t a -> m # foldMap' :: Monoid m => (a -> m) -> Dom' t a -> m # foldr :: (a -> b -> b) -> b -> Dom' t a -> b # foldr' :: (a -> b -> b) -> b -> Dom' t a -> b # foldl :: (b -> a -> b) -> b -> Dom' t a -> b # foldl' :: (b -> a -> b) -> b -> Dom' t a -> b # foldr1 :: (a -> a -> a) -> Dom' t a -> a # foldl1 :: (a -> a -> a) -> Dom' t a -> a # toList :: Dom' t a -> [a] # null :: Dom' t a -> Bool # length :: Dom' t a -> Int # elem :: Eq a => a -> Dom' t a -> Bool # maximum :: Ord a => Dom' t a -> a # minimum :: Ord a => Dom' t a -> a # sum :: Num a => Dom' t a -> a # product :: Num a => Dom' t a -> a #
Traversable (Dom' t) Source #
Instance details Defined in Agda.Syntax.Internal Methods traverse :: Applicative f => (a -> f b) -> Dom' t a -> f (Dom' t b) # sequenceA :: Applicative f => Dom' t (f a) -> f (Dom' t a) # mapM :: Monad m => (a -> m b) -> Dom' t a -> m (Dom' t b) # sequence :: Monad m => Dom' t (m a) -> m (Dom' t a) #
NFData e => NFData (Dom e) Source #
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Dom e -> () #
Decoration (Dom' t) Source #
Instance details Defined in Agda.Syntax.Internal Methods traverseF :: Functor m => (a -> m b) -> Dom' t a -> m (Dom' t b) Source # distributeF :: Functor m => Dom' t (m a) -> m (Dom' t a) Source #
Pretty a => Pretty (Tele (Dom a)) Source #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Tele (Dom a) -> Doc Source # prettyPrec :: Int -> Tele (Dom a) -> Doc Source # prettyList :: [Tele (Dom a)] -> Doc Source #
SgTel (Dom (ArgName, Type)) Source #
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom (ArgName, Type) -> Telescope Source #
SgTel (Dom Type) Source #
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom Type -> Telescope Source #
LensSort a => LensSort (Dom a) Source #
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' Sort (Dom a) Source # getSort :: Dom a -> Sort Source #
PrecomputeFreeVars a => PrecomputeFreeVars (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Dom a -> FV (Dom a) Source #
Free t => Free (Dom t) Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Dom t -> FreeM a c Source #
TermLike a => TermLike (Dom a) Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Dom a -> m (Dom a) Source # foldTerm :: Monoid m => (Term -> m) -> Dom a -> m Source #
GetDefs a => GetDefs (Dom a) Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Dom a -> m () Source #
EmbPrj a => EmbPrj (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Dom a -> S Int32 Source # icod_ :: Dom a -> S Int32 Source # value :: Int32 -> R (Dom a) Source #
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Dom a -> m Doc Source #
NamesIn a => NamesIn (Dom a) Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Dom a -> Set QName Source #
AddContext (Dom (String, Type)) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Dom (String, Type) -> m a -> m a Source # contextSize :: Dom (String, Type) -> Nat Source #
AddContext (Dom (Name, Type)) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Dom (Name, Type) -> m a -> m a Source # contextSize :: Dom (Name, Type) -> Nat Source #
AddContext (Dom Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Dom Type -> m a -> m a Source # contextSize :: Dom Type -> Nat Source #
AddContext (KeepNames Telescope) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => KeepNames Telescope -> m a -> m a Source # contextSize :: KeepNames Telescope -> Nat Source #
IsSizeType a => IsSizeType (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Monad.SizedTypes Methods isSizeType :: (HasOptions m, HasBuiltins m) => Dom a -> m (Maybe BoundedSize) Source #
MentionsMeta t => MentionsMeta (Dom t) Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Dom t -> Bool Source #
Normalise t => Normalise (Dom t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Dom t -> ReduceM (Dom t) Source #
Simplify t => Simplify (Dom t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Dom t -> ReduceM (Dom t) Source #
Reduce t => Reduce (Dom t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Dom t -> ReduceM (Dom t) Source # reduceB' :: Dom t -> ReduceM (Blocked (Dom t)) Source #
SynEq a => SynEq (Dom a) Source #
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Dom a -> Dom a -> SynEqM (Dom a, Dom a) synEq' :: Dom a -> Dom a -> SynEqM (Dom a, Dom a)
(Reduce a, ForceNotFree a) => ForceNotFree (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Dom a -> m (Dom a)
UsableModality a => UsableModality (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Dom a -> TCM Bool Source #
UsableRelevance a => UsableRelevance (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Dom a -> TCM Bool Source #
GetMatchables a => GetMatchables (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: Dom a -> [QName] Source #
ComputeOccurrences a => ComputeOccurrences (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Dom a -> OccM OccurrencesBuilder Source #
HasPolarity a => HasPolarity (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Dom a -> TCM [Polarity] Source #
AnyRigid a => AnyRigid (Dom a) Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat -> tcm Bool) -> Dom a -> tcm Bool Source #
Occurs a => Occurs (Dom a) Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Dom a -> OccursM (Dom a) Source # metaOccurs :: MetaId -> Dom a -> TCM () Source #
Unquote a => Unquote (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM (Dom a) Source #
EqualSy a => EqualSy (Dom a) Source #	Ignore the tactic.
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Dom a -> Dom a -> Bool Source #
AbsTerm a => AbsTerm (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Dom a -> Dom a Source #
ToNLPat a b => ToNLPat (Dom a) (Dom b) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: Dom a -> Dom b Source #
Reify i a => Reify (Dom i) (Arg a) Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MonadReify m => Dom i -> m (Arg a) Source # reifyWhen :: MonadReify m => Bool -> Dom i -> m (Arg a) Source #
NLPatToTerm p a => NLPatToTerm (Dom p) (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: (MonadReduce m, HasBuiltins m, HasConstInfo m, MonadDebug m) => Dom p -> m (Dom a) Source #
PatternFrom t a b => PatternFrom (Dom t) (Arg a) (Arg b) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> Dom t -> Arg a -> TCM (Arg b) Source #
Match t a b => Match (Dom t) (Arg a) (Arg b) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> Dom t -> Arg a -> Arg b -> NLM () Source #
Eq a => Eq (Dom' t a) Source #	Ignores `Origin` and `FreeVariables` and tactic.
Instance details Defined in Agda.Syntax.Internal Methods (==) :: Dom' t a -> Dom' t a -> Bool # (/=) :: Dom' t a -> Dom' t a -> Bool #
(Data t, Data e) => Data (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Dom' t e -> c (Dom' t e) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Dom' t e) # toConstr :: Dom' t e -> Constr # dataTypeOf :: Dom' t e -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (Dom' t e)) # dataCast2 :: Typeable t0 => (forall d e0. (Data d, Data e0) => c (t0 d e0)) -> Maybe (c (Dom' t e)) # gmapT :: (forall b. Data b => b -> b) -> Dom' t e -> Dom' t e # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Dom' t e -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Dom' t e -> r # gmapQ :: (forall d. Data d => d -> u) -> Dom' t e -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Dom' t e -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Dom' t e -> m (Dom' t e) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Dom' t e -> m (Dom' t e) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Dom' t e -> m (Dom' t e) #
(Show t, Show e) => Show (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Dom' t e -> ShowS # show :: Dom' t e -> String # showList :: [Dom' t e] -> ShowS #
(Pretty t, Pretty e) => Pretty (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Dom' t e -> Doc Source # prettyPrec :: Int -> Dom' t e -> Doc Source # prettyList :: [Dom' t e] -> Doc Source #
(KillRange t, KillRange a) => KillRange (Dom' t a) Source #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Dom' t a) Source #
HasRange a => HasRange (Dom' t a) Source #
Instance details Defined in Agda.Syntax.Internal Methods getRange :: Dom' t a -> Range Source #
LensArgInfo (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods getArgInfo :: Dom' t e -> ArgInfo Source # setArgInfo :: ArgInfo -> Dom' t e -> Dom' t e Source # mapArgInfo :: (ArgInfo -> ArgInfo) -> Dom' t e -> Dom' t e Source #
LensFreeVariables (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods getFreeVariables :: Dom' t e -> FreeVariables Source # setFreeVariables :: FreeVariables -> Dom' t e -> Dom' t e Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> Dom' t e -> Dom' t e Source #
LensOrigin (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods getOrigin :: Dom' t e -> Origin Source # setOrigin :: Origin -> Dom' t e -> Dom' t e Source # mapOrigin :: (Origin -> Origin) -> Dom' t e -> Dom' t e Source #
LensCohesion (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods getCohesion :: Dom' t e -> Cohesion Source # setCohesion :: Cohesion -> Dom' t e -> Dom' t e Source # mapCohesion :: (Cohesion -> Cohesion) -> Dom' t e -> Dom' t e Source #
LensRelevance (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods getRelevance :: Dom' t e -> Relevance Source # setRelevance :: Relevance -> Dom' t e -> Dom' t e Source # mapRelevance :: (Relevance -> Relevance) -> Dom' t e -> Dom' t e Source #
LensQuantity (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods getQuantity :: Dom' t e -> Quantity Source # setQuantity :: Quantity -> Dom' t e -> Dom' t e Source # mapQuantity :: (Quantity -> Quantity) -> Dom' t e -> Dom' t e Source #
LensModality (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods getModality :: Dom' t e -> Modality Source # setModality :: Modality -> Dom' t e -> Dom' t e Source # mapModality :: (Modality -> Modality) -> Dom' t e -> Dom' t e Source #
LensHiding (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods getHiding :: Dom' t e -> Hiding Source # setHiding :: Hiding -> Dom' t e -> Dom' t e Source # mapHiding :: (Hiding -> Hiding) -> Dom' t e -> Dom' t e Source #
SgTel (ArgName, Dom Type) Source #
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: (ArgName, Dom Type) -> Telescope Source #
AddContext ([WithHiding Name], Dom Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([WithHiding Name], Dom Type) -> m a -> m a Source # contextSize :: ([WithHiding Name], Dom Type) -> Nat Source #
AddContext ([Name], Dom Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([Name], Dom Type) -> m a -> m a Source # contextSize :: ([Name], Dom Type) -> Nat Source #
AddContext (String, Dom Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (String, Dom Type) -> m a -> m a Source # contextSize :: (String, Dom Type) -> Nat Source #
AddContext (Name, Dom Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (Name, Dom Type) -> m a -> m a Source # contextSize :: (Name, Dom Type) -> Nat Source #
AddContext (KeepNames String, Dom Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (KeepNames String, Dom Type) -> m a -> m a Source # contextSize :: (KeepNames String, Dom Type) -> Nat Source #
(InstantiateFull t, InstantiateFull e) => InstantiateFull (Dom' t e) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Dom' t e -> ReduceM (Dom' t e) Source #
(Instantiate t, Instantiate e) => Instantiate (Dom' t e) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Dom' t e -> ReduceM (Dom' t e) Source #
ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBinding Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => (Dom r, Name) -> m TypedBinding Source #

pattern ClosedLevel :: Integer -> Level Source #

Constant level n

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

namedArgFromDom :: Dom' t a -> NamedArg a Source #

domFromArg :: Arg a -> Dom a Source #

domFromNamedArg :: NamedArg a -> Dom a Source #

defaultDom :: a -> Dom a Source #

defaultArgDom :: ArgInfo -> a -> Dom a Source #

defaultNamedArgDom :: ArgInfo -> String -> a -> Dom a Source #

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

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

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

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

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

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

clausePats :: Clause -> [Arg DeBruijnPattern] Source #

patVarNameToString :: PatVarName -> String Source #

nameToPatVarName :: Name -> PatVarName Source #

defaultPatternInfo :: PatternInfo Source #

varP :: a -> Pattern' a Source #

dotP :: Term -> Pattern' a Source #

litP :: Literal -> Pattern' a Source #

namedVarP :: PatVarName -> Named_ Pattern Source #

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

absurdP :: Int -> DeBruijnPattern Source #

Make an absurd pattern with the given de Bruijn index.

noConPatternInfo :: ConPatternInfo Source #

toConPatternInfo :: ConInfo -> ConPatternInfo Source #

Build partial ConPatternInfo from ConInfo

fromConPatternInfo :: ConPatternInfo -> ConInfo Source #

Build ConInfo from ConPatternInfo.

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

Retrieve the PatternInfo from a pattern

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

Retrieve the origin of a pattern

properlyMatching :: Pattern' a -> Bool Source #

Does the pattern perform a match that could fail?

properlyMatching' Source #

Arguments

:: Bool	Should absurd patterns count as proper match?
-> Bool	Should projection patterns count as proper match?
-> Pattern' a	The pattern.
-> Bool

isEqualityType :: EqualityView -> Bool Source #

isPathType :: PathView -> Bool Source #

isIOne :: IntervalView -> Bool Source #

absurdBody :: Abs Term Source #

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

isAbsurdBody :: Abs Term -> Bool Source #

absurdPatternName :: PatVarName Source #

isAbsurdPatternName :: PatVarName -> Bool Source #

var :: Nat -> Term Source #

An unapplied variable.

dontCare :: Term -> Term Source #

Add DontCare is it is not already a DontCare.

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

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

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

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

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

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

__DUMMY_TERM__ :: HasCallStack => Term Source #

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

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

__DUMMY_LEVEL__ :: HasCallStack => Level Source #

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

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

__DUMMY_SORT__ :: HasCallStack => Sort Source #

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

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

__DUMMY_TYPE__ :: HasCallStack => Type Source #

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

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

__DUMMY_DOM__ :: HasCallStack => Dom Type Source #

atomicLevel :: LevelAtom -> Level Source #

unreducedLevel :: Term -> Level Source #

topSort :: Type Source #

Top sort (Setomega).

sort :: Sort -> Type Source #

varSort :: Int -> Sort Source #

tmSort :: Term -> Sort Source #

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

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

levelSuc :: Level -> Level Source #

mkType :: Integer -> Sort Source #

mkProp :: Integer -> Sort Source #

isSort :: Term -> Maybe Sort Source #

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

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

A traversal for the names in a telescope.

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

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

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

telFromList :: ListTel -> Telescope Source #

Convert a list telescope to a telescope.

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

Convert a telescope to its list form.

listTel :: Lens' ListTel Telescope Source #

Lens to edit a Telescope as a list.

blockingMeta :: Blocked t -> Maybe MetaId Source #

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

notBlocked :: a -> Blocked a Source #

blocked_ :: MetaId -> Blocked_ Source #

notBlocked_ :: Blocked_ Source #

stripDontCare :: Term -> Term Source #

Removing a topmost DontCare constructor.

arity :: Type -> Nat Source #

Doesn't do any reduction.

suggests :: [Suggestion] -> String Source #

unSpine :: Term -> Term Source #

Convert top-level postfix projections into prefix projections.

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

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

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

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

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

Drop Apply constructor. (Safe)

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

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

Drop Apply constructors. (Safe)

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

Split at first non-Apply

argsFromElims :: Elims -> Args Source #

Discards Proj f entries.

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

Drop Proj constructors. (Safe)

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

prettyPrecLevelSucs :: Int -> Integer -> (Int -> Doc) -> Doc Source #

module Agda.Syntax.Abstract.Name

newtype MetaId Source #

A meta variable identifier is just a natural number.

Constructors

MetaId
Fields metaId :: Nat

Instances

Instances details

Enum MetaId Source #
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 Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: MetaId -> MetaId -> Bool # (/=) :: MetaId -> MetaId -> Bool #
Integral MetaId Source #
Instance details Defined in Agda.Syntax.Common 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 Source #
Instance details Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MetaId -> c MetaId # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MetaId # toConstr :: MetaId -> Constr # dataTypeOf :: MetaId -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MetaId) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MetaId) # gmapT :: (forall b. Data b => b -> b) -> MetaId -> MetaId # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MetaId -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MetaId -> r # gmapQ :: (forall d. Data d => d -> u) -> MetaId -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> MetaId -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId #
Num MetaId Source #
Instance details Defined in Agda.Syntax.Common Methods (+) :: MetaId -> MetaId -> MetaId # (-) :: MetaId -> MetaId -> MetaId # (*) :: MetaId -> MetaId -> MetaId # negate :: MetaId -> MetaId # abs :: MetaId -> MetaId # signum :: MetaId -> MetaId # fromInteger :: Integer -> MetaId #
Ord MetaId Source #
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 Source #
Instance details Defined in Agda.Syntax.Common Methods toRational :: MetaId -> Rational #
Show MetaId Source #	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 #
Generic MetaId Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep MetaId :: Type -> Type # Methods from :: MetaId -> Rep MetaId x # to :: Rep MetaId x -> MetaId #
NFData MetaId Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: MetaId -> () #
Hashable MetaId Source #
Instance details Defined in Agda.Syntax.Common Methods hashWithSalt :: Int -> MetaId -> Int hash :: MetaId -> Int
Pretty MetaId Source #
Instance details Defined in Agda.Syntax.Common Methods pretty :: MetaId -> Doc Source # prettyPrec :: Int -> MetaId -> Doc Source # prettyList :: [MetaId] -> Doc Source #
GetDefs MetaId Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => MetaId -> m () Source #
HasFresh MetaId Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' MetaId TCState Source # nextFresh' :: MetaId -> MetaId Source #
EmbPrj MetaId Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: MetaId -> S Int32 Source # icod_ :: MetaId -> S Int32 Source # value :: Int32 -> R MetaId Source #
PrettyTCM MetaId Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => MetaId -> m Doc Source #
UnFreezeMeta MetaId Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => MetaId -> m () Source #
IsInstantiatedMeta MetaId Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => MetaId -> m Bool Source #
FromTerm MetaId Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction MetaId) Source #
ToTerm MetaId Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (MetaId -> Term) Source # toTermR :: TCM (MetaId -> ReduceM Term) Source #
PrimTerm MetaId Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: MetaId -> TCM Term Source #
Unquote MetaId Source #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM MetaId Source #
Singleton MetaId () Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods singleton :: MetaId -> () Source #
Singleton MetaId MetaSet Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods singleton :: MetaId -> MetaSet Source #
Reify MetaId Expr Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MonadReify m => MetaId -> m Expr Source # reifyWhen :: MonadReify m => Bool -> MetaId -> m Expr Source #
type Rep MetaId Source #
Instance details Defined in Agda.Syntax.Common type Rep MetaId = D1 ('MetaData "MetaId" "Agda.Syntax.Common" "Agda-2.6.1.3-inplace" 'True) (C1 ('MetaCons "MetaId" 'PrefixI 'True) (S1 ('MetaSel ('Just "metaId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Nat)))