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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Internal

Contents

- Orphan instances

Synopsis

- 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
- data DataOrRecord' p
  - = IsData
  - | IsRecord p
- type Type = Type' Term
- pattern Type :: Level' t -> Sort' t
- data Clause = Clause {
  - clauseLHSRange :: Range
  - clauseFullRange :: Range
  - clauseTel :: Telescope
  - namedClausePats :: NAPs
  - clauseBody :: Maybe Term
  - clauseType :: Maybe (Arg Type)
  - clauseCatchall :: Catchall
  - clauseRecursive :: Maybe Bool
  - clauseUnreachable :: Maybe Bool
  - clauseEllipsis :: ExpandedEllipsis
  - clauseWhereModule :: Maybe ModuleName
  }
- data Substitution' a
  - = IdS
  - | EmptyS Impossible
  - | a :# (Substitution' a)
  - | Strengthen Impossible !Int (Substitution' a)
  - | Wk !Int (Substitution' a)
  - | Lift !Int (Substitution' a)
- data Level' t = Max !Integer [PlusLevel' t]
- data ConHead = ConHead {
  - conName :: QName
  - conDataRecord :: DataOrRecord
  - conInductive :: Induction
  - conFields :: [Arg QName]
  }
- var :: Nat -> Term
- type Pattern = Pattern' PatVarName
- litP :: Literal -> Pattern' a
- varP :: a -> Pattern' a
- 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 Dom' t e = Dom {
  - domInfo :: ArgInfo
  - domName :: Maybe NamedName
  - domIsFinite :: Bool
  - domTactic :: Maybe t
  - unDom :: e
  }
- telToList :: Tele (Dom t) -> [Dom (ArgName, t)]
- type Telescope = Tele (Dom Type)
- type Substitution = Substitution' Term
- type Dom = Dom' Term
- type Level = Level' Term
- type Elim = Elim' Term
- data Sort' t
  - = Univ Univ (Level' t)
  - | Inf Univ !Integer
  - | SizeUniv
  - | LockUniv
  - | LevelUniv
  - | IntervalUniv
  - | PiSort (Dom' t t) (Sort' t) (Abs (Sort' t))
  - | FunSort (Sort' t) (Sort' t)
  - | UnivSort (Sort' t)
  - | MetaS !MetaId [Elim' t]
  - | DefS QName [Elim' t]
  - | DummyS String
- class PatternVars a where
  - type PatternVarOut a
  - patternVars :: a -> [Arg (Either (PatternVarOut a) Term)]
- type Sort = Sort' Term
- type DataOrRecord = DataOrRecord' PatternOrCopattern
- type Args = [Arg Term]
- data Abs a
  - = Abs {
    - absName :: ArgName
    - unAbs :: a
    }
  - | NoAbs {
    - absName :: ArgName
    - unAbs :: a
    }
- class LensSort a where
  - lensSort :: Lens' a Sort
  - getSort :: a -> Sort
- type Elims = [Elim]
- arity :: Type -> Nat
- pattern Prop :: Level' t -> Sort' t
- pattern SSet :: Level' t -> Sort' t
- data PlusLevel' t = Plus !Integer t
- class TermSize a where
  - termSize :: a -> Int
  - tsize :: a -> Sum Int
- type Blocked = Blocked' Term
- type NotBlocked = NotBlocked' Term
- 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
- type NamedArgs = [NamedArg Term]
- type DataOrRecord_ = DataOrRecord' ()
- pattern IsRecord_ :: DataOrRecord_
- class LensConName a where
  - getConName :: a -> QName
  - setConName :: QName -> a -> a
  - mapConName :: (QName -> QName) -> a -> a
- type ConInfo = ConOrigin
- data Type'' t a = El {
  - _getSort :: Sort' t
  - unEl :: a
  }
- type Type' a = Type'' Term a
- data Tele a
  - = EmptyTel
  - | ExtendTel a (Abs (Tele a))
- data UnivSize
  - = USmall
  - | ULarge
- type PlusLevel = PlusLevel' Term
- type LevelAtom = Term
- newtype BraveTerm = BraveTerm {
  - unBrave :: Term
  }
- type Blocked_ = Blocked ()
- type NAPs = [NamedArg DeBruijnPattern]
- type DeBruijnPattern = Pattern' DBPatVar
- clausePats :: Clause -> [Arg DeBruijnPattern]
- type PatVarName = ArgName
- patVarNameToString :: PatVarName -> String
- nameToPatVarName :: Name -> PatVarName
- data PatternInfo = PatternInfo {
  - patOrigin :: PatOrigin
  - patAsNames :: [Name]
  }
- data PatOrigin
  - = PatOSystem
  - | PatOSplit
  - | PatOSplitArg ArgName
  - | PatOVar Name
  - | PatODot
  - | PatOWild
  - | PatOCon
  - | PatORec
  - | PatOLit
  - | PatOAbsurd
- defaultPatternInfo :: PatternInfo
- data ConPatternInfo = ConPatternInfo {
  - conPInfo :: PatternInfo
  - conPRecord :: Bool
  - conPFallThrough :: Bool
  - conPType :: Maybe (Arg Type)
  - conPLazy :: Bool
  }
- dotP :: Term -> Pattern' a
- data DBPatVar = DBPatVar {
  - dbPatVarName :: PatVarName
  - dbPatVarIndex :: !Int
  }
- namedVarP :: PatVarName -> Named_ Pattern
- namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern
- absurdP :: Int -> DeBruijnPattern
- absurdPatternName :: PatVarName
- noConPatternInfo :: ConPatternInfo
- toConPatternInfo :: ConInfo -> ConPatternInfo
- fromConPatternInfo :: ConPatternInfo -> ConInfo
- type family PatternVarOut a
- patternInfo :: Pattern' x -> Maybe PatternInfo
- patternOrigin :: Pattern' x -> Maybe PatOrigin
- type PatternSubstitution = Substitution' DeBruijnPattern
- data EqualityView
  - = EqualityViewType EqualityTypeData
  - | OtherType Type
  - | IdiomType Type
- data EqualityTypeData = EqualityTypeData {
  - _eqtRange :: Range
  - _eqtSort :: Sort
  - _eqtName :: QName
  - _eqtParams :: Args
  - _eqtType :: Arg Term
  - _eqtLhs :: Arg Term
  - _eqtRhs :: Arg Term
  }
- pattern EqualityType :: Range -> Sort -> QName -> Args -> Arg Term -> Arg Term -> Arg Term -> EqualityView
- eqtRange :: EqualityView -> Range
- eqtSort :: EqualityView -> Sort
- eqtName :: EqualityView -> QName
- eqtParams :: EqualityView -> Args
- eqtType :: EqualityView -> Arg Term
- eqtLhs :: EqualityView -> Arg Term
- eqtRhs :: EqualityView -> Arg Term
- isEqualityType :: EqualityView -> Bool
- data PathView
  - = PathType {
    - pathSort :: Sort
    - pathName :: QName
    - pathLevel :: Arg Term
    - pathType :: Arg Term
    - pathLhs :: Arg Term
    - pathRhs :: Arg Term
    }
  - | OType Type
- isPathType :: PathView -> Bool
- data IntervalView
  - = IZero
  - | IOne
  - | IMin (Arg Term) (Arg Term)
  - | IMax (Arg Term) (Arg Term)
  - | INeg (Arg Term)
  - | OTerm Term
- isIOne :: IntervalView -> Bool
- absurdBody :: Abs Term
- isAbsurdBody :: Abs Term -> Bool
- isAbsurdPatternName :: PatVarName -> Bool
- dontCare :: Term -> Term
- type DummyTermKind = String
- dummyLocName :: CallStack -> String
- dummyTermWith :: DummyTermKind -> CallStack -> Term
- __DUMMY_TERM_WITH__ :: HasCallStack => DummyTermKind -> Term
- dummyTerm :: CallStack -> Term
- __DUMMY_TERM__ :: HasCallStack => Term
- dummyLevel :: CallStack -> Level
- atomicLevel :: t -> Level' t
- __DUMMY_LEVEL__ :: HasCallStack => Level
- dummySort :: CallStack -> Sort
- __DUMMY_SORT__ :: HasCallStack => Sort
- dummyType :: CallStack -> Type
- __DUMMY_TYPE__ :: HasCallStack => Type
- dummyDom :: CallStack -> Dom Type
- __DUMMY_DOM__ :: HasCallStack => Dom Type
- pattern ClosedLevel :: Integer -> Level
- varSort :: Int -> Sort
- tmSort :: Term -> Sort
- tmSSort :: Term -> Sort
- levelPlus :: Integer -> Level -> Level
- levelSuc :: Level -> Level
- mkType :: Integer -> Sort
- mkProp :: Integer -> Sort
- mkSSet :: Integer -> Sort
- impossibleTerm :: CallStack -> Term
- isSort :: Term -> Maybe Sort
- sortUniv :: Sort' t -> Maybe Univ
- isProp :: Sort' t -> Bool
- isStrictDataSort :: Sort' t -> Bool
- propToType :: Sort' t -> Sort' t
- mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a)
- mapAbsNames :: (ArgName -> ArgName) -> Tele a -> Tele a
- replaceEmptyName :: ArgName -> Tele a -> Tele a
- type ListTel' a = [Dom (a, Type)]
- type ListTel = ListTel' ArgName
- telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope
- telFromList :: ListTel -> Telescope
- listTel :: Lens' Telescope ListTel
- class TelToArgs a where
  - telToArgs :: a -> [Arg ArgName]
- class SgTel a where
  - sgTel :: a -> Telescope
- stripDontCare :: Term -> Term
- class Suggest a where
  - suggestName :: a -> Maybe String
- data Suggestion = Suggest a => Suggestion a
- suggests :: [Suggestion] -> String
- unSpine :: Term -> Term
- unSpine' :: (ProjOrigin -> QName -> Bool) -> Term -> Term
- hasElims :: Term -> Maybe (Elims -> Term, Elims)
- type family TypeOf a
- pDom :: LensHiding a => a -> Doc -> Doc
- prettyPrecLevelSucs :: Int -> Integer -> (Int -> Doc) -> Doc
- module Agda.Syntax.Internal.Blockers
- module Agda.Syntax.Internal.Elim
- module Agda.Syntax.Internal.Univ
- module Agda.Syntax.Abstract.Name
- data MetaId = MetaId {
  - metaId :: !Word64
  - metaModule :: !ModuleNameHash
  }
- newtype ProblemId = ProblemId Nat

# Documentation

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. Dummy terms should never be used in places where they can affect type checking, so syntactic checks are free to ignore the eliminators, which are only there to ease debugging when a dummy term incorrectly leaks into a relevant position.

#### Instances

Instances details

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 PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: PlusLevel -> Doc Source # prettyPrec :: Int -> PlusLevel -> Doc Source # prettyList :: [PlusLevel] -> 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 Term Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Term -> Doc Source # prettyPrec :: Int -> Term -> Doc Source # prettyList :: [Term] -> 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 CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods pretty :: CompiledClauses -> Doc Source # prettyPrec :: Int -> CompiledClauses -> Doc Source # prettyList :: [CompiledClauses] -> Doc Source #
LensSort Sort Source # |
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' Sort Sort Source # getSort :: Sort -> Sort 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 #
TermSize Level Source # |
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Level -> Int Source # tsize :: Level -> Sum Int Source #
TermSize PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal Methods termSize :: PlusLevel -> Int Source # tsize :: PlusLevel -> 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 #
GetDefs Level Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Level -> m () Source #
GetDefs PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => PlusLevel -> m () Source #
GetDefs Sort Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Sort -> m () Source #
GetDefs Telescope Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Telescope -> m () Source #
GetDefs Term Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Term -> m () Source #
GetDefs Type Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Type -> 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 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 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 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 #
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 #
AllMetas Level Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> Level -> m Source #
AllMetas PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> PlusLevel -> m Source #
AllMetas Sort Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> Sort -> m Source #
AllMetas Term Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> Term -> m Source #
AllMetas Type Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> Type -> m Source #
NamesIn Level Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Level -> m Source #
NamesIn PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> PlusLevel -> m Source #
NamesIn Sort Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Sort -> m Source #
NamesIn Term Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Term -> m Source #
NamesIn CompiledClauses Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> CompiledClauses -> m Source #
KillRange Level Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Level Source #
KillRange PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT PlusLevel Source #
KillRange Sort Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Sort Source #
KillRange Substitution Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Substitution 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 #
Reify Level Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Level |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Level = Expr

Methods

reify :: MonadReify m => Level -> m (ReifiesTo Level) Source #

reifyWhen :: MonadReify m => Bool -> Level -> m (ReifiesTo Level) Source #

Reify Sort Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Sort |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Sort = Expr

Methods

reify :: MonadReify m => Sort -> m (ReifiesTo Sort) Source #

reifyWhen :: MonadReify m => Bool -> Sort -> m (ReifiesTo Sort) Source #

Reify Telescope Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Telescope |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Telescope = Telescope

Methods

reify :: MonadReify m => Telescope -> m (ReifiesTo Telescope) Source #

reifyWhen :: MonadReify m => Bool -> Telescope -> m (ReifiesTo Telescope) Source #

Reify Term Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Term |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Term = Expr

Methods

reify :: MonadReify m => Term -> m (ReifiesTo Term) Source #

reifyWhen :: MonadReify m => Bool -> Term -> m (ReifiesTo Term) Source #

Reify Type Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Type |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Type = Type

Methods

reify :: MonadReify m => Type -> m (ReifiesTo Type) Source #

reifyWhen :: MonadReify m => Bool -> Type -> m (ReifiesTo Type) Source #

TerSetSizeDepth ListTel Source # |
Instance details Defined in Agda.Termination.Monad Methods terSetSizeDepth :: ListTel -> TerM a -> TerM a Source #
TerSetSizeDepth Telescope Source # |
Instance details Defined in Agda.Termination.Monad Methods terSetSizeDepth :: Telescope -> TerM a -> TerM a Source #
AbsTerm Level Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> Term -> Level -> Level Source #
AbsTerm PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> Term -> PlusLevel -> PlusLevel Source #
AbsTerm Sort Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> Term -> Sort -> Sort Source #
AbsTerm Term Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> Term -> Term -> Term Source #
AbsTerm Type Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> Term -> Type -> Type Source #
EqualSy Level Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Level -> Level -> Bool Source #
EqualSy PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: PlusLevel -> PlusLevel -> Bool Source #
EqualSy Sort Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Sort -> Sort -> Bool Source #
EqualSy Term Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Term -> Term -> Bool Source #
EqualSy Type Source # | Ignores sorts.
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Type -> Type -> Bool Source #
IsPrefixOf Args Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods isPrefixOf :: Args -> Args -> Maybe Elims 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 #
CheckInternal Elims Source # |

Instance details

Defined in Agda.TypeChecking.CheckInternal

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Elims -> Comparison -> TypeOf Elims -> m Elims Source #

checkInternal :: MonadCheckInternal m => Elims -> Comparison -> TypeOf Elims -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf Elims ~ ()) => Action m -> Elims -> m Elims Source #

inferInternal :: (MonadCheckInternal m, TypeOf Elims ~ ()) => Elims -> m () Source #

CheckInternal Level Source # |

Instance details

Defined in Agda.TypeChecking.CheckInternal

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Level -> Comparison -> TypeOf Level -> m Level Source #

checkInternal :: MonadCheckInternal m => Level -> Comparison -> TypeOf Level -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf Level ~ ()) => Action m -> Level -> m Level Source #

inferInternal :: (MonadCheckInternal m, TypeOf Level ~ ()) => Level -> m () Source #

CheckInternal PlusLevel Source # |

Instance details

Defined in Agda.TypeChecking.CheckInternal

Methods

checkInternal' :: MonadCheckInternal m => Action m -> PlusLevel -> Comparison -> TypeOf PlusLevel -> m PlusLevel Source #

checkInternal :: MonadCheckInternal m => PlusLevel -> Comparison -> TypeOf PlusLevel -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf PlusLevel ~ ()) => Action m -> PlusLevel -> m PlusLevel Source #

inferInternal :: (MonadCheckInternal m, TypeOf PlusLevel ~ ()) => PlusLevel -> m () Source #

CheckInternal Sort Source # |

Instance details

Defined in Agda.TypeChecking.CheckInternal

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Sort -> Comparison -> TypeOf Sort -> m Sort Source #

checkInternal :: MonadCheckInternal m => Sort -> Comparison -> TypeOf Sort -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf Sort ~ ()) => Action m -> Sort -> m Sort Source #

inferInternal :: (MonadCheckInternal m, TypeOf Sort ~ ()) => Sort -> m () Source #

CheckInternal Term Source # |

Instance details

Defined in Agda.TypeChecking.CheckInternal

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Term -> Comparison -> TypeOf Term -> m Term Source #

checkInternal :: MonadCheckInternal m => Term -> Comparison -> TypeOf Term -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf Term ~ ()) => Action m -> Term -> m Term Source #

inferInternal :: (MonadCheckInternal m, TypeOf Term ~ ()) => Term -> m () Source #

CheckInternal Type Source # |

Instance details

Defined in Agda.TypeChecking.CheckInternal

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Type -> Comparison -> TypeOf Type -> m Type Source #

checkInternal :: MonadCheckInternal m => Type -> Comparison -> TypeOf Type -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf Type ~ ()) => Action m -> Type -> m Type Source #

inferInternal :: (MonadCheckInternal m, TypeOf Type ~ ()) => Type -> m () 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 #
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 #
PrecomputeFreeVars Level Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Level -> FV Level Source #
PrecomputeFreeVars PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: PlusLevel -> FV PlusLevel Source #
PrecomputeFreeVars Sort Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Sort -> FV Sort Source #
PrecomputeFreeVars Term Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Term -> FV Term Source #
PrecomputeFreeVars Type Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Type -> FV Type Source #
ForceNotFree Level Source # |
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Level -> m Level
ForceNotFree PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => PlusLevel -> m PlusLevel
ForceNotFree Sort Source # |
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Sort -> m Sort
ForceNotFree Term Source # |
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Term -> m Term
ForceNotFree Type Source # |
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Type -> m Type
UsableModality Level Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Level -> m Bool Source #
UsableModality Sort Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Sort -> m Bool Source #
UsableModality Term Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Term -> m Bool Source #
UsableRelevance Level Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Level -> m Bool Source #
UsableRelevance PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> PlusLevel -> m Bool Source #
UsableRelevance Sort Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Sort -> m Bool Source #
UsableRelevance Term Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Term -> m Bool Source #
NoProjectedVar Term Source # |
Instance details Defined in Agda.TypeChecking.MetaVars Methods noProjectedVar :: Term -> Either ProjectedVar () Source #
ReduceAndEtaContract Term Source # |
Instance details Defined in Agda.TypeChecking.MetaVars Methods reduceAndEtaContract :: Term -> TCM Term Source #
MentionsMeta Elim Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Elim -> Bool Source #
MentionsMeta Level Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Level -> Bool Source #
MentionsMeta PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> PlusLevel -> Bool Source #
MentionsMeta Sort Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Sort -> Bool Source #
MentionsMeta Term Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Term -> Bool Source #
MentionsMeta Type Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Type -> Bool Source #
AnyRigid Level Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Level -> tcm Bool Source #
AnyRigid PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> PlusLevel -> tcm Bool Source #
AnyRigid Sort Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Sort -> tcm Bool Source #
AnyRigid Term Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Term -> tcm Bool Source #
AnyRigid Type Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Type -> tcm Bool Source #
Occurs Elims Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Elims -> OccursM Elims Source # metaOccurs :: MetaId -> Elims -> 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 PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: PlusLevel -> OccursM PlusLevel Source # metaOccurs :: MetaId -> PlusLevel -> 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 Term Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Term -> OccursM Term Source # metaOccurs :: MetaId -> Term -> TCM () Source #
Occurs Type Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Type -> OccursM Type Source # metaOccurs :: MetaId -> Type -> TCM () 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 #
IsInstantiatedMeta Level Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: ReadTCState m => Level -> m Bool Source #
IsInstantiatedMeta PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: ReadTCState m => PlusLevel -> m Bool Source #
IsInstantiatedMeta Term Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: ReadTCState m => Term -> m Bool Source #
UnFreezeMeta Level Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Level -> m () Source #
UnFreezeMeta PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => PlusLevel -> m () Source #
UnFreezeMeta Sort Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Sort -> m () Source #
UnFreezeMeta Term Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Term -> m () Source #
UnFreezeMeta Type Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Type -> m () Source #
IsSizeType Term Source # |
Instance details Defined in Agda.TypeChecking.Monad.SizedTypes Methods isSizeType :: (HasOptions m, HasBuiltins m) => Term -> m (Maybe BoundedSize) Source #
ComputeOccurrences Level Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Level -> OccM OccurrencesBuilder Source #
ComputeOccurrences PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: PlusLevel -> OccM OccurrencesBuilder Source #
ComputeOccurrences Term Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Term -> OccM OccurrencesBuilder Source #
ComputeOccurrences Type Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Type -> OccM OccurrencesBuilder Source #
PrettyTCM Elim Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Elim -> m Doc 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 Term Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Term -> m Doc Source #
PrettyTCM Type Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Type -> m Doc Source #
PrimTerm Type Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Type -> TCM Term Source #
PrimType Type Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primType :: Type -> TCM Type Source #
ToTerm Term Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Term -> ReduceM Term) Source #
ToTerm Type Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Type -> ReduceM Term) 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 #
InstantiateFull Level Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Level -> ReduceM Level Source #
InstantiateFull PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: PlusLevel -> ReduceM PlusLevel Source #
InstantiateFull Sort Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Sort -> ReduceM Sort Source #
InstantiateFull Substitution Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Substitution -> ReduceM Substitution 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 #
IsMeta Term Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods isMeta :: Term -> Maybe MetaId Source #
Normalise Level Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Level -> ReduceM Level Source #
Normalise PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: PlusLevel -> ReduceM PlusLevel 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 #
Reduce Elim Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Elim -> ReduceM Elim Source # reduceB' :: Elim -> ReduceM (Blocked Elim) Source #
Reduce Level Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Level -> ReduceM Level Source # reduceB' :: Level -> ReduceM (Blocked Level) Source #
Reduce PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: PlusLevel -> ReduceM PlusLevel Source # reduceB' :: PlusLevel -> ReduceM (Blocked PlusLevel) 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 Term Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Term -> ReduceM Term Source # reduceB' :: Term -> ReduceM (Blocked Term) Source #
Reduce Type Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Type -> ReduceM Type Source # reduceB' :: Type -> ReduceM (Blocked Type) Source #
Simplify Level Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Level -> ReduceM Level
Simplify PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: PlusLevel -> ReduceM PlusLevel
Simplify Sort Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Sort -> ReduceM Sort
Simplify Term Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Term -> ReduceM Term
GetMatchables Term Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: Term -> [QName] Source #
EmbPrj Blocked_ Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Blocked_ -> S Word32 Source # icod_ :: Blocked_ -> S Word32 Source # value :: Word32 -> R Blocked_ Source #
EmbPrj Level Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Level -> S Word32 Source # icod_ :: Level -> S Word32 Source # value :: Word32 -> R Level Source #
EmbPrj NotBlocked Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: NotBlocked -> S Word32 Source # icod_ :: NotBlocked -> S Word32 Source # value :: Word32 -> R NotBlocked Source #
EmbPrj PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: PlusLevel -> S Word32 Source # icod_ :: PlusLevel -> S Word32 Source # value :: Word32 -> R PlusLevel Source #
EmbPrj Sort Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Sort -> S Word32 Source # icod_ :: Sort -> S Word32 Source # value :: Word32 -> R Sort Source #
EmbPrj Term Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Term -> S Word32 Source # icod_ :: Term -> S Word32 Source # value :: Word32 -> R Term Source #
EmbPrj CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: CompiledClauses -> S Word32 Source # icod_ :: CompiledClauses -> S Word32 Source # value :: Word32 -> R CompiledClauses 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 #
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 Term Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Term -> Term Source #
Abstract Type Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Type -> Type 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 #
Subst Term Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Term |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Term = Term

Methods

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

Subst Boundary Source # | Substitution into a `Boundary` a priori creates a `TmBoundary` which we convert back via `varBoundary`. A priori, this is a partial operation.

Instance details

Defined in Agda.TypeChecking.Telescope

Associated Types

type SubstArg Boundary |
Instance details Defined in Agda.TypeChecking.Telescope type SubstArg Boundary = Term

Methods

applySubst :: Substitution' (SubstArg Boundary) -> Boundary -> Boundary Source #

Subst TmBoundary Source # |

Instance details

Defined in Agda.TypeChecking.Telescope

Associated Types

type SubstArg TmBoundary |
Instance details Defined in Agda.TypeChecking.Telescope type SubstArg TmBoundary = Term

Methods

applySubst :: Substitution' (SubstArg TmBoundary) -> TmBoundary -> TmBoundary 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 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 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 #
SynEq Level Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Level -> Level -> SynEqM (Level, Level) synEq' :: Level -> Level -> SynEqM (Level, Level)
SynEq PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: PlusLevel -> PlusLevel -> SynEqM (PlusLevel, PlusLevel) synEq' :: PlusLevel -> PlusLevel -> SynEqM (PlusLevel, PlusLevel)
SynEq Sort Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Sort -> Sort -> SynEqM (Sort, Sort) synEq' :: Sort -> Sort -> SynEqM (Sort, Sort)
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)
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)
PiApplyM Term Source # |
Instance details Defined in Agda.TypeChecking.Telescope Methods piApplyM' :: (MonadReduce m, HasBuiltins m) => m Empty -> Type -> Term -> m Type Source # piApplyM :: (MonadReduce m, HasBuiltins m) => Type -> Term -> m Type Source #
NFData Level Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Level -> () Source #
NFData PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: PlusLevel -> () Source #
NFData Sort Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Sort -> () Source #
NFData Term Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Term -> () Source #
NFData Type Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Type -> () Source #
Show Term Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Term -> ShowS Source # show :: Term -> String Source # showList :: [Term] -> ShowS Source #
Eq Level Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Level -> Level -> Bool Source # (/=) :: Level -> Level -> Bool Source #
Eq NotBlocked Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: NotBlocked -> NotBlocked -> Bool Source # (/=) :: NotBlocked -> NotBlocked -> Bool Source #
Eq PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: PlusLevel -> PlusLevel -> Bool Source # (/=) :: PlusLevel -> PlusLevel -> Bool Source #
Eq Sort Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Sort -> Sort -> Bool Source # (/=) :: Sort -> Sort -> Bool Source #
Eq Substitution Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Substitution -> Substitution -> Bool Source # (/=) :: Substitution -> Substitution -> Bool Source #
Eq Term Source # | Syntactic `Term` equality, ignores stuff below `DontCare` and sharing.
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Term -> Term -> Bool Source # (/=) :: Term -> Term -> Bool Source #
Eq SingleLevel Source # |
Instance details Defined in Agda.TypeChecking.Level Methods (==) :: SingleLevel -> SingleLevel -> Bool Source # (/=) :: SingleLevel -> SingleLevel -> Bool Source #
Ord Level Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Level -> Level -> Ordering Source # (<) :: Level -> Level -> Bool Source # (<=) :: Level -> Level -> Bool Source # (>) :: Level -> Level -> Bool Source # (>=) :: Level -> Level -> Bool Source # max :: Level -> Level -> Level Source # min :: Level -> Level -> Level Source #
Ord PlusLevel Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Methods

compare :: PlusLevel -> PlusLevel -> Ordering Source #

(<) :: PlusLevel -> PlusLevel -> Bool Source #

(<=) :: PlusLevel -> PlusLevel -> Bool Source #

(>) :: PlusLevel -> PlusLevel -> Bool Source #

(>=) :: PlusLevel -> PlusLevel -> Bool Source #

max :: PlusLevel -> PlusLevel -> PlusLevel Source #

min :: PlusLevel -> PlusLevel -> PlusLevel Source #

Ord Sort Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Sort -> Sort -> Ordering Source # (<) :: Sort -> Sort -> Bool Source # (<=) :: Sort -> Sort -> Bool Source # (>) :: Sort -> Sort -> Bool Source # (>=) :: Sort -> Sort -> Bool Source # max :: Sort -> Sort -> Sort Source # min :: Sort -> Sort -> Sort Source #
Ord Substitution Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Methods

compare :: Substitution -> Substitution -> Ordering Source #

(<) :: Substitution -> Substitution -> Bool Source #

(<=) :: Substitution -> Substitution -> Bool Source #

(>) :: Substitution -> Substitution -> Bool Source #

(>=) :: Substitution -> Substitution -> Bool Source #

max :: Substitution -> Substitution -> Substitution Source #

min :: Substitution -> Substitution -> Substitution Source #

Ord Term Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Term -> Term -> Ordering Source # (<) :: Term -> Term -> Bool Source # (<=) :: Term -> Term -> Bool Source # (>) :: Term -> Term -> Bool Source # (>=) :: Term -> Term -> Bool Source # max :: Term -> Term -> Term Source # min :: Term -> Term -> Term Source #
Match NLPSort Sort Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Context -> TypeOf Sort -> NLPSort -> Sort -> NLM () Source #
Match NLPType Type Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Context -> TypeOf Type -> NLPType -> Type -> NLM () Source #
Match NLPat Level Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Context -> TypeOf Level -> NLPat -> Level -> NLM () Source #
Match NLPat Term Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Context -> TypeOf Term -> NLPat -> Term -> NLM () Source #
NLPatToTerm Nat Term Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: PureTCM m => Nat -> m Term Source #
NLPatToTerm NLPSort Sort Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: PureTCM m => NLPSort -> m Sort Source #
NLPatToTerm NLPType Type Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: PureTCM m => NLPType -> m Type Source #
NLPatToTerm NLPat Level Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: PureTCM m => NLPat -> m Level Source #
NLPatToTerm NLPat Term Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: PureTCM m => NLPat -> m Term Source #
PatternFrom Level NLPat Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> TypeOf Level -> Level -> TCM NLPat Source #
PatternFrom Sort NLPSort Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> TypeOf Sort -> Sort -> TCM NLPSort Source #
PatternFrom Term NLPat Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> TypeOf Term -> Term -> TCM NLPat Source #
PatternFrom Type NLPType Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> TypeOf Type -> Type -> TCM NLPType Source #
MonadError Blocked_ NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods throwError :: Blocked_ -> NLM a Source # catchError :: NLM a -> (Blocked_ -> NLM a) -> NLM 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 #
PatternFrom Elims [Elim' NLPat] Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> TypeOf Elims -> Elims -> TCM [Elim' NLPat] Source #
Pretty a => Pretty (Blocked a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Blocked a -> Doc Source # prettyPrec :: Int -> Blocked a -> Doc Source # prettyList :: [Blocked a] -> Doc 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 #
LensSort a => LensSort (Dom a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' (Dom a) Sort Source # getSort :: Dom a -> Sort Source #
LensSort (Type' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' (Type' a) Sort Source # getSort :: Type' a -> Sort Source #
SgTel (Dom Type) Source # |
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom Type -> Telescope Source #
SgTel (Dom (ArgName, Type)) Source # |
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom (ArgName, Type) -> Telescope Source #
GetDefs a => GetDefs (Dom a) Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Dom a -> m () 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 #
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 #
NamesIn a => NamesIn (Type' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Type' a -> m Source #
KillRange a => KillRange (Blocked a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Blocked a) Source #
KillRange a => KillRange (Type' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Type' a) Source #
Reify i => Reify (Dom i) Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Dom i) |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (Dom i) = Arg (ReifiesTo i)

Methods

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

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

AbsTerm a => AbsTerm (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> Term -> Dom a -> 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 #
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 #
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 #
PrecomputeFreeVars a => PrecomputeFreeVars (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Dom a -> FV (Dom a) Source #
(Reduce a, ForceNotFree a, TermSubst 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 :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Dom a -> m Bool Source #
UsableRelevance a => UsableModality (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Type' a -> m Bool Source #
UsableRelevance a => UsableRelevance (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Dom a -> m Bool Source #
UsableRelevance a => UsableRelevance (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Type' a -> m Bool Source #
MentionsMeta t => MentionsMeta (Dom t) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Dom t -> Bool Source #
AnyRigid a => AnyRigid (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Dom a -> tcm Bool Source #
Occurs (Abs Term) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Abs Term -> OccursM (Abs Term) Source # metaOccurs :: MetaId -> Abs Term -> TCM () Source #
Occurs (Abs Type) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Abs Type -> OccursM (Abs Type) Source # metaOccurs :: MetaId -> Abs Type -> TCM () 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 #
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 (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 (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 (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 #
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 #
ComputeOccurrences a => ComputeOccurrences (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Dom a -> OccM OccurrencesBuilder Source #
PrettyTCM (Arg Term) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Arg Term -> m Doc Source #
PrettyTCM (Arg Type) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Arg Type -> m Doc Source #
PrettyTCM (NamedArg Term) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedArg Term -> m Doc Source #
PrettyTCM (Named_ Term) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Named_ Term -> m Doc Source #
PrettyTCM a => PrettyTCM (Blocked a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Blocked a -> m Doc Source #
PrettyTCM (Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Dom Type -> m Doc Source #
PrettyTCM (Type' NLPat) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Type' NLPat -> m Doc Source #
ToTerm (Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Dom Type -> ReduceM Term) Source #
Instantiate a => Instantiate (Blocked a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Blocked a -> ReduceM (Blocked a) Source #
Instantiate t => Instantiate (Type' t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Type' t -> ReduceM (Type' t) 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 (Dom t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Dom t -> ReduceM (Dom t) Source #
Normalise t => Normalise (Type' t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Type' t -> ReduceM (Type' 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 #
Simplify t => Simplify (Dom t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Dom t -> ReduceM (Dom t)
Simplify t => Simplify (Type' t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Type' t -> ReduceM (Type' t)
GetMatchables a => GetMatchables (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: Dom a -> [QName] Source #
EmbPrj a => EmbPrj (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Dom a -> S Word32 Source # icod_ :: Dom a -> S Word32 Source # value :: Word32 -> R (Dom a) Source #
EmbPrj a => EmbPrj (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Type' a -> S Word32 Source # icod_ :: Type' a -> S Word32 Source # value :: Word32 -> R (Type' 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 #
Subst a => Subst (Blocked a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Blocked a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Blocked a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Blocked a)) -> Blocked a -> Blocked a 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)
Unquote a => Unquote (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM (Dom a) Source #
NFData e => NFData (Dom e) Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Dom e -> () Source #
Eq t => Eq (Blocked t) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Blocked t -> Blocked t -> Bool Source # (/=) :: Blocked t -> Blocked t -> Bool 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 Source # (/=) :: Type' a -> Type' a -> Bool Source #
Ord a => Ord (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Dom a -> Dom a -> Ordering Source # (<) :: Dom a -> Dom a -> Bool Source # (<=) :: Dom a -> Dom a -> Bool Source # (>) :: Dom a -> Dom a -> Bool Source # (>=) :: Dom a -> Dom a -> Bool Source # max :: Dom a -> Dom a -> Dom a Source # min :: Dom a -> Dom a -> Dom a Source #
Ord a => Ord (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Type' a -> Type' a -> Ordering Source # (<) :: Type' a -> Type' a -> Bool Source # (<=) :: Type' a -> Type' a -> Bool Source # (>) :: Type' a -> Type' a -> Bool Source # (>=) :: Type' a -> Type' a -> Bool Source # max :: Type' a -> Type' a -> Type' a Source # min :: Type' a -> Type' a -> Type' a Source #
Match [Elim' NLPat] Elims Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Context -> TypeOf Elims -> [Elim' NLPat] -> Elims -> NLM () 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 #
Match a b => Match (Dom a) (Dom b) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Context -> TypeOf (Dom b) -> Dom a -> Dom b -> NLM () Source #
NLPatToTerm p a => NLPatToTerm (Dom p) (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: PureTCM m => Dom p -> m (Dom a) Source #
PatternFrom a b => PatternFrom (Dom a) (Dom b) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> TypeOf (Dom a) -> Dom a -> TCM (Dom b) Source #
SgTel (ArgName, Dom Type) Source # |
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: (ArgName, Dom Type) -> Telescope Source #
(ToAbstract r, AbsOfRef r ~ Expr) => ToAbstract (Dom r, Name) Source # |

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Dom r, Name) |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Dom r, Name) = TypedBinding

Methods

toAbstract :: MonadReflectedToAbstract m => (Dom r, Name) -> m (AbsOfRef (Dom r, Name)) 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 #
AddContext (List1 Name, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 Name, Dom Type) -> m a -> m a Source # contextSize :: (List1 Name, Dom Type) -> Nat Source #
AddContext (List1 (Arg Name), Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (Arg Name), Type) -> m a -> m a Source # contextSize :: (List1 (Arg Name), Type) -> Nat Source #
AddContext (List1 (NamedArg Name), Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (NamedArg Name), Type) -> m a -> m a Source # contextSize :: (List1 (NamedArg Name), Type) -> Nat Source #
AddContext (List1 (WithHiding Name), Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (WithHiding Name), Dom Type) -> m a -> m a Source # contextSize :: (List1 (WithHiding Name), Dom Type) -> Nat Source #
AddContext (Text, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (Text, Dom Type) -> m a -> m a Source # contextSize :: (Text, 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 ([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 ([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 ([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 #
type TypeOf Elims Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf Elims = (Type, Elims -> Term)
type TypeOf Level Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf Level = ()
type TypeOf PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf PlusLevel = ()
type TypeOf Sort Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf Sort = ()
type TypeOf Term Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf Term = Type
type TypeOf Type Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf Type = ()
type ReifiesTo Level Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Level = Expr
type ReifiesTo Sort Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Sort = Expr
type ReifiesTo Telescope Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Telescope = Telescope
type ReifiesTo Term Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Term = Expr
type ReifiesTo Type Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Type = Type
type SubstArg Term Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Term = Term
type SubstArg Boundary Source # |
Instance details Defined in Agda.TypeChecking.Telescope type SubstArg Boundary = Term
type SubstArg TmBoundary Source # |
Instance details Defined in Agda.TypeChecking.Telescope type SubstArg TmBoundary = Term
type TypeOf (Abs Term) Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf (Abs Term) = (Dom Type, Abs Type)
type TypeOf (Abs Type) Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf (Abs Type) = Dom Type
type TypeOf (Dom a) Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf (Dom a) = TypeOf a
type TypeOf [PlusLevel] Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf [PlusLevel] = ()
type ReifiesTo (Dom i) Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (Dom i) = Arg (ReifiesTo i)
type SubstArg (Blocked a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Blocked a) = SubstArg a
type AbsOfRef (Dom r, Name) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Dom r, Name) = TypedBinding

data DataOrRecord' p Source #

Constructors

IsData |
IsRecord p |

#### Instances

Instances details

CopatternMatchingAllowed DataOrRecord Source # |
Instance details Defined in Agda.Syntax.Internal Methods copatternMatchingAllowed :: DataOrRecord -> Bool Source #
PatternMatchingAllowed DataOrRecord Source # |
Instance details Defined in Agda.Syntax.Internal Methods patternMatchingAllowed :: DataOrRecord -> Bool Source #
KillRange DataOrRecord Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT DataOrRecord Source #
PrettyTCM DataOrRecord_ Source # |
Instance details Defined in Agda.TypeChecking.Pretty.Warning Methods prettyTCM :: MonadPretty m => DataOrRecord_ -> m Doc Source #
EmbPrj DataOrRecord Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DataOrRecord -> S Word32 Source # icod_ :: DataOrRecord -> S Word32 Source # value :: Word32 -> R DataOrRecord Source #
NFData a => NFData (DataOrRecord' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: DataOrRecord' a -> () Source #
Generic (DataOrRecord' p) Source # |

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep (DataOrRecord' p) |
Instance details Defined in Agda.Syntax.Internal type Rep (DataOrRecord' p) = D1 ('MetaData "DataOrRecord'" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "IsData" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsRecord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 p)))

Methods

from :: DataOrRecord' p -> Rep (DataOrRecord' p) x Source #

to :: Rep (DataOrRecord' p) x -> DataOrRecord' p Source #

Show p => Show (DataOrRecord' p) Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> DataOrRecord' p -> ShowS Source # show :: DataOrRecord' p -> String Source # showList :: [DataOrRecord' p] -> ShowS Source #
Eq p => Eq (DataOrRecord' p) Source # |
Instance details Defined in Agda.Syntax.Internal Methods (==) :: DataOrRecord' p -> DataOrRecord' p -> Bool Source # (/=) :: DataOrRecord' p -> DataOrRecord' p -> Bool Source #
type Rep (DataOrRecord' p) Source # |
Instance details Defined in Agda.Syntax.Internal type Rep (DataOrRecord' p) = D1 ('MetaData "DataOrRecord'" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "IsData" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsRecord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 p)))

type Type = Type' Term Source #

pattern Type :: Level' t -> Sort' t Source #

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

  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?

- clauseWhereModule :: Maybe ModuleName

  Keeps track of the module name associate with the clause's where clause.

#### Instances

Instances details

Pretty Clause Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Clause -> Doc Source # prettyPrec :: Int -> Clause -> Doc Source # prettyList :: [Clause] -> Doc Source #
GetDefs Clause Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Clause -> m () Source #
NamesIn Clause Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> 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 #
HasRange Clause Source # |
Instance details Defined in Agda.Syntax.Internal Methods getRange :: Clause -> Range Source #
KillRange Clause Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Clause 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 #
Free Clause Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Clause -> FreeM a c Source #
Occurs Clause Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Clause -> OccursM Clause Source # metaOccurs :: MetaId -> Clause -> TCM () Source #
ComputeOccurrences Clause Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Clause -> OccM OccurrencesBuilder Source #
PrettyTCM Clause Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Clause -> m Doc Source #
NormaliseProjP Clause Source # |
Instance details Defined in Agda.TypeChecking.Records Methods normaliseProjP :: HasConstInfo m => Clause -> m Clause 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 #
EmbPrj Clause Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Clause -> S Word32 Source # icod_ :: Clause -> S Word32 Source # value :: Word32 -> R Clause 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 #
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 #
NFData Clause Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Clause -> () Source #
Generic Clause Source # |

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep Clause |

Instance details

Defined in Agda.Syntax.Internal

type Rep Clause = D1 ('MetaData "Clause" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Clause" 'PrefixI 'True) (((S1 ('MetaSel ('Just "clauseLHSRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "clauseFullRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :*: (S1 ('MetaSel ('Just "clauseTel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope) :*: (S1 ('MetaSel ('Just "namedClausePats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NAPs) :*: S1 ('MetaSel ('Just "clauseBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Term))))) :*: ((S1 ('MetaSel ('Just "clauseType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Arg Type))) :*: (S1 ('MetaSel ('Just "clauseCatchall") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Catchall) :*: S1 ('MetaSel ('Just "clauseRecursive") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool)))) :*: (S1 ('MetaSel ('Just "clauseUnreachable") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool)) :*: (S1 ('MetaSel ('Just "clauseEllipsis") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExpandedEllipsis) :*: S1 ('MetaSel ('Just "clauseWhereModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModuleName)))))))

Methods

from :: Clause -> Rep Clause x Source #

to :: Rep Clause x -> Clause Source #

Show Clause Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Clause -> ShowS Source # show :: Clause -> String Source # showList :: [Clause] -> ShowS 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 #
Reify (QNamed Clause) Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (QNamed Clause) |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (QNamed Clause) = Clause

Methods

reify :: MonadReify m => QNamed Clause -> m (ReifiesTo (QNamed Clause)) Source #

reifyWhen :: MonadReify m => Bool -> QNamed Clause -> m (ReifiesTo (QNamed Clause)) Source #

PrettyTCM (QNamed Clause) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => QNamed Clause -> m Doc Source #
type Rep Clause Source # |

Instance details

Defined in Agda.Syntax.Internal

type Rep Clause = D1 ('MetaData "Clause" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Clause" 'PrefixI 'True) (((S1 ('MetaSel ('Just "clauseLHSRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "clauseFullRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :*: (S1 ('MetaSel ('Just "clauseTel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope) :*: (S1 ('MetaSel ('Just "namedClausePats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NAPs) :*: S1 ('MetaSel ('Just "clauseBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Term))))) :*: ((S1 ('MetaSel ('Just "clauseType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Arg Type))) :*: (S1 ('MetaSel ('Just "clauseCatchall") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Catchall) :*: S1 ('MetaSel ('Just "clauseRecursive") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool)))) :*: (S1 ('MetaSel ('Just "clauseUnreachable") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool)) :*: (S1 ('MetaSel ('Just "clauseEllipsis") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExpandedEllipsis) :*: S1 ('MetaSel ('Just "clauseWhereModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModuleName)))))))

type ReifiesTo (QNamed Clause) Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (QNamed Clause) = Clause

data Substitution' a Source #

Substitutions.

Constructors

IdS | Identity substitution. `Γ ⊢ IdS : Γ`
EmptyS Impossible | 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 Impossible !Int (Substitution' a)

Strengthening substitution. First argument is `IMPOSSIBLE`. In `'Strengthen err n ρ` the number `n` must be non-negative. This substitution should only be applied to values `t` for which none of the variables `0` up to `n - 1` are free in `t[ρ]`, and in that case `n` is subtracted from all free de Bruijn indices in `t[ρ]`. Γ ⊢ ρ : Δ |Θ| = n --------------------------- Γ ⊢ Strengthen n ρ : Δ, Θ @

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

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 #
Functor Substitution' Source # |
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Substitution' a -> Substitution' b Source # (<$) :: a -> Substitution' b -> Substitution' a Source #
Foldable Substitution' Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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

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

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

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

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

null :: Substitution' a -> Bool Source #

length :: Substitution' a -> Int Source #

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

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

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

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

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

Traversable Substitution' Source # |
Instance details Defined in Agda.Syntax.Internal Methods traverse :: Applicative f => (a -> f b) -> Substitution' a -> f (Substitution' b) Source # sequenceA :: Applicative f => Substitution' (f a) -> f (Substitution' a) Source # mapM :: Monad m => (a -> m b) -> Substitution' a -> m (Substitution' b) Source # sequence :: Monad m => Substitution' (m a) -> m (Substitution' a) Source #
Eq Substitution Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Substitution -> Substitution -> Bool Source # (/=) :: Substitution -> Substitution -> Bool Source #
Ord Substitution Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Methods

compare :: Substitution -> Substitution -> Ordering Source #

(<) :: Substitution -> Substitution -> Bool Source #

(<=) :: Substitution -> Substitution -> Bool Source #

(>) :: Substitution -> Substitution -> Bool Source #

(>=) :: Substitution -> Substitution -> Bool Source #

max :: Substitution -> Substitution -> Substitution Source #

min :: Substitution -> Substitution -> Substitution 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 #
NamesIn a => NamesIn (Substitution' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Substitution' a -> m Source #
(Pretty a, PrettyTCM a, EndoSubst a) => PrettyTCM (Substitution' a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Substitution' a -> m Doc Source #
EmbPrj a => EmbPrj (Substitution' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Substitution' a -> S Word32 Source # icod_ :: Substitution' a -> S Word32 Source # value :: Word32 -> R (Substitution' a) Source #
EndoSubst a => Subst (Substitution' a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Substitution' a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Substitution' a) = a

Methods

applySubst :: Substitution' (SubstArg (Substitution' a)) -> Substitution' a -> Substitution' a Source #

Null (Substitution' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods empty :: Substitution' a Source # null :: Substitution' a -> Bool Source #
NFData a => NFData (Substitution' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Substitution' a -> () Source #
Generic (Substitution' a) Source # |

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep (Substitution' a) |

Instance details

Defined in Agda.Syntax.Internal

type Rep (Substitution' a) = D1 ('MetaData "Substitution'" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((C1 ('MetaCons "IdS" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "EmptyS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible)) :+: C1 ('MetaCons ":#" ('InfixI 'RightAssociative 4) 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))))) :+: (C1 ('MetaCons "Strengthen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a)))) :+: (C1 ('MetaCons "Wk" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))) :+: C1 ('MetaCons "Lift" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))))))

Methods

from :: Substitution' a -> Rep (Substitution' a) x Source #

to :: Rep (Substitution' a) x -> Substitution' a Source #

Show a => Show (Substitution' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Substitution' a -> ShowS Source # show :: Substitution' a -> String Source # showList :: [Substitution' a] -> ShowS Source #
type SubstArg (Substitution' a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Substitution' a) = a
type Rep (Substitution' a) Source # |

Instance details

Defined in Agda.Syntax.Internal

type Rep (Substitution' a) = D1 ('MetaData "Substitution'" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((C1 ('MetaCons "IdS" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "EmptyS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible)) :+: C1 ('MetaCons ":#" ('InfixI 'RightAssociative 4) 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))))) :+: (C1 ('MetaCons "Strengthen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a)))) :+: (C1 ('MetaCons "Wk" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))) :+: C1 ('MetaCons "Lift" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))))))

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

Pretty Level Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Level -> Doc Source # prettyPrec :: Int -> Level -> Doc Source # prettyList :: [Level] -> Doc Source #
TermSize Level Source # |
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Level -> Int Source # tsize :: Level -> Sum Int Source #
GetDefs Level Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Level -> 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 #
AllMetas Level Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> Level -> m Source #
NamesIn Level Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Level -> m Source #
KillRange Level Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Level Source #
Reify Level Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Level |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Level = Expr

Methods

reify :: MonadReify m => Level -> m (ReifiesTo Level) Source #

reifyWhen :: MonadReify m => Bool -> Level -> m (ReifiesTo Level) Source #

AbsTerm Level Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> Term -> Level -> Level Source #
EqualSy Level Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Level -> Level -> Bool Source #
CheckInternal Level Source # |

Instance details

Defined in Agda.TypeChecking.CheckInternal

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Level -> Comparison -> TypeOf Level -> m Level Source #

checkInternal :: MonadCheckInternal m => Level -> Comparison -> TypeOf Level -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf Level ~ ()) => Action m -> Level -> m Level Source #

inferInternal :: (MonadCheckInternal m, TypeOf Level ~ ()) => Level -> m () Source #

Free Level Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Level -> FreeM a c Source #
PrecomputeFreeVars Level Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Level -> FV Level Source #
ForceNotFree Level Source # |
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Level -> m Level
UsableModality Level Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Level -> m Bool Source #
UsableRelevance Level Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Level -> m Bool Source #
MentionsMeta Level Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Level -> Bool Source #
AnyRigid Level Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM 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 #
IsInstantiatedMeta Level Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: ReadTCState m => Level -> m Bool Source #
UnFreezeMeta Level Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Level -> m () Source #
ComputeOccurrences Level Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Level -> OccM OccurrencesBuilder Source #
PrettyTCM Level Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Level -> m Doc Source #
Instantiate Level Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Level -> ReduceM Level 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 #
Reduce Level Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Level -> ReduceM Level Source # reduceB' :: Level -> ReduceM (Blocked Level) Source #
Simplify Level Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Level -> ReduceM Level
EmbPrj Level Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Level -> S Word32 Source # icod_ :: Level -> S Word32 Source # value :: Word32 -> R Level 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 #
SynEq Level Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Level -> Level -> SynEqM (Level, Level) synEq' :: Level -> Level -> SynEqM (Level, Level)
NFData Level Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Level -> () Source #
Functor Level' Source # |
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Level' a -> Level' b Source # (<$) :: a -> Level' b -> Level' a Source #
Foldable Level' Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => Level' m -> m Source #

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

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

foldr :: (a -> b -> b) -> b -> Level' a -> b Source #

foldr' :: (a -> b -> b) -> b -> Level' a -> b Source #

foldl :: (b -> a -> b) -> b -> Level' a -> b Source #

foldl' :: (b -> a -> b) -> b -> Level' a -> b Source #

foldr1 :: (a -> a -> a) -> Level' a -> a Source #

foldl1 :: (a -> a -> a) -> Level' a -> a Source #

toList :: Level' a -> [a] Source #

null :: Level' a -> Bool Source #

length :: Level' a -> Int Source #

elem :: Eq a => a -> Level' a -> Bool Source #

maximum :: Ord a => Level' a -> a Source #

minimum :: Ord a => Level' a -> a Source #

sum :: Num a => Level' a -> a Source #

product :: Num a => Level' a -> a Source #

Traversable Level' Source # |
Instance details Defined in Agda.Syntax.Internal Methods traverse :: Applicative f => (a -> f b) -> Level' a -> f (Level' b) Source # sequenceA :: Applicative f => Level' (f a) -> f (Level' a) Source # mapM :: Monad m => (a -> m b) -> Level' a -> m (Level' b) Source # sequence :: Monad m => Level' (m a) -> m (Level' a) Source #
Eq Level Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Level -> Level -> Bool Source # (/=) :: Level -> Level -> Bool Source #
Ord Level Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Level -> Level -> Ordering Source # (<) :: Level -> Level -> Bool Source # (<=) :: Level -> Level -> Bool Source # (>) :: Level -> Level -> Bool Source # (>=) :: Level -> Level -> Bool Source # max :: Level -> Level -> Level Source # min :: Level -> Level -> Level Source #
Match NLPat Level Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Context -> TypeOf Level -> NLPat -> Level -> NLM () Source #
NLPatToTerm NLPat Level Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: PureTCM m => NLPat -> m Level Source #
PatternFrom Level NLPat Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> TypeOf Level -> Level -> TCM NLPat Source #
IsMeta a => IsMeta (Level' a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods isMeta :: Level' a -> Maybe MetaId Source #
Subst a => Subst (Level' a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Level' a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Level' a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Level' a)) -> Level' a -> Level' a Source #

Show t => Show (Level' t) Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Level' t -> ShowS Source # show :: Level' t -> String Source # showList :: [Level' t] -> ShowS Source #
type TypeOf Level Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf Level = ()
type ReifiesTo Level Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Level = Expr
type SubstArg (Level' a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Level' a) = SubstArg a

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.

- conDataRecord :: DataOrRecord

  Data or record constructor?

- conInductive :: Induction

  Record constructors can be coinductive.

- conFields :: [Arg QName]

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

#### Instances

Instances details

CopatternMatchingAllowed ConHead Source # |
Instance details Defined in Agda.Syntax.Internal Methods copatternMatchingAllowed :: ConHead -> Bool Source #
Pretty ConHead Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: ConHead -> Doc Source # prettyPrec :: Int -> ConHead -> Doc Source # prettyList :: [ConHead] -> Doc 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 #
NamesIn ConHead Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> ConHead -> m Source #
HasRange ConHead Source # |
Instance details Defined in Agda.Syntax.Internal Methods getRange :: ConHead -> Range 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 #
PrettyTCM ConHead Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ConHead -> m Doc Source #
InstantiateFull ConHead Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ConHead -> ReduceM ConHead Source #
EmbPrj ConHead Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ConHead -> S Word32 Source # icod_ :: ConHead -> S Word32 Source # value :: Word32 -> R ConHead Source #
NFData ConHead Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: ConHead -> () Source #
Generic ConHead Source # |

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep ConHead |

Instance details

Defined in Agda.Syntax.Internal

type Rep ConHead = D1 ('MetaData "ConHead" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "ConHead" 'PrefixI 'True) ((S1 ('MetaSel ('Just "conName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "conDataRecord") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataOrRecord)) :*: (S1 ('MetaSel ('Just "conInductive") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Induction) :*: S1 ('MetaSel ('Just "conFields") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Arg QName]))))

Methods

from :: ConHead -> Rep ConHead x Source #

to :: Rep ConHead x -> ConHead Source #

Show ConHead Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> ConHead -> ShowS Source # show :: ConHead -> String Source # showList :: [ConHead] -> ShowS Source #
Eq ConHead Source # |
Instance details Defined in Agda.Syntax.Internal Methods (==) :: ConHead -> ConHead -> Bool Source # (/=) :: ConHead -> ConHead -> Bool Source #
Ord ConHead Source # |
Instance details Defined in Agda.Syntax.Internal Methods compare :: ConHead -> ConHead -> Ordering Source # (<) :: ConHead -> ConHead -> Bool Source # (<=) :: ConHead -> ConHead -> Bool Source # (>) :: ConHead -> ConHead -> Bool Source # (>=) :: ConHead -> ConHead -> Bool Source # max :: ConHead -> ConHead -> ConHead Source # min :: ConHead -> ConHead -> ConHead Source #
type Rep ConHead Source # |

Instance details

Defined in Agda.Syntax.Internal

type Rep ConHead = D1 ('MetaData "ConHead" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "ConHead" 'PrefixI 'True) ((S1 ('MetaSel ('Just "conName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "conDataRecord") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataOrRecord)) :*: (S1 ('MetaSel ('Just "conInductive") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Induction) :*: S1 ('MetaSel ('Just "conFields") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Arg QName]))))

var :: Nat -> Term Source #

An unapplied variable.

type Pattern Source #

Arguments

= Pattern' PatVarName | The `PatVarName` is a name suggestion.

litP :: Literal -> Pattern' a Source #

varP :: a -> Pattern' a Source #

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

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 #
Reduce DeBruijnPattern Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: DeBruijnPattern -> ReduceM DeBruijnPattern Source # reduceB' :: DeBruijnPattern -> ReduceM (Blocked DeBruijnPattern) Source #
Subst DeBruijnPattern Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg DeBruijnPattern |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg DeBruijnPattern = DeBruijnPattern

Methods

applySubst :: Substitution' (SubstArg DeBruijnPattern) -> DeBruijnPattern -> DeBruijnPattern Source #

Subst Pattern Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Pattern |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Pattern = Term

Methods

applySubst :: Substitution' (SubstArg Pattern) -> Pattern -> Pattern Source #

Subst SplitPattern Source # |

Instance details

Defined in Agda.TypeChecking.Coverage.Match

Associated Types

type SubstArg SplitPattern |
Instance details Defined in Agda.TypeChecking.Coverage.Match type SubstArg SplitPattern = SplitPattern

Methods

applySubst :: Substitution' (SubstArg SplitPattern) -> SplitPattern -> SplitPattern Source #

Functor Pattern' Source # |
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Pattern' a -> Pattern' b Source # (<$) :: a -> Pattern' b -> Pattern' a Source #
Foldable Pattern' Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => Pattern' m -> m Source #

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

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

foldr :: (a -> b -> b) -> b -> Pattern' a -> b Source #

foldr' :: (a -> b -> b) -> b -> Pattern' a -> b Source #

foldl :: (b -> a -> b) -> b -> Pattern' a -> b Source #

foldl' :: (b -> a -> b) -> b -> Pattern' a -> b Source #

foldr1 :: (a -> a -> a) -> Pattern' a -> a Source #

foldl1 :: (a -> a -> a) -> Pattern' a -> a Source #

toList :: Pattern' a -> [a] Source #

null :: Pattern' a -> Bool Source #

length :: Pattern' a -> Int Source #

elem :: Eq a => a -> Pattern' a -> Bool Source #

maximum :: Ord a => Pattern' a -> a Source #

minimum :: Ord a => Pattern' a -> a Source #

sum :: Num a => Pattern' a -> a Source #

product :: Num a => Pattern' a -> a Source #

Traversable Pattern' Source # |
Instance details Defined in Agda.Syntax.Internal Methods traverse :: Applicative f => (a -> f b) -> Pattern' a -> f (Pattern' b) Source # sequenceA :: Applicative f => Pattern' (f a) -> f (Pattern' a) Source # mapM :: Monad m => (a -> m b) -> Pattern' a -> m (Pattern' b) Source # sequence :: Monad m => Pattern' (m a) -> m (Pattern' a) Source #
LabelPatVars Pattern DeBruijnPattern Source # |

Instance details

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVarLabel DeBruijnPattern |
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVarLabel DeBruijnPattern = Int

Methods

labelPatVars :: Pattern -> State [PatVarLabel DeBruijnPattern] DeBruijnPattern Source #

unlabelPatVars :: DeBruijnPattern -> Pattern 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 #
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 #
DeBruijn (Pattern' a) => TermToPattern Term (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Internal Methods termToPattern :: Term -> TCM (Pattern' a) Source #
IsProjP (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods isProjP :: Pattern' a -> Maybe (ProjOrigin, AmbiguousQName) Source #
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 #
PatternVars (Arg (Pattern' a)) Source # |

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut (Arg (Pattern' a)) |
Instance details Defined in Agda.Syntax.Internal type PatternVarOut (Arg (Pattern' a)) = a

Methods

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

PatternVars (NamedArg (Pattern' a)) Source # |

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut (NamedArg (Pattern' a)) |
Instance details Defined in Agda.Syntax.Internal type PatternVarOut (NamedArg (Pattern' a)) = a

Methods

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

NamesIn (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Pattern' a -> m Source #
CountPatternVars (Pattern' x) Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods countPatternVars :: Pattern' x -> Int Source #
PatternVarModalities (Pattern' x) Source # |

Instance details

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVar (Pattern' x) |
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVar (Pattern' x) = x

Methods

patternVarModalities :: Pattern' x -> [(PatVar (Pattern' x), Modality)] Source #

KillRange a => KillRange (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Pattern' a) Source #
UsableSizeVars (Masked DeBruijnPattern) Source # |
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet Source #
UsableSizeVars [DeBruijnPattern] Source # |
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: [DeBruijnPattern] -> TerM VarSet Source #
PrettyTCM a => PrettyTCM (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Pattern' a -> m Doc Source #
NormaliseProjP (Pattern' x) Source # |
Instance details Defined in Agda.TypeChecking.Records Methods normaliseProjP :: HasConstInfo m => Pattern' x -> m (Pattern' x) 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 #
IsFlexiblePattern (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Pattern' a -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Pattern' a -> m Bool Source #
EmbPrj a => EmbPrj (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Pattern' a -> S Word32 Source # icod_ :: Pattern' a -> S Word32 Source # value :: Word32 -> R (Pattern' a) 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 #
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 #
DeBruijn a => IApplyVars (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Telescope.Path Methods iApplyVars :: Pattern' a -> [Int] Source #
NFData x => NFData (Pattern' x) Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Pattern' x -> () Source #
Generic (Pattern' x) Source # |

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep (Pattern' x) |

Instance details

Defined in Agda.Syntax.Internal

type Rep (Pattern' x) = D1 ('MetaData "Pattern'" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((C1 ('MetaCons "VarP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 x)) :+: (C1 ('MetaCons "DotP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: C1 ('MetaCons "ConP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConHead) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConPatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' x)]))))) :+: ((C1 ('MetaCons "LitP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: C1 ('MetaCons "ProjP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProjOrigin) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))) :+: (C1 ('MetaCons "IApplyP" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 x))) :+: C1 ('MetaCons "DefP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' x)]))))))

Methods

from :: Pattern' x -> Rep (Pattern' x) x0 Source #

to :: Rep (Pattern' x) x0 -> Pattern' x Source #

Show x => Show (Pattern' x) Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Pattern' x -> ShowS Source # show :: Pattern' x -> String Source # showList :: [Pattern' x] -> ShowS Source #
Eq a => Eq (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Pattern' a -> Pattern' a -> Bool Source # (/=) :: Pattern' a -> Pattern' a -> Bool Source #
ToNLPat (Arg DeBruijnPattern) (Elim' NLPat) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: Arg DeBruijnPattern -> Elim' NLPat Source #
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: NamedArg DeBruijnPattern -> Elim' NLPat Source #
type PatVarLabel DeBruijnPattern Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVarLabel DeBruijnPattern = Int
type SubstArg DeBruijnPattern Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg DeBruijnPattern = DeBruijnPattern
type SubstArg Pattern Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Pattern = Term
type SubstArg SplitPattern Source # |
Instance details Defined in Agda.TypeChecking.Coverage.Match type SubstArg SplitPattern = SplitPattern
type PatternVarOut (Arg (Pattern' a)) Source # |
Instance details Defined in Agda.Syntax.Internal type PatternVarOut (Arg (Pattern' a)) = a
type PatternVarOut (NamedArg (Pattern' a)) Source # |
Instance details Defined in Agda.Syntax.Internal type PatternVarOut (NamedArg (Pattern' a)) = a
type PatVar (Pattern' x) Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVar (Pattern' x) = x
type Rep (Pattern' x) Source # |

Instance details

Defined in Agda.Syntax.Internal

type Rep (Pattern' x) = D1 ('MetaData "Pattern'" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((C1 ('MetaCons "VarP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 x)) :+: (C1 ('MetaCons "DotP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: C1 ('MetaCons "ConP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConHead) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConPatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' x)]))))) :+: ((C1 ('MetaCons "LitP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: C1 ('MetaCons "ProjP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProjOrigin) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))) :+: (C1 ('MetaCons "IApplyP" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 x))) :+: C1 ('MetaCons "DefP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' x)]))))))

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 `annFinite (argInfoAnnotation domInfo) = 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
- domName :: Maybe NamedName

  e.g. `x` in `{x = y : A} -> B`.

- domIsFinite :: Bool

  Is this a Π-type (False), or a partial type (True)?

- 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 #
GetDefs Telescope Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Telescope -> m () Source #
Reify Telescope Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Telescope |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Telescope = Telescope

Methods

reify :: MonadReify m => Telescope -> m (ReifiesTo Telescope) Source #

reifyWhen :: MonadReify m => Bool -> Telescope -> m (ReifiesTo Telescope) Source #

TerSetSizeDepth ListTel Source # |
Instance details Defined in Agda.Termination.Monad Methods terSetSizeDepth :: ListTel -> TerM a -> TerM a Source #
TerSetSizeDepth Telescope Source # |
Instance details Defined in Agda.Termination.Monad Methods terSetSizeDepth :: Telescope -> TerM a -> TerM a 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 #
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 #
PrettyTCM Telescope Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Telescope -> m Doc Source #
Reduce Telescope Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Telescope -> ReduceM Telescope Source # reduceB' :: Telescope -> ReduceM (Blocked Telescope) 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 #
Abstract Telescope Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Telescope -> Telescope 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 #
LensSort a => LensSort (Dom a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' (Dom a) Sort Source # getSort :: Dom a -> Sort Source #
SgTel (Dom Type) Source # |
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom Type -> Telescope Source #
SgTel (Dom (ArgName, Type)) Source # |
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom (ArgName, Type) -> Telescope Source #
GetDefs a => GetDefs (Dom a) Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Dom a -> m () 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 #
Reify i => Reify (Dom i) Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Dom i) |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (Dom i) = Arg (ReifiesTo i)

Methods

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

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

AbsTerm a => AbsTerm (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> Term -> Dom a -> 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 #
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 #
PrecomputeFreeVars a => PrecomputeFreeVars (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Dom a -> FV (Dom a) Source #
(Reduce a, ForceNotFree a, TermSubst 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 :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Dom a -> m Bool Source #
UsableRelevance a => UsableRelevance (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Dom a -> m Bool Source #
MentionsMeta t => MentionsMeta (Dom t) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Dom t -> Bool Source #
AnyRigid a => AnyRigid (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM 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 #
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 (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 (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 (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 #
ComputeOccurrences a => ComputeOccurrences (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Dom a -> OccM OccurrencesBuilder Source #
PrettyTCM (Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Dom Type -> m Doc Source #
ToTerm (Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Dom Type -> ReduceM Term) Source #
Normalise t => Normalise (Dom t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: 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 #
Simplify t => Simplify (Dom t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Dom t -> ReduceM (Dom t)
GetMatchables a => GetMatchables (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: Dom a -> [QName] Source #
EmbPrj a => EmbPrj (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Dom a -> S Word32 Source # icod_ :: Dom a -> S Word32 Source # value :: Word32 -> R (Dom a) 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)
Unquote a => Unquote (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM (Dom a) Source #
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 #
NFData e => NFData (Dom e) Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Dom e -> () Source #
Functor (Dom' t) Source # |
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Dom' t a -> Dom' t b Source # (<$) :: a -> Dom' t b -> Dom' t a Source #
Foldable (Dom' t) Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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

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

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

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

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

null :: Dom' t a -> Bool Source #

length :: Dom' t a -> Int Source #

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

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

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

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

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

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) Source # sequenceA :: Applicative f => Dom' t (f a) -> f (Dom' t a) Source # mapM :: Monad m => (a -> m b) -> Dom' t a -> m (Dom' t b) Source # sequence :: Monad m => Dom' t (m a) -> m (Dom' t a) Source #
Ord a => Ord (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Dom a -> Dom a -> Ordering Source # (<) :: Dom a -> Dom a -> Bool Source # (<=) :: Dom a -> Dom a -> Bool Source # (>) :: Dom a -> Dom a -> Bool Source # (>=) :: Dom a -> Dom a -> Bool Source # max :: Dom a -> Dom a -> Dom a Source # min :: Dom a -> 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 #
Match a b => Match (Dom a) (Dom b) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Context -> TypeOf (Dom b) -> Dom a -> Dom b -> NLM () Source #
NLPatToTerm p a => NLPatToTerm (Dom p) (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: PureTCM m => Dom p -> m (Dom a) Source #
PatternFrom a b => PatternFrom (Dom a) (Dom b) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> TypeOf (Dom a) -> Dom a -> TCM (Dom b) Source #
LensAnnotation (Dom' t e) Source # |
Instance details Defined in Agda.Syntax.Internal Methods getAnnotation :: Dom' t e -> Annotation Source # setAnnotation :: Annotation -> Dom' t e -> Dom' t e Source # mapAnnotation :: (Annotation -> Annotation) -> Dom' t e -> Dom' t e 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 #
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 #
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 #
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 #
LensLock (Dom' t e) Source # |
Instance details Defined in Agda.Syntax.Internal Methods getLock :: Dom' t e -> Lock Source # setLock :: Lock -> Dom' t e -> Dom' t e Source # mapLock :: (Lock -> Lock) -> Dom' t e -> Dom' t e Source #
LensModalPolarity (Dom' t e) Source # |
Instance details Defined in Agda.Syntax.Internal Methods getModalPolarity :: Dom' t e -> PolarityModality Source # setModalPolarity :: PolarityModality -> Dom' t e -> Dom' t e Source # mapModalPolarity :: (PolarityModality -> PolarityModality) -> 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 #
LensNamed (Dom' t e) Source # |

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type NameOf (Dom' t e) |
Instance details Defined in Agda.Syntax.Internal type NameOf (Dom' t e) = NamedName

Methods

lensNamed :: Lens' (Dom' t e) (Maybe (NameOf (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 #
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 #
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 #
(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 #
SgTel (ArgName, Dom Type) Source # |
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: (ArgName, Dom Type) -> Telescope Source #
(AllMetas a, AllMetas b) => AllMetas (Dom' a b) Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> Dom' a b -> m Source #
(NamesIn a, NamesIn b) => NamesIn (Dom' a b) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Dom' a b -> m Source #
HasRange a => HasRange (Dom' t a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods getRange :: Dom' t a -> Range Source #
(KillRange t, KillRange a) => KillRange (Dom' t a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Dom' t a) Source #
(ToAbstract r, AbsOfRef r ~ Expr) => ToAbstract (Dom r, Name) Source # |

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Dom r, Name) |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Dom r, Name) = TypedBinding

Methods

toAbstract :: MonadReflectedToAbstract m => (Dom r, Name) -> m (AbsOfRef (Dom r, Name)) 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 #
AddContext (List1 Name, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 Name, Dom Type) -> m a -> m a Source # contextSize :: (List1 Name, Dom Type) -> Nat Source #
AddContext (List1 (WithHiding Name), Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (WithHiding Name), Dom Type) -> m a -> m a Source # contextSize :: (List1 (WithHiding Name), Dom Type) -> Nat Source #
AddContext (Text, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (Text, Dom Type) -> m a -> m a Source # contextSize :: (Text, 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 ([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 #
(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 #
(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 #
(Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Dom' a b) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Dom' a b) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Dom' a b) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Dom' a b)) -> Dom' a b -> Dom' a b Source #

(Show t, Show e) => Show (Dom' t e) Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Dom' t e -> ShowS Source # show :: Dom' t e -> String Source # showList :: [Dom' t e] -> ShowS 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 Source # (/=) :: Dom' t a -> Dom' t a -> Bool Source #
type ReifiesTo Telescope Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Telescope = Telescope
type TypeOf (Dom a) Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf (Dom a) = TypeOf a
type ReifiesTo (Dom i) Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (Dom i) = Arg (ReifiesTo i)
type NameOf (Dom' t e) Source # |
Instance details Defined in Agda.Syntax.Internal type NameOf (Dom' t e) = NamedName
type AbsOfRef (Dom r, Name) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Dom r, Name) = TypedBinding
type SubstArg (Dom' a b) Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Dom' a b) = SubstArg a

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

Convert a telescope to its list form.

type Telescope = Tele (Dom Type) Source #

type Substitution = Substitution' Term Source #

type Dom = Dom' Term Source #

type Level = Level' Term Source #

type Elim = Elim' Term Source #

data Sort' t Source #

Sorts.

Constructors

Univ Univ (Level' t) | `Prop ℓ`, `Set ℓ`, `SSet ℓ`.
Inf Univ !Integer | `Propωᵢ`, `(S)Setωᵢ`.
SizeUniv | `SizeUniv`, a sort inhabited by type `Size`.
LockUniv | `LockUniv`, a sort for locks.
LevelUniv | `LevelUniv`, a sort inhabited by type `Level`. When --level-universe isn't on, this universe reduces to `Set 0`
IntervalUniv | `IntervalUniv`, a sort inhabited by the cubical interval.
PiSort (Dom' t t) (Sort' 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

Pretty Sort Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Sort -> Doc Source # prettyPrec :: Int -> Sort -> Doc Source # prettyList :: [Sort] -> Doc Source #
LensSort Sort Source # |
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' Sort Sort Source # getSort :: Sort -> Sort Source #
TermSize Sort Source # |
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Sort -> Int Source # tsize :: Sort -> Sum Int Source #
GetDefs Sort Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Sort -> 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 #
AllMetas Sort Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> Sort -> m Source #
NamesIn Sort Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Sort -> m Source #
KillRange Sort Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Sort Source #
Reify Sort Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Sort |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Sort = Expr

Methods

reify :: MonadReify m => Sort -> m (ReifiesTo Sort) Source #

reifyWhen :: MonadReify m => Bool -> Sort -> m (ReifiesTo Sort) Source #

AbsTerm Sort Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> Term -> Sort -> Sort Source #
EqualSy Sort Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Sort -> Sort -> Bool Source #
CheckInternal Sort Source # |

Instance details

Defined in Agda.TypeChecking.CheckInternal

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Sort -> Comparison -> TypeOf Sort -> m Sort Source #

checkInternal :: MonadCheckInternal m => Sort -> Comparison -> TypeOf Sort -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf Sort ~ ()) => Action m -> Sort -> m Sort Source #

inferInternal :: (MonadCheckInternal m, TypeOf Sort ~ ()) => Sort -> m () Source #

Free Sort Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Sort -> FreeM a c Source #
PrecomputeFreeVars Sort Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Sort -> FV Sort Source #
ForceNotFree Sort Source # |
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Sort -> m Sort
UsableModality Sort Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Sort -> m Bool Source #
UsableRelevance Sort Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Sort -> m Bool Source #
MentionsMeta Sort Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Sort -> Bool Source #
AnyRigid Sort Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM 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 #
UnFreezeMeta Sort Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Sort -> m () Source #
PrettyTCM Sort Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Sort -> m Doc Source #
Instantiate Sort Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Sort -> ReduceM Sort 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 #
Reduce Sort Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Sort -> ReduceM Sort Source # reduceB' :: Sort -> ReduceM (Blocked Sort) Source #
Simplify Sort Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Sort -> ReduceM Sort
EmbPrj Sort Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Sort -> S Word32 Source # icod_ :: Sort -> S Word32 Source # value :: Word32 -> R Sort 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 #
SynEq Sort Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Sort -> Sort -> SynEqM (Sort, Sort) synEq' :: Sort -> Sort -> SynEqM (Sort, Sort)
NFData Sort Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Sort -> () Source #
Eq Sort Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Sort -> Sort -> Bool Source # (/=) :: Sort -> Sort -> Bool Source #
Ord Sort Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Sort -> Sort -> Ordering Source # (<) :: Sort -> Sort -> Bool Source # (<=) :: Sort -> Sort -> Bool Source # (>) :: Sort -> Sort -> Bool Source # (>=) :: Sort -> Sort -> Bool Source # max :: Sort -> Sort -> Sort Source # min :: Sort -> Sort -> Sort Source #
Match NLPSort Sort Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Context -> TypeOf Sort -> NLPSort -> Sort -> NLM () Source #
NLPatToTerm NLPSort Sort Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: PureTCM m => NLPSort -> m Sort Source #
PatternFrom Sort NLPSort Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> TypeOf Sort -> Sort -> TCM NLPSort Source #
IsMeta a => IsMeta (Sort' a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods isMeta :: Sort' a -> Maybe MetaId Source #
(Coercible a Term, Subst a) => Subst (Sort' a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Sort' a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Sort' a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Sort' a)) -> Sort' a -> Sort' a Source #

Show t => Show (Sort' t) Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Sort' t -> ShowS Source # show :: Sort' t -> String Source # showList :: [Sort' t] -> ShowS Source #
type TypeOf Sort Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf Sort = ()
type ReifiesTo Sort Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Sort = Expr
type SubstArg (Sort' a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Sort' a) = SubstArg a

class PatternVars a where Source #

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

Associated Types

type PatternVarOut a Source #

Methods

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

#### Instances

Instances details

PatternVars (Arg (Pattern' a)) Source # |

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut (Arg (Pattern' a)) |
Instance details Defined in Agda.Syntax.Internal type PatternVarOut (Arg (Pattern' a)) = a

Methods

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

PatternVars (NamedArg (Pattern' a)) Source # |

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut (NamedArg (Pattern' a)) |
Instance details Defined in Agda.Syntax.Internal type PatternVarOut (NamedArg (Pattern' a)) = a

Methods

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

PatternVars a => PatternVars [a] Source # |

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type PatternVarOut [a] |
Instance details Defined in Agda.Syntax.Internal type PatternVarOut [a] = PatternVarOut a

Methods

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

type Sort = Sort' Term Source #

type DataOrRecord = DataOrRecord' PatternOrCopattern Source #

type Args = [Arg Term] Source #

Type of argument lists.

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

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 #
Functor Abs Source # |
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Abs a -> Abs b Source # (<$) :: a -> Abs b -> Abs a Source #
Foldable Abs Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => Abs m -> m Source #

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

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

foldr :: (a -> b -> b) -> b -> Abs a -> b Source #

foldr' :: (a -> b -> b) -> b -> Abs a -> b Source #

foldl :: (b -> a -> b) -> b -> Abs a -> b Source #

foldl' :: (b -> a -> b) -> b -> Abs a -> b Source #

foldr1 :: (a -> a -> a) -> Abs a -> a Source #

foldl1 :: (a -> a -> a) -> Abs a -> a Source #

toList :: Abs a -> [a] Source #

null :: Abs a -> Bool Source #

length :: Abs a -> Int Source #

elem :: Eq a => a -> Abs a -> Bool Source #

maximum :: Ord a => Abs a -> a Source #

minimum :: Ord a => Abs a -> a Source #

sum :: Num a => Abs a -> a Source #

product :: Num a => Abs a -> a Source #

Traversable Abs Source # |
Instance details Defined in Agda.Syntax.Internal Methods traverse :: Applicative f => (a -> f b) -> Abs a -> f (Abs b) Source # sequenceA :: Applicative f => Abs (f a) -> f (Abs a) Source # mapM :: Monad m => (a -> m b) -> Abs a -> m (Abs b) Source # sequence :: Monad m => Abs (m a) -> m (Abs a) Source #
Pretty t => Pretty (Abs t) Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Abs t -> Doc Source # prettyPrec :: Int -> Abs t -> Doc Source # prettyList :: [Abs t] -> Doc Source #
Suggest (Abs b) Source # |
Instance details Defined in Agda.Syntax.Internal Methods suggestName :: Abs b -> Maybe String Source #
GetDefs a => GetDefs (Abs a) Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Abs a -> m () 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 #
NamesIn a => NamesIn (Abs a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Abs a -> m Source #
KillRange a => KillRange (Abs a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Abs a) Source #
(Free i, Reify i) => Reify (Abs i) Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Abs i) |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (Abs i) = (Name, ReifiesTo i)

Methods

reify :: MonadReify m => Abs i -> m (ReifiesTo (Abs i)) Source #

reifyWhen :: MonadReify m => Bool -> Abs i -> m (ReifiesTo (Abs i)) Source #

(TermSubst a, AbsTerm a) => AbsTerm (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> Term -> Abs a -> Abs a Source #
(Subst a, EqualSy a) => EqualSy (Abs a) Source # | Ignores `absName`.
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Abs a -> Abs a -> Bool 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 #
PrecomputeFreeVars a => PrecomputeFreeVars (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Abs a -> FV (Abs a) Source #
(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 a, UsableRelevance a) => UsableRelevance (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> 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 a, AnyRigid a) => AnyRigid (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Abs a -> tcm Bool Source #
Occurs (Abs Term) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Abs Term -> OccursM (Abs Term) Source # metaOccurs :: MetaId -> Abs Term -> TCM () Source #
Occurs (Abs Type) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Abs Type -> OccursM (Abs Type) Source # metaOccurs :: MetaId -> Abs Type -> TCM () Source #
IsInstantiatedMeta a => IsInstantiatedMeta (Abs a) Source # | Does not worry about raising.
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: ReadTCState m => Abs a -> m Bool Source #
UnFreezeMeta a => UnFreezeMeta (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Abs a -> m () Source #
ComputeOccurrences a => ComputeOccurrences (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Abs a -> OccM OccurrencesBuilder Source #
(PrettyTCM a, Subst a) => PrettyTCM (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Abs a -> m Doc Source #
Instantiate t => Instantiate (Abs t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Abs t -> ReduceM (Abs t) Source #
(Subst a, InstantiateFull a) => InstantiateFull (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Abs a -> ReduceM (Abs a) Source #
(Subst a, Normalise a) => Normalise (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Abs a -> ReduceM (Abs a) Source #
(Subst 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 #
(Subst a, Simplify a) => Simplify (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Abs a -> ReduceM (Abs a)
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 #
EmbPrj a => EmbPrj (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Abs a -> S Word32 Source # icod_ :: Abs a -> S Word32 Source # value :: Word32 -> R (Abs a) Source #
Subst a => Subst (Abs a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Abs a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Abs a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Abs a)) -> Abs a -> Abs a Source #

(Subst 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)
Sized a => Sized (Abs a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods size :: Abs a -> Int Source # natSize :: Abs a -> Peano Source #
NFData a => NFData (Abs a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Abs a -> () Source #
Generic (Abs a) Source # |

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep (Abs a) |

Instance details

Defined in Agda.Syntax.Internal

type Rep (Abs a) = D1 ('MetaData "Abs" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Abs" 'PrefixI 'True) (S1 ('MetaSel ('Just "absName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgName) :*: S1 ('MetaSel ('Just "unAbs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "NoAbs" 'PrefixI 'True) (S1 ('MetaSel ('Just "absName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgName) :*: S1 ('MetaSel ('Just "unAbs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

Methods

from :: Abs a -> Rep (Abs a) x Source #

to :: Rep (Abs a) x -> Abs a Source #

Show a => Show (Abs a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Abs a -> ShowS Source # show :: Abs a -> String Source # showList :: [Abs a] -> ShowS Source #
(Subst 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 Source # (/=) :: Abs a -> Abs a -> Bool Source #
(Subst a, Ord a) => Ord (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Abs a -> Abs a -> Ordering Source # (<) :: Abs a -> Abs a -> Bool Source # (<=) :: Abs a -> Abs a -> Bool Source # (>) :: Abs a -> Abs a -> Bool Source # (>=) :: Abs a -> Abs a -> Bool Source # max :: Abs a -> Abs a -> Abs a Source # min :: Abs a -> 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 :: PureTCM m => Abs p -> m (Abs a) Source #
type TypeOf (Abs Term) Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf (Abs Term) = (Dom Type, Abs Type)
type TypeOf (Abs Type) Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf (Abs Type) = Dom Type
type ReifiesTo (Abs i) Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (Abs i) = (Name, ReifiesTo i)
type SubstArg (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Abs a) = SubstArg a
type Rep (Abs a) Source # |

Instance details

Defined in Agda.Syntax.Internal

type Rep (Abs a) = D1 ('MetaData "Abs" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Abs" 'PrefixI 'True) (S1 ('MetaSel ('Just "absName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgName) :*: S1 ('MetaSel ('Just "unAbs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "NoAbs" 'PrefixI 'True) (S1 ('MetaSel ('Just "absName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgName) :*: S1 ('MetaSel ('Just "unAbs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

class LensSort a where Source #

Minimal complete definition

lensSort

Methods

lensSort :: Lens' a Sort Source #

getSort :: a -> Sort Source #

#### Instances

Instances details

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

type Elims Source #

Arguments

= [Elim] | eliminations ordered left-to-right.

arity :: Type -> Nat Source #

Doesn't do any reduction.

pattern Prop :: Level' t -> Sort' t Source #

pattern SSet :: Level' t -> Sort' t Source #

data PlusLevel' t Source #

Constructors

Plus !Integer t |

#### Instances

Instances details

Pretty PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: PlusLevel -> Doc Source # prettyPrec :: Int -> PlusLevel -> Doc Source # prettyList :: [PlusLevel] -> Doc Source #
TermSize PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal Methods termSize :: PlusLevel -> Int Source # tsize :: PlusLevel -> Sum Int Source #
GetDefs PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => PlusLevel -> 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 #
AllMetas PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> PlusLevel -> m Source #
NamesIn PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> PlusLevel -> m Source #
KillRange PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT PlusLevel Source #
AbsTerm PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> Term -> PlusLevel -> PlusLevel Source #
EqualSy PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: PlusLevel -> PlusLevel -> Bool Source #
CheckInternal PlusLevel Source # |

Instance details

Defined in Agda.TypeChecking.CheckInternal

Methods

checkInternal' :: MonadCheckInternal m => Action m -> PlusLevel -> Comparison -> TypeOf PlusLevel -> m PlusLevel Source #

checkInternal :: MonadCheckInternal m => PlusLevel -> Comparison -> TypeOf PlusLevel -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf PlusLevel ~ ()) => Action m -> PlusLevel -> m PlusLevel Source #

inferInternal :: (MonadCheckInternal m, TypeOf PlusLevel ~ ()) => PlusLevel -> m () Source #

PrecomputeFreeVars PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: PlusLevel -> FV PlusLevel Source #
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 :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> PlusLevel -> m Bool Source #
MentionsMeta PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> PlusLevel -> Bool Source #
AnyRigid PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM 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 #
IsInstantiatedMeta PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: ReadTCState m => PlusLevel -> m Bool Source #
UnFreezeMeta PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => PlusLevel -> m () Source #
ComputeOccurrences PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: PlusLevel -> OccM OccurrencesBuilder 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 #
Reduce PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: PlusLevel -> ReduceM PlusLevel Source # reduceB' :: PlusLevel -> ReduceM (Blocked PlusLevel) Source #
Simplify PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: PlusLevel -> ReduceM PlusLevel
EmbPrj PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: PlusLevel -> S Word32 Source # icod_ :: PlusLevel -> S Word32 Source # value :: Word32 -> R PlusLevel 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 #
SynEq PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: PlusLevel -> PlusLevel -> SynEqM (PlusLevel, PlusLevel) synEq' :: PlusLevel -> PlusLevel -> SynEqM (PlusLevel, PlusLevel)
NFData PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: PlusLevel -> () Source #
Functor PlusLevel' Source # |
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> PlusLevel' a -> PlusLevel' b Source # (<$) :: a -> PlusLevel' b -> PlusLevel' a Source #
Foldable PlusLevel' Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => PlusLevel' m -> m Source #

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

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

foldr :: (a -> b -> b) -> b -> PlusLevel' a -> b Source #

foldr' :: (a -> b -> b) -> b -> PlusLevel' a -> b Source #

foldl :: (b -> a -> b) -> b -> PlusLevel' a -> b Source #

foldl' :: (b -> a -> b) -> b -> PlusLevel' a -> b Source #

foldr1 :: (a -> a -> a) -> PlusLevel' a -> a Source #

foldl1 :: (a -> a -> a) -> PlusLevel' a -> a Source #

toList :: PlusLevel' a -> [a] Source #

null :: PlusLevel' a -> Bool Source #

length :: PlusLevel' a -> Int Source #

elem :: Eq a => a -> PlusLevel' a -> Bool Source #

maximum :: Ord a => PlusLevel' a -> a Source #

minimum :: Ord a => PlusLevel' a -> a Source #

sum :: Num a => PlusLevel' a -> a Source #

product :: Num a => PlusLevel' a -> a Source #

Traversable PlusLevel' Source # |
Instance details Defined in Agda.Syntax.Internal Methods traverse :: Applicative f => (a -> f b) -> PlusLevel' a -> f (PlusLevel' b) Source # sequenceA :: Applicative f => PlusLevel' (f a) -> f (PlusLevel' a) Source # mapM :: Monad m => (a -> m b) -> PlusLevel' a -> m (PlusLevel' b) Source # sequence :: Monad m => PlusLevel' (m a) -> m (PlusLevel' a) Source #
Eq PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: PlusLevel -> PlusLevel -> Bool Source # (/=) :: PlusLevel -> PlusLevel -> Bool Source #
Ord PlusLevel Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Methods

compare :: PlusLevel -> PlusLevel -> Ordering Source #

(<) :: PlusLevel -> PlusLevel -> Bool Source #

(<=) :: PlusLevel -> PlusLevel -> Bool Source #

(>) :: PlusLevel -> PlusLevel -> Bool Source #

(>=) :: PlusLevel -> PlusLevel -> Bool Source #

max :: PlusLevel -> PlusLevel -> PlusLevel Source #

min :: PlusLevel -> PlusLevel -> PlusLevel Source #

Free t => Free (PlusLevel' t) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => PlusLevel' t -> FreeM a c Source #
Instantiate t => Instantiate (PlusLevel' t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: PlusLevel' t -> ReduceM (PlusLevel' t) Source #
IsMeta a => IsMeta (PlusLevel' a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods isMeta :: PlusLevel' a -> Maybe MetaId Source #
Subst a => Subst (PlusLevel' a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (PlusLevel' a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (PlusLevel' a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (PlusLevel' a)) -> PlusLevel' a -> PlusLevel' a Source #

Show t => Show (PlusLevel' t) Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> PlusLevel' t -> ShowS Source # show :: PlusLevel' t -> String Source # showList :: [PlusLevel' t] -> ShowS Source #
type TypeOf PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf PlusLevel = ()
type TypeOf [PlusLevel] Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf [PlusLevel] = ()
type SubstArg (PlusLevel' a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (PlusLevel' a) = SubstArg a

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 Level Source # |
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Level -> Int Source # tsize :: Level -> Sum Int Source #
TermSize PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal Methods termSize :: PlusLevel -> Int Source # tsize :: PlusLevel -> 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 #
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 #
(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 #

type Blocked = Blocked' Term Source #

type NotBlocked = NotBlocked' Term Source #

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 #

type NamedArgs = [NamedArg Term] Source #

type DataOrRecord_ = DataOrRecord' () Source #

pattern IsRecord_ :: DataOrRecord_ 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 #

type ConInfo = ConOrigin Source #

data Type'' t a Source #

Types are terms with a sort annotation.

Constructors

El |

Fields

- _getSort :: Sort' t
- unEl :: a

#### Instances

Instances details

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 #
GetDefs Telescope Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Telescope -> m () Source #
GetDefs Type Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Type -> 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 #
AllMetas Type Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> Type -> m Source #
Reify Telescope Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Telescope |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Telescope = Telescope

Methods

reify :: MonadReify m => Telescope -> m (ReifiesTo Telescope) Source #

reifyWhen :: MonadReify m => Bool -> Telescope -> m (ReifiesTo Telescope) Source #

Reify Type Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Type |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Type = Type

Methods

reify :: MonadReify m => Type -> m (ReifiesTo Type) Source #

reifyWhen :: MonadReify m => Bool -> Type -> m (ReifiesTo Type) Source #

TerSetSizeDepth ListTel Source # |
Instance details Defined in Agda.Termination.Monad Methods terSetSizeDepth :: ListTel -> TerM a -> TerM a Source #
TerSetSizeDepth Telescope Source # |
Instance details Defined in Agda.Termination.Monad Methods terSetSizeDepth :: Telescope -> TerM a -> TerM a Source #
AbsTerm Type Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> Term -> Type -> Type Source #
EqualSy Type Source # | Ignores sorts.
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Type -> Type -> Bool Source #
CheckInternal Type Source # |

Instance details

Defined in Agda.TypeChecking.CheckInternal

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Type -> Comparison -> TypeOf Type -> m Type Source #

checkInternal :: MonadCheckInternal m => Type -> Comparison -> TypeOf Type -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf Type ~ ()) => Action m -> Type -> m Type Source #

inferInternal :: (MonadCheckInternal m, TypeOf Type ~ ()) => Type -> m () 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 #
PrecomputeFreeVars Type Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Type -> FV Type Source #
ForceNotFree Type Source # |
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Type -> m Type
MentionsMeta Type Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Type -> Bool Source #
AnyRigid Type Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM 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 #
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 #
UnFreezeMeta Type Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Type -> m () Source #
ComputeOccurrences Type Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Type -> OccM OccurrencesBuilder 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 #
PrimTerm Type Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Type -> TCM Term Source #
PrimType Type Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primType :: Type -> TCM Type Source #
ToTerm Type Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Type -> ReduceM Term) 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 #
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 #
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 #
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)
NFData Type Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Type -> () Source #
Match NLPType Type Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Context -> TypeOf Type -> NLPType -> Type -> NLM () Source #
NLPatToTerm NLPType Type Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: PureTCM m => NLPType -> m Type Source #
PatternFrom Type NLPType Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> TypeOf Type -> Type -> TCM NLPType Source #
LensSort (Type' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' (Type' a) Sort Source # getSort :: Type' a -> Sort Source #
SgTel (Dom Type) Source # |
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom Type -> Telescope Source #
SgTel (Dom (ArgName, Type)) Source # |
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom (ArgName, Type) -> Telescope Source #
NamesIn a => NamesIn (Type' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Type' a -> m Source #
KillRange a => KillRange (Type' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Type' 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 #
UsableRelevance a => UsableModality (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Type' a -> m Bool Source #
UsableRelevance a => UsableRelevance (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Type' a -> m Bool Source #
Occurs (Abs Type) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Abs Type -> OccursM (Abs Type) Source # metaOccurs :: MetaId -> Abs Type -> TCM () 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 (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 (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 (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 #
PrettyTCM (Arg Type) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Arg Type -> m Doc Source #
PrettyTCM (Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Dom Type -> m Doc Source #
PrettyTCM (Type' NLPat) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Type' NLPat -> m Doc Source #
ToTerm (Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Dom Type -> ReduceM Term) Source #
Instantiate t => Instantiate (Type' t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Type' t -> ReduceM (Type' t) 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)
EmbPrj a => EmbPrj (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Type' a -> S Word32 Source # icod_ :: Type' a -> S Word32 Source # value :: Word32 -> R (Type' a) Source #
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 #
Functor (Type'' t) Source # |
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Type'' t a -> Type'' t b Source # (<$) :: a -> Type'' t b -> Type'' t a Source #
Foldable (Type'' t) Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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) Source # sequenceA :: Applicative f => Type'' t (f a) -> f (Type'' t a) Source # mapM :: Monad m => (a -> m b) -> Type'' t a -> m (Type'' t b) Source # sequence :: Monad m => Type'' t (m a) -> m (Type'' t a) 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 Source # (/=) :: Type' a -> Type' a -> Bool Source #
Ord a => Ord (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Type' a -> Type' a -> Ordering Source # (<) :: Type' a -> Type' a -> Bool Source # (<=) :: Type' a -> Type' a -> Bool Source # (>) :: Type' a -> Type' a -> Bool Source # (>=) :: Type' a -> Type' a -> Bool Source # max :: Type' a -> Type' a -> Type' a Source # min :: Type' a -> Type' a -> Type' a Source #
SgTel (ArgName, Dom Type) Source # |
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: (ArgName, Dom Type) -> Telescope 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 #
AddContext (List1 Name, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 Name, Dom Type) -> m a -> m a Source # contextSize :: (List1 Name, Dom Type) -> Nat Source #
AddContext (List1 (Arg Name), Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (Arg Name), Type) -> m a -> m a Source # contextSize :: (List1 (Arg Name), Type) -> Nat Source #
AddContext (List1 (NamedArg Name), Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (NamedArg Name), Type) -> m a -> m a Source # contextSize :: (List1 (NamedArg Name), Type) -> Nat Source #
AddContext (List1 (WithHiding Name), Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (WithHiding Name), Dom Type) -> m a -> m a Source # contextSize :: (List1 (WithHiding Name), Dom Type) -> Nat Source #
AddContext (Text, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (Text, Dom Type) -> m a -> m a Source # contextSize :: (Text, 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 ([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 ([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 ([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 #
IsMeta a => IsMeta (Type'' t a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods isMeta :: Type'' t a -> Maybe MetaId Source #
(Coercible a Term, Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Type'' a b) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Type'' a b) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Type'' a b) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Type'' a b)) -> Type'' a b -> Type'' a b Source #

(Show t, Show a) => Show (Type'' t a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Type'' t a -> ShowS Source # show :: Type'' t a -> String Source # showList :: [Type'' t a] -> ShowS Source #
type TypeOf Type Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf Type = ()
type ReifiesTo Telescope Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Telescope = Telescope
type ReifiesTo Type Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Type = Type
type TypeOf (Abs Type) Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf (Abs Type) = Dom Type
type SubstArg (Type'' a b) Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Type'' a b) = SubstArg a

type Type' a = Type'' Term a 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

TelToArgs Telescope Source # |
Instance details Defined in Agda.Syntax.Internal Methods telToArgs :: Telescope -> [Arg ArgName] Source #
GetDefs Telescope Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Telescope -> m () Source #
Reify Telescope Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Telescope |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Telescope = Telescope

Methods

reify :: MonadReify m => Telescope -> m (ReifiesTo Telescope) Source #

reifyWhen :: MonadReify m => Bool -> Telescope -> m (ReifiesTo Telescope) Source #

TerSetSizeDepth Telescope Source # |
Instance details Defined in Agda.Termination.Monad Methods terSetSizeDepth :: Telescope -> TerM a -> TerM a 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 #
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 #
PrettyTCM Telescope Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Telescope -> m Doc Source #
Reduce Telescope Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Telescope -> ReduceM Telescope Source # reduceB' :: Telescope -> ReduceM (Blocked Telescope) Source #
TeleNoAbs Telescope Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods teleNoAbs :: Telescope -> Term -> Term Source #
Abstract Telescope Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Telescope -> Telescope Source #
Functor Tele Source # |
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Tele a -> Tele b Source # (<$) :: a -> Tele b -> Tele a Source #
Foldable Tele Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => Tele m -> m Source #

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

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

foldr :: (a -> b -> b) -> b -> Tele a -> b Source #

foldr' :: (a -> b -> b) -> b -> Tele a -> b Source #

foldl :: (b -> a -> b) -> b -> Tele a -> b Source #

foldl' :: (b -> a -> b) -> b -> Tele a -> b Source #

foldr1 :: (a -> a -> a) -> Tele a -> a Source #

foldl1 :: (a -> a -> a) -> Tele a -> a Source #

toList :: Tele a -> [a] Source #

null :: Tele a -> Bool Source #

length :: Tele a -> Int Source #

elem :: Eq a => a -> Tele a -> Bool Source #

maximum :: Ord a => Tele a -> a Source #

minimum :: Ord a => Tele a -> a Source #

sum :: Num a => Tele a -> a Source #

product :: Num a => Tele a -> a Source #

Traversable Tele Source # |
Instance details Defined in Agda.Syntax.Internal Methods traverse :: Applicative f => (a -> f b) -> Tele a -> f (Tele b) Source # sequenceA :: Applicative f => Tele (f a) -> f (Tele a) Source # mapM :: Monad m => (a -> m b) -> Tele a -> m (Tele b) Source # sequence :: Monad m => Tele (m a) -> m (Tele 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 #
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 #
TermLike a => AllMetas (Tele a) Source # |
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> Tele a -> m Source #
NamesIn a => NamesIn (Tele a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Tele a -> m 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 #
MentionsMeta a => MentionsMeta (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Tele a -> Bool 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 #
ComputeOccurrences a => ComputeOccurrences (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Tele a -> OccM OccurrencesBuilder Source #
Instantiate t => Instantiate (Tele t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Tele t -> ReduceM (Tele t) Source #
(Subst a, InstantiateFull a) => InstantiateFull (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Tele a -> ReduceM (Tele a) Source #
(Subst a, Normalise a) => Normalise (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Tele a -> ReduceM (Tele a) Source #
(Subst a, Simplify a) => Simplify (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Tele a -> ReduceM (Tele a)
EmbPrj a => EmbPrj (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Tele a -> S Word32 Source # icod_ :: Tele a -> S Word32 Source # value :: Word32 -> R (Tele a) Source #
TermSubst 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 #
Subst a => Subst (Tele a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Tele a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Tele a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Tele a)) -> Tele a -> Tele a Source #

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 # natSize :: Tele a -> Peano Source #
NFData a => NFData (Tele a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Tele a -> () Source #
Generic (Tele a) Source # |

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep (Tele a) |

Instance details

Defined in Agda.Syntax.Internal

type Rep (Tele a) = D1 ('MetaData "Tele" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "EmptyTel" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ExtendTel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Abs (Tele a)))))

Methods

from :: Tele a -> Rep (Tele a) x Source #

to :: Rep (Tele a) x -> Tele a Source #

Show a => Show (Tele a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Tele a -> ShowS Source # show :: Tele a -> String Source # showList :: [Tele a] -> ShowS Source #
(Subst a, Eq a) => Eq (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Tele a -> Tele a -> Bool Source # (/=) :: Tele a -> Tele a -> Bool Source #
(Subst a, Ord a) => Ord (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Tele a -> Tele a -> Ordering Source # (<) :: Tele a -> Tele a -> Bool Source # (<=) :: Tele a -> Tele a -> Bool Source # (>) :: Tele a -> Tele a -> Bool Source # (>=) :: Tele a -> Tele a -> Bool Source # max :: Tele a -> Tele a -> Tele a Source # min :: Tele a -> Tele a -> Tele a Source #
type ReifiesTo Telescope Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Telescope = Telescope
type SubstArg (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Tele a) = SubstArg a
type Rep (Tele a) Source # |

Instance details

Defined in Agda.Syntax.Internal

type Rep (Tele a) = D1 ('MetaData "Tele" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "EmptyTel" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ExtendTel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Abs (Tele a)))))

data UnivSize Source #

Constructors

USmall | `PropSetSSet ℓ`.
ULarge | `(PropSetSSet)ωᵢ`.

#### Instances

Instances details

Show UnivSize Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> UnivSize -> ShowS Source # show :: UnivSize -> String Source # showList :: [UnivSize] -> ShowS Source #
Eq UnivSize Source # |
Instance details Defined in Agda.Syntax.Internal Methods (==) :: UnivSize -> UnivSize -> Bool Source # (/=) :: UnivSize -> UnivSize -> Bool Source #

type PlusLevel = PlusLevel' Term Source #

type LevelAtom = Term 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

Apply BraveTerm Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: BraveTerm -> Args -> BraveTerm Source # applyE :: BraveTerm -> Elims -> BraveTerm Source #
Subst BraveTerm Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg BraveTerm |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg BraveTerm = BraveTerm

Methods

applySubst :: Substitution' (SubstArg BraveTerm) -> BraveTerm -> BraveTerm Source #

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 #
Show BraveTerm Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> BraveTerm -> ShowS Source # show :: BraveTerm -> String Source # showList :: [BraveTerm] -> ShowS Source #
type SubstArg BraveTerm Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg BraveTerm = BraveTerm

type Blocked_ = Blocked () Source #

`'Blocked a` without the `a`.

type NAPs = [NamedArg DeBruijnPattern] Source #

Named pattern arguments.

type DeBruijnPattern = Pattern' DBPatVar Source #

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

type PatVarName = ArgName Source #

Pattern variables.

patVarNameToString :: PatVarName -> String Source #

nameToPatVarName :: Name -> PatVarName Source #

data PatternInfo Source #

Constructors

PatternInfo |

Fields

- patOrigin :: PatOrigin
- patAsNames :: [Name]

#### Instances

Instances details

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 Word32 Source # icod_ :: PatternInfo -> S Word32 Source # value :: Word32 -> R PatternInfo Source #
NFData PatternInfo Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: PatternInfo -> () Source #
Generic PatternInfo Source # |

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep PatternInfo |

Instance details

Defined in Agda.Syntax.Internal

type Rep PatternInfo = D1 ('MetaData "PatternInfo" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "PatternInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "patOrigin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatOrigin) :*: S1 ('MetaSel ('Just "patAsNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])))

Methods

from :: PatternInfo -> Rep PatternInfo x Source #

to :: Rep PatternInfo x -> PatternInfo Source #

Show PatternInfo Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> PatternInfo -> ShowS Source # show :: PatternInfo -> String Source # showList :: [PatternInfo] -> ShowS Source #
Eq PatternInfo Source # |
Instance details Defined in Agda.Syntax.Internal Methods (==) :: PatternInfo -> PatternInfo -> Bool Source # (/=) :: PatternInfo -> PatternInfo -> Bool Source #
type Rep PatternInfo Source # |

Instance details

Defined in Agda.Syntax.Internal

type Rep PatternInfo = D1 ('MetaData "PatternInfo" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "PatternInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "patOrigin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatOrigin) :*: S1 ('MetaSel ('Just "patAsNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])))

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
PatOSplitArg ArgName | Argument to 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

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 Word32 Source # icod_ :: PatOrigin -> S Word32 Source # value :: Word32 -> R PatOrigin Source #
NFData PatOrigin Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: PatOrigin -> () Source #
Generic PatOrigin Source # |

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep PatOrigin |

Instance details

Defined in Agda.Syntax.Internal

type Rep PatOrigin = D1 ('MetaData "PatOrigin" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (((C1 ('MetaCons "PatOSystem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatOSplit" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PatOSplitArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgName)) :+: (C1 ('MetaCons "PatOVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "PatODot" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "PatOWild" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatOCon" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PatORec" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PatOLit" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatOAbsurd" 'PrefixI 'False) (U1 :: Type -> Type)))))

Methods

from :: PatOrigin -> Rep PatOrigin x Source #

to :: Rep PatOrigin x -> PatOrigin Source #

Show PatOrigin Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> PatOrigin -> ShowS Source # show :: PatOrigin -> String Source # showList :: [PatOrigin] -> ShowS Source #
Eq PatOrigin Source # |
Instance details Defined in Agda.Syntax.Internal Methods (==) :: PatOrigin -> PatOrigin -> Bool Source # (/=) :: PatOrigin -> PatOrigin -> Bool Source #
type Rep PatOrigin Source # |

Instance details

Defined in Agda.Syntax.Internal

type Rep PatOrigin = D1 ('MetaData "PatOrigin" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (((C1 ('MetaCons "PatOSystem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatOSplit" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PatOSplitArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgName)) :+: (C1 ('MetaCons "PatOVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "PatODot" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "PatOWild" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatOCon" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PatORec" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PatOLit" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatOAbsurd" 'PrefixI 'False) (U1 :: Type -> Type)))))

defaultPatternInfo :: PatternInfo 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

NamesIn ConPatternInfo Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> ConPatternInfo -> m Source #
KillRange ConPatternInfo Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT 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 #
EmbPrj ConPatternInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ConPatternInfo -> S Word32 Source # icod_ :: ConPatternInfo -> S Word32 Source # value :: Word32 -> R ConPatternInfo Source #
Subst ConPatternInfo Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg ConPatternInfo |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg ConPatternInfo = Term

Methods

applySubst :: Substitution' (SubstArg ConPatternInfo) -> ConPatternInfo -> ConPatternInfo Source #

NFData ConPatternInfo Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: ConPatternInfo -> () Source #
Generic ConPatternInfo Source # |

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep ConPatternInfo |

Instance details

Defined in Agda.Syntax.Internal

type Rep ConPatternInfo = D1 ('MetaData "ConPatternInfo" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "ConPatternInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "conPInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Just "conPRecord") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "conPFallThrough") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "conPType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Arg Type))) :*: S1 ('MetaSel ('Just "conPLazy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))

Methods

from :: ConPatternInfo -> Rep ConPatternInfo x Source #

to :: Rep ConPatternInfo x -> ConPatternInfo Source #

Show ConPatternInfo Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> ConPatternInfo -> ShowS Source # show :: ConPatternInfo -> String Source # showList :: [ConPatternInfo] -> ShowS Source #
type SubstArg ConPatternInfo Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg ConPatternInfo = Term
type Rep ConPatternInfo Source # |

Instance details

Defined in Agda.Syntax.Internal

type Rep ConPatternInfo = D1 ('MetaData "ConPatternInfo" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "ConPatternInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "conPInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Just "conPRecord") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "conPFallThrough") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "conPType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Arg Type))) :*: S1 ('MetaSel ('Just "conPLazy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))

dotP :: Term -> Pattern' a Source #

data DBPatVar Source #

Type used when numbering pattern variables.

Constructors

DBPatVar |

Fields

- dbPatVarName :: PatVarName
- dbPatVarIndex :: !Int

#### Instances

Instances details

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 #
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 #
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 #
EmbPrj DBPatVar Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DBPatVar -> S Word32 Source # icod_ :: DBPatVar -> S Word32 Source # value :: Word32 -> R DBPatVar Source #
Subst DeBruijnPattern Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg DeBruijnPattern |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg DeBruijnPattern = DeBruijnPattern

Methods

applySubst :: Substitution' (SubstArg DeBruijnPattern) -> DeBruijnPattern -> DeBruijnPattern 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 #
NFData DBPatVar Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: DBPatVar -> () Source #
Generic DBPatVar Source # |

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep DBPatVar |

Instance details

Defined in Agda.Syntax.Internal

type Rep DBPatVar = D1 ('MetaData "DBPatVar" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "DBPatVar" 'PrefixI 'True) (S1 ('MetaSel ('Just "dbPatVarName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatVarName) :*: S1 ('MetaSel ('Just "dbPatVarIndex") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int)))

Methods

from :: DBPatVar -> Rep DBPatVar x Source #

to :: Rep DBPatVar x -> DBPatVar Source #

Show DBPatVar Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> DBPatVar -> ShowS Source # show :: DBPatVar -> String Source # showList :: [DBPatVar] -> ShowS Source #
Eq DBPatVar Source # |
Instance details Defined in Agda.Syntax.Internal Methods (==) :: DBPatVar -> DBPatVar -> Bool Source # (/=) :: DBPatVar -> DBPatVar -> Bool Source #
LabelPatVars Pattern DeBruijnPattern Source # |

Instance details

Defined in Agda.Syntax.Internal.Pattern

Associated Types

type PatVarLabel DeBruijnPattern |
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVarLabel DeBruijnPattern = Int

Methods

labelPatVars :: Pattern -> State [PatVarLabel DeBruijnPattern] DeBruijnPattern Source #

unlabelPatVars :: DeBruijnPattern -> Pattern Source #

UsableSizeVars (Masked DeBruijnPattern) Source # |
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet Source #
UsableSizeVars [DeBruijnPattern] Source # |
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: [DeBruijnPattern] -> TerM VarSet Source #
ToNLPat (Arg DeBruijnPattern) (Elim' NLPat) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: Arg DeBruijnPattern -> Elim' NLPat Source #
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: NamedArg DeBruijnPattern -> Elim' NLPat Source #
type PatVarLabel DeBruijnPattern Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVarLabel DeBruijnPattern = Int
type SubstArg DeBruijnPattern Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg DeBruijnPattern = DeBruijnPattern
type Rep DBPatVar Source # |

Instance details

Defined in Agda.Syntax.Internal

type Rep DBPatVar = D1 ('MetaData "DBPatVar" "Agda.Syntax.Internal" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "DBPatVar" 'PrefixI 'True) (S1 ('MetaSel ('Just "dbPatVarName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatVarName) :*: S1 ('MetaSel ('Just "dbPatVarIndex") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int)))

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.

absurdPatternName :: PatVarName Source #

noConPatternInfo :: ConPatternInfo Source #

toConPatternInfo :: ConInfo -> ConPatternInfo Source #

Build partial `ConPatternInfo` from `ConInfo`

fromConPatternInfo :: ConPatternInfo -> ConInfo Source #

Build `ConInfo` from `ConPatternInfo`.

type family PatternVarOut a Source #

#### Instances

Instances details

type PatternVarOut (Arg (Pattern' a)) Source # |
Instance details Defined in Agda.Syntax.Internal type PatternVarOut (Arg (Pattern' a)) = a
type PatternVarOut (NamedArg (Pattern' a)) Source # |
Instance details Defined in Agda.Syntax.Internal type PatternVarOut (NamedArg (Pattern' a)) = a
type PatternVarOut [a] Source # |
Instance details Defined in Agda.Syntax.Internal type PatternVarOut [a] = PatternVarOut a

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

Retrieve the PatternInfo from a pattern

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

Retrieve the origin of a pattern

type PatternSubstitution = Substitution' DeBruijnPattern Source #

data EqualityView Source #

View type as equality type.

Constructors

EqualityViewType EqualityTypeData | A type of the form `u ≡ v` decomposed into its parts. Used as type for the `rewrite` expression.
OtherType Type | A reduced type used as type for a `with` expression.
IdiomType Type | A reduced type used as type for the `with` inspect idiom.

#### Instances

Instances details

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 #
Free EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => EqualityView -> FreeM a c Source #
EqualityUnview EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Monad.Builtin Methods equalityUnview :: EqualityView -> Type Source #
PrettyTCM EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => EqualityView -> m Doc Source #
Instantiate EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: EqualityView -> ReduceM EqualityView 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 #
Reduce EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: EqualityView -> ReduceM EqualityView Source # reduceB' :: EqualityView -> ReduceM (Blocked EqualityView) Source #
Simplify EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: EqualityView -> ReduceM EqualityView
Subst EqualityView Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg EqualityView |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg EqualityView = Term

Methods

applySubst :: Substitution' (SubstArg EqualityView) -> EqualityView -> EqualityView Source #

type SubstArg EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg EqualityView = Term

data EqualityTypeData Source #

Constructors

EqualityTypeData |

Fields

- _eqtRange :: Range

  Range of the `rewrite` expression, if any.

- _eqtSort :: Sort

  Sort of this type.

- _eqtName :: QName

  Builtin EQUALITY.

- _eqtParams :: Args

  Hidden. Empty or `Level`.

- _eqtType :: Arg Term

  Hidden.

- _eqtLhs :: Arg Term

  NotHidden.

- _eqtRhs :: Arg Term

  NotHidden.

#### Instances

Instances details

EqualityUnview EqualityTypeData Source # |
Instance details Defined in Agda.TypeChecking.Monad.Builtin Methods equalityUnview :: EqualityTypeData -> Type Source #
Subst EqualityTypeData Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg EqualityTypeData |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg EqualityTypeData = Term

Methods

applySubst :: Substitution' (SubstArg EqualityTypeData) -> EqualityTypeData -> EqualityTypeData Source #

type SubstArg EqualityTypeData Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg EqualityTypeData = Term

pattern EqualityType :: Range -> Sort -> QName -> Args -> Arg Term -> Arg Term -> Arg Term -> EqualityView Source #

eqtRange :: EqualityView -> Range Source #

eqtSort :: EqualityView -> Sort Source #

eqtName :: EqualityView -> QName Source #

eqtParams :: EqualityView -> Args Source #

eqtType :: EqualityView -> Arg Term Source #

eqtLhs :: EqualityView -> Arg Term Source #

eqtRhs :: EqualityView -> Arg Term Source #

isEqualityType :: EqualityView -> Bool Source #

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

isPathType :: PathView -> Bool Source #

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 Source # show :: IntervalView -> String Source # showList :: [IntervalView] -> ShowS Source #

isIOne :: IntervalView -> Bool Source #

absurdBody :: Abs Term Source #

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

isAbsurdBody :: Abs Term -> Bool Source #

isAbsurdPatternName :: PatVarName -> Bool Source #

dontCare :: Term -> Term Source #

Add `DontCare` is it is not already a `DontCare`.

type DummyTermKind = String Source #

dummyLocName :: CallStack -> String Source #

Construct a string representing the call-site that created the dummy thing.

dummyTermWith :: DummyTermKind -> CallStack -> Term Source #

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

__DUMMY_TERM_WITH__ :: HasCallStack => DummyTermKind -> Term Source #

dummyTerm :: CallStack -> Term Source #

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

__DUMMY_TERM__ :: HasCallStack => Term Source #

dummyLevel :: CallStack -> Level Source #

A dummy level to constitute a level/sort created at location. Note: use macro DUMMY_LEVEL !

atomicLevel :: t -> Level' t Source #

__DUMMY_LEVEL__ :: HasCallStack => Level Source #

dummySort :: CallStack -> Sort Source #

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

__DUMMY_SORT__ :: HasCallStack => Sort Source #

dummyType :: CallStack -> Type Source #

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

__DUMMY_TYPE__ :: HasCallStack => Type Source #

dummyDom :: CallStack -> Dom Type Source #

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

__DUMMY_DOM__ :: HasCallStack => Dom Type Source #

pattern ClosedLevel :: Integer -> Level Source #

Constant level `n`

varSort :: Int -> Sort Source #

tmSort :: Term -> Sort Source #

tmSSort :: 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 #

mkSSet :: Integer -> Sort Source #

impossibleTerm :: CallStack -> Term Source #

isSort :: Term -> Maybe Sort Source #

sortUniv :: Sort' t -> Maybe Univ Source #

Get the flavor of the universe. `Nothing` could also mean "don't know".

isProp :: Sort' t -> Bool Source #

Is this a Prop universe? Answers are yes (`True`) or maybe (`False`).

isStrictDataSort :: Sort' t -> Bool Source #

Is this a strict universe inhabitable by data types?

propToType :: Sort' t -> Sort' t Source #

Turn a known `UProp` sort into a `UType` sort, leave others unchanged.

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 #

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

Telescope as list.

type ListTel = ListTel' ArgName Source #

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

telFromList :: ListTel -> Telescope Source #

Convert a list telescope to a telescope.

listTel :: Lens' Telescope ListTel Source #

Lens to edit a `Telescope` as a list.

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 #

class SgTel a where Source #

Constructing a singleton telescope.

Methods

sgTel :: a -> Telescope Source #

#### Instances

Instances details

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

stripDontCare :: Term -> Term Source #

Removing a topmost `DontCare` constructor.

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 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 String Source # |
Instance details Defined in Agda.Syntax.Internal Methods suggestName :: String -> Maybe String Source #
Suggest (Abs b) Source # |
Instance details Defined in Agda.Syntax.Internal Methods suggestName :: Abs b -> Maybe String Source #

data Suggestion Source #

Constructors

Suggest a => Suggestion a |

suggests :: [Suggestion] -> String Source #

unSpine :: Term -> Term Source #

Convert top-level postfix projections into prefix projections.

unSpine' :: (ProjOrigin -> QName -> 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.

type family TypeOf a Source #

#### Instances

Instances details

type TypeOf Elims Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf Elims = (Type, Elims -> Term)
type TypeOf Level Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf Level = ()
type TypeOf PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf PlusLevel = ()
type TypeOf Sort Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf Sort = ()
type TypeOf Term Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf Term = Type
type TypeOf Type Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf Type = ()
type TypeOf NLPat Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base type TypeOf NLPat = Type
type TypeOf (Arg a) Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf (Arg a) = Dom (TypeOf a)
type TypeOf (Abs Term) Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf (Abs Term) = (Dom Type, Abs Type)
type TypeOf (Abs Type) Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf (Abs Type) = Dom Type
type TypeOf (Dom a) Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf (Dom a) = TypeOf a
type TypeOf [PlusLevel] Source # |
Instance details Defined in Agda.Syntax.Internal type TypeOf [PlusLevel] = ()
type TypeOf [Elim' NLPat] Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base type TypeOf [Elim' NLPat] = (Type, Elims -> Term)

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

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

module Agda.Syntax.Internal.Blockers

module Agda.Syntax.Internal.Elim

module Agda.Syntax.Internal.Univ

module Agda.Syntax.Abstract.Name

data MetaId Source #

Meta-variable identifiers use the same structure as `NameId`s.

Constructors

MetaId |

Fields

- metaId :: !Word64
- metaModule :: !ModuleNameHash

#### Instances

Instances details

EncodeTCM MetaId Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: MetaId -> TCM Value Source #
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 #
NamesIn MetaId Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> MetaId -> m Source #
Reify MetaId Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo MetaId |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo MetaId = Expr

Methods

reify :: MonadReify m => MetaId -> m (ReifiesTo MetaId) Source #

reifyWhen :: MonadReify m => Bool -> MetaId -> m (ReifiesTo MetaId) Source #

HasFresh MetaId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' TCState MetaId Source # nextFresh' :: MetaId -> MetaId Source #
IsInstantiatedMeta MetaId Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: ReadTCState m => MetaId -> m Bool Source #
UnFreezeMeta MetaId Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => MetaId -> m () Source #
PrettyTCM MetaId Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => MetaId -> m Doc Source #
FromTerm MetaId Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction MetaId) Source #
PrimTerm MetaId Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: MetaId -> TCM Term Source #
PrimType MetaId Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primType :: MetaId -> TCM Type Source #
ToTerm MetaId Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (MetaId -> ReduceM Term) Source #
EmbPrj MetaId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: MetaId -> S Word32 Source # icod_ :: MetaId -> S Word32 Source # value :: Word32 -> R MetaId Source #
Unquote MetaId Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM MetaId Source #
ToJSON MetaId Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: MetaId -> Value Source # toEncoding :: MetaId -> Encoding Source # toJSONList :: [MetaId] -> Value Source # toEncodingList :: [MetaId] -> Encoding Source # omitField :: MetaId -> Bool Source #
NFData MetaId Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: MetaId -> () Source #
Enum MetaId Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

succ :: MetaId -> MetaId Source #

pred :: MetaId -> MetaId Source #

toEnum :: Int -> MetaId Source #

fromEnum :: MetaId -> Int Source #

enumFrom :: MetaId -> [MetaId] Source #

enumFromThen :: MetaId -> MetaId -> [MetaId] Source #

enumFromTo :: MetaId -> MetaId -> [MetaId] Source #

enumFromThenTo :: MetaId -> MetaId -> MetaId -> [MetaId] Source #

Generic MetaId Source # |

Instance details

Defined in Agda.Syntax.Common

Associated Types

type Rep MetaId |
Instance details Defined in Agda.Syntax.Common type Rep MetaId = D1 ('MetaData "MetaId" "Agda.Syntax.Common" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "MetaId" 'PrefixI 'True) (S1 ('MetaSel ('Just "metaId") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Word64) :*: S1 ('MetaSel ('Just "metaModule") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 ModuleNameHash)))

Methods

from :: MetaId -> Rep MetaId x Source #

to :: Rep MetaId x -> MetaId Source #

Show MetaId Source # | The record selectors are not included in the resulting strings.
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> MetaId -> ShowS Source # show :: MetaId -> String Source # showList :: [MetaId] -> ShowS Source #
Eq MetaId Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: MetaId -> MetaId -> Bool Source # (/=) :: MetaId -> MetaId -> Bool Source #
Ord MetaId Source # |
Instance details Defined in Agda.Syntax.Common Methods compare :: MetaId -> MetaId -> Ordering Source # (<) :: MetaId -> MetaId -> Bool Source # (<=) :: MetaId -> MetaId -> Bool Source # (>) :: MetaId -> MetaId -> Bool Source # (>=) :: MetaId -> MetaId -> Bool Source # max :: MetaId -> MetaId -> MetaId Source # min :: MetaId -> MetaId -> MetaId Source #
Hashable MetaId Source # |
Instance details Defined in Agda.Syntax.Common Methods hashWithSalt :: Int -> MetaId -> Int Source # hash :: MetaId -> Int Source #
Singleton MetaId MetaSet Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods singleton :: MetaId -> MetaSet Source #
Singleton MetaId () Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods singleton :: MetaId -> () Source #
InstantiateFull (Judgement MetaId) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Judgement MetaId -> ReduceM (Judgement MetaId) Source #
type ReifiesTo MetaId Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo MetaId = Expr
type Rep MetaId Source # |
Instance details Defined in Agda.Syntax.Common type Rep MetaId = D1 ('MetaData "MetaId" "Agda.Syntax.Common" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "MetaId" 'PrefixI 'True) (S1 ('MetaSel ('Just "metaId") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Word64) :*: S1 ('MetaSel ('Just "metaModule") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 ModuleNameHash)))

newtype ProblemId Source #

A "problem" consists of a set of constraints and the same constraint can be part of multiple problems.

Constructors

ProblemId Nat |

#### Instances

Instances details

EncodeTCM ProblemId Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: ProblemId -> TCM Value Source #
Pretty ProblemId Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: ProblemId -> Doc Source # prettyPrec :: Int -> ProblemId -> Doc Source # prettyList :: [ProblemId] -> Doc Source #
HasFresh ProblemId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' TCState ProblemId Source # nextFresh' :: ProblemId -> ProblemId Source #
PrettyTCM ProblemId Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ProblemId -> m Doc Source #
EmbPrj ProblemId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ProblemId -> S Word32 Source # icod_ :: ProblemId -> S Word32 Source # value :: Word32 -> R ProblemId Source #
ToJSON ProblemId Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: ProblemId -> Value Source # toEncoding :: ProblemId -> Encoding Source # toJSONList :: [ProblemId] -> Value Source # toEncodingList :: [ProblemId] -> Encoding Source # omitField :: ProblemId -> Bool Source #
NFData ProblemId Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: ProblemId -> () Source #
Enum ProblemId Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

succ :: ProblemId -> ProblemId Source #

pred :: ProblemId -> ProblemId Source #

toEnum :: Int -> ProblemId Source #

fromEnum :: ProblemId -> Int Source #

enumFrom :: ProblemId -> [ProblemId] Source #

enumFromThen :: ProblemId -> ProblemId -> [ProblemId] Source #

enumFromTo :: ProblemId -> ProblemId -> [ProblemId] Source #

enumFromThenTo :: ProblemId -> ProblemId -> ProblemId -> [ProblemId] Source #

Num ProblemId Source # |
Instance details Defined in Agda.Syntax.Common Methods (+) :: ProblemId -> ProblemId -> ProblemId Source # (-) :: ProblemId -> ProblemId -> ProblemId Source # (*) :: ProblemId -> ProblemId -> ProblemId Source # negate :: ProblemId -> ProblemId Source # abs :: ProblemId -> ProblemId Source # signum :: ProblemId -> ProblemId Source # fromInteger :: Integer -> ProblemId Source #
Integral ProblemId Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

quot :: ProblemId -> ProblemId -> ProblemId Source #

rem :: ProblemId -> ProblemId -> ProblemId Source #

div :: ProblemId -> ProblemId -> ProblemId Source #

mod :: ProblemId -> ProblemId -> ProblemId Source #

quotRem :: ProblemId -> ProblemId -> (ProblemId, ProblemId) Source #

divMod :: ProblemId -> ProblemId -> (ProblemId, ProblemId) Source #

toInteger :: ProblemId -> Integer Source #

Real ProblemId Source # |
Instance details Defined in Agda.Syntax.Common Methods toRational :: ProblemId -> Rational Source #
Show ProblemId Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> ProblemId -> ShowS Source # show :: ProblemId -> String Source # showList :: [ProblemId] -> ShowS Source #
Eq ProblemId Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: ProblemId -> ProblemId -> Bool Source # (/=) :: ProblemId -> ProblemId -> Bool Source #
Ord ProblemId Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

compare :: ProblemId -> ProblemId -> Ordering Source #

(<) :: ProblemId -> ProblemId -> Bool Source #

(<=) :: ProblemId -> ProblemId -> Bool Source #

(>) :: ProblemId -> ProblemId -> Bool Source #

(>=) :: ProblemId -> ProblemId -> Bool Source #

max :: ProblemId -> ProblemId -> ProblemId Source #

min :: ProblemId -> ProblemId -> ProblemId Source #

Monad m => MonadFresh ProblemId (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods fresh :: PureConversionT m ProblemId Source #

# Orphan instances

NFData IsFibrant Source # |
Instance details Methods rnf :: IsFibrant -> () Source #