Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Agda.Syntax.Common
Contents
Description
Some common syntactic entities are defined in this module.
Synopsis
- data Hiding
- data Arg e = Arg {}
- type Nat = Int
- newtype InteractionId = InteractionId {
- interactionId :: Nat
- data Modality = Modality {}
- newtype ProblemId = ProblemId Nat
- data Fixity = Fixity {}
- data MetaId = MetaId {
- metaId :: !Word64
- metaModule :: !ModuleNameHash
- data Ranged a = Ranged {
- rangeOf :: Range
- rangedThing :: a
- data TerminationCheck m
- type Notation = [NotationPart]
- data Lock
- data Cubical
- type NamedArg a = Arg (Named_ a)
- data ImportedName' n m
- = ImportedModule m
- | ImportedName n
- data ConOrigin
- data ProjOrigin
- data Relevance
- data NameId = NameId !Word64 !ModuleNameHash
- data WithHiding a = WithHiding {}
- data Associativity
- newtype Constr a = Constr a
- data Overlappable
- type Arity = Nat
- data FileType
- data Language
- data RecordDirectives' a = RecordDirectives {
- recInductive :: Maybe (Ranged Induction)
- recHasEta :: Maybe HasEta0
- recPattern :: Maybe Range
- recConstructor :: Maybe a
- type HasEta0 = HasEta' ()
- data HasEta' a
- type HasEta = HasEta' PatternOrCopattern
- data PatternOrCopattern
- class PatternMatchingAllowed a where
- patternMatchingAllowed :: a -> Bool
- class CopatternMatchingAllowed a where
- copatternMatchingAllowed :: a -> Bool
- class LensHiding a where
- class LensArgInfo a where
- getArgInfo :: a -> ArgInfo
- setArgInfo :: ArgInfo -> a -> a
- mapArgInfo :: (ArgInfo -> ArgInfo) -> a -> a
- data Named name a = Named {
- nameOf :: Maybe name
- namedThing :: a
- newtype UnderAddition t = UnderAddition t
- newtype UnderComposition t = UnderComposition t
- data Quantity
- data Cohesion
- = Flat
- | Continuous
- | Squash
- class LensModality a where
- getModality :: a -> Modality
- setModality :: Modality -> a -> a
- mapModality :: (Modality -> Modality) -> a -> a
- class LensRelevance a where
- getRelevance :: a -> Relevance
- setRelevance :: Relevance -> a -> a
- mapRelevance :: (Relevance -> Relevance) -> a -> a
- class LensQuantity a where
- getQuantity :: a -> Quantity
- setQuantity :: Quantity -> a -> a
- mapQuantity :: (Quantity -> Quantity) -> a -> a
- class LensCohesion a where
- getCohesion :: a -> Cohesion
- setCohesion :: Cohesion -> a -> a
- mapCohesion :: (Cohesion -> Cohesion) -> a -> a
- data Q0Origin
- = Q0Inferred
- | Q0 Range
- | Q0Erased Range
- data Q1Origin
- = Q1Inferred
- | Q1 Range
- | Q1Linear Range
- data QωOrigin
- = QωInferred
- | Qω Range
- | QωPlenty Range
- data Erased
- data Annotation = Annotation {}
- class LensAnnotation a where
- getAnnotation :: a -> Annotation
- setAnnotation :: Annotation -> a -> a
- mapAnnotation :: (Annotation -> Annotation) -> a -> a
- data LockOrigin
- class LensLock a where
- data ArgInfo = ArgInfo {}
- data Origin
- data WithOrigin a = WithOrigin {}
- class LensOrigin a where
- data FreeVariables
- = UnknownFVs
- | KnownFVs IntSet
- class LensFreeVariables a where
- getFreeVariables :: a -> FreeVariables
- setFreeVariables :: FreeVariables -> a -> a
- mapFreeVariables :: (FreeVariables -> FreeVariables) -> a -> a
- class Eq a => Underscore a where
- underscore :: a
- isUnderscore :: a -> Bool
- type Named_ = Named NamedName
- type NamedName = WithOrigin (Ranged ArgName)
- type ArgName = String
- class LensNamed a where
- type RawName = String
- type RString = Ranged RawName
- data IsInfix
- data Access
- data IsAbstract
- class LensIsAbstract a where
- class AnyIsAbstract a where
- anyIsAbstract :: a -> IsAbstract
- data IsInstance
- data IsMacro
- data IsOpaque
- data OpaqueId = OpaqueId !Word64 !ModuleNameHash
- class LensIsOpaque a where
- lensIsOpaque :: Lens' a IsOpaque
- data JointOpacity
- = UniqueOpaque !OpaqueId
- | DifferentOpaque !(HashSet OpaqueId)
- | NoOpaque
- class AllAreOpaque a where
- jointOpacity :: a -> JointOpacity
- newtype ModuleNameHash = ModuleNameHash {
- moduleNameHash :: Word64
- data PositionInName
- data MaybePlaceholder e
- = Placeholder !PositionInName
- | NoPlaceholder !(Maybe PositionInName) e
- type PrecedenceLevel = Double
- data FixityLevel
- data Fixity' = Fixity' {
- theFixity :: !Fixity
- theNotation :: Notation
- theNameRange :: Range
- class LensFixity a where
- lensFixity :: Lens' a Fixity
- class LensFixity' a where
- lensFixity' :: Lens' a Fixity'
- data ImportDirective' n m = ImportDirective {
- importDirRange :: Range
- using :: Using' n m
- hiding :: HidingDirective' n m
- impRenaming :: RenamingDirective' n m
- publicOpen :: Maybe Range
- data Using' n m
- = UseEverything
- | Using [ImportedName' n m]
- type HidingDirective' n m = [ImportedName' n m]
- type RenamingDirective' n m = [Renaming' n m]
- data Renaming' n m = Renaming {
- renFrom :: ImportedName' n m
- renTo :: ImportedName' n m
- renFixity :: Maybe Fixity
- renToRange :: Range
- data PositivityCheck
- data UniverseCheck
- data CoverageCheck
- data RewriteEqn' qn nm p e
- data ExpandedEllipsis
- = ExpandedEllipsis {
- ellipsisRange :: Range
- ellipsisWithArgs :: Int
- | NoEllipsis
- = ExpandedEllipsis {
- data NotationPart
- data BoundVariablePosition = BoundVariablePosition {
- holeNumber :: !Int
- varNumber :: !Int
- fromImportedName :: ImportedName' a a -> a
- partitionImportedNames :: [ImportedName' n m] -> ([n], [m])
- defaultArgInfo :: ArgInfo
- defaultArg :: a -> Arg a
- hasQuantity0 :: LensQuantity a => a -> Bool
- defaultFixity :: Fixity
- isInstance :: LensHiding a => a -> Bool
- emptyRecordDirectives :: RecordDirectives' a
- hidingToString :: Hiding -> String
- mergeHiding :: LensHiding a => WithHiding a -> a
- visible :: LensHiding a => a -> Bool
- notVisible :: LensHiding a => a -> Bool
- hidden :: LensHiding a => a -> Bool
- hide :: LensHiding a => a -> a
- hideOrKeepInstance :: LensHiding a => a -> a
- makeInstance :: LensHiding a => a -> a
- makeInstance' :: LensHiding a => Overlappable -> a -> a
- isOverlappable :: LensHiding a => a -> Bool
- sameHiding :: (LensHiding a, LensHiding b) => a -> b -> Bool
- composeModality :: Modality -> Modality -> Modality
- unitModality :: Modality
- inverseComposeModality :: Modality -> Modality -> Modality
- addModality :: Modality -> Modality -> Modality
- zeroModality :: Modality
- moreUsableModality :: Modality -> Modality -> Bool
- usableModality :: LensModality a => a -> Bool
- usableRelevance :: LensRelevance a => a -> Bool
- usableQuantity :: LensQuantity a => a -> Bool
- usableCohesion :: LensCohesion a => a -> Bool
- composeRelevance :: Relevance -> Relevance -> Relevance
- composeQuantity :: Quantity -> Quantity -> Quantity
- composeCohesion :: Cohesion -> Cohesion -> Cohesion
- applyModality :: LensModality a => Modality -> a -> a
- inverseComposeRelevance :: Relevance -> Relevance -> Relevance
- inverseComposeQuantity :: Quantity -> Quantity -> Quantity
- inverseComposeCohesion :: Cohesion -> Cohesion -> Cohesion
- inverseApplyModalityButNotQuantity :: LensModality a => Modality -> a -> a
- addRelevance :: Relevance -> Relevance -> Relevance
- addQuantity :: Quantity -> Quantity -> Quantity
- addCohesion :: Cohesion -> Cohesion -> Cohesion
- zeroRelevance :: Relevance
- zeroQuantity :: Quantity
- zeroCohesion :: Cohesion
- unitRelevance :: Relevance
- unitQuantity :: Quantity
- unitCohesion :: Cohesion
- topModality :: Modality
- topRelevance :: Relevance
- topQuantity :: Quantity
- topCohesion :: Cohesion
- defaultModality :: Modality
- defaultRelevance :: Relevance
- defaultQuantity :: Quantity
- defaultCohesion :: Cohesion
- sameModality :: (LensModality a, LensModality b) => a -> b -> Bool
- sameRelevance :: Relevance -> Relevance -> Bool
- sameQuantity :: Quantity -> Quantity -> Bool
- sameCohesion :: Cohesion -> Cohesion -> Bool
- lModRelevance :: Lens' Modality Relevance
- lModQuantity :: Lens' Modality Quantity
- lModCohesion :: Lens' Modality Cohesion
- getRelevanceMod :: LensModality a => LensGet a Relevance
- setRelevanceMod :: LensModality a => LensSet a Relevance
- mapRelevanceMod :: LensModality a => LensMap a Relevance
- getQuantityMod :: LensModality a => LensGet a Quantity
- setQuantityMod :: LensModality a => LensSet a Quantity
- mapQuantityMod :: LensModality a => LensMap a Quantity
- getCohesionMod :: LensModality a => LensGet a Cohesion
- setCohesionMod :: LensModality a => LensSet a Cohesion
- mapCohesionMod :: LensModality a => LensMap a Cohesion
- moreQuantity :: Quantity -> Quantity -> Bool
- applyQuantity :: LensQuantity a => Quantity -> a -> a
- inverseApplyQuantity :: LensQuantity a => Quantity -> a -> a
- hasQuantity1 :: LensQuantity a => a -> Bool
- hasQuantityω :: LensQuantity a => a -> Bool
- noUserQuantity :: LensQuantity a => a -> Bool
- defaultErased :: Erased
- asQuantity :: Erased -> Quantity
- erasedFromQuantity :: Quantity -> Maybe Erased
- sameErased :: Erased -> Erased -> Bool
- isErased :: Erased -> Bool
- composeErased :: Erased -> Erased -> Erased
- allRelevances :: [Relevance]
- isRelevant :: LensRelevance a => a -> Bool
- isIrrelevant :: LensRelevance a => a -> Bool
- isNonStrict :: LensRelevance a => a -> Bool
- moreRelevant :: Relevance -> Relevance -> Bool
- applyRelevance :: LensRelevance a => Relevance -> a -> a
- inverseApplyRelevance :: LensRelevance a => Relevance -> a -> a
- irrToNonStrict :: Relevance -> Relevance
- nonStrictToRel :: Relevance -> Relevance
- nonStrictToIrr :: Relevance -> Relevance
- defaultAnnotation :: Annotation
- defaultLock :: Lock
- allCohesions :: [Cohesion]
- moreCohesion :: Cohesion -> Cohesion -> Bool
- applyCohesion :: LensCohesion a => Cohesion -> a -> a
- inverseApplyCohesion :: LensCohesion a => Cohesion -> a -> a
- unknownFreeVariables :: FreeVariables
- noFreeVariables :: FreeVariables
- oneFreeVariable :: Int -> FreeVariables
- freeVariablesFromList :: [Int] -> FreeVariables
- hasNoFreeVariables :: LensFreeVariables a => a -> Bool
- getHidingArgInfo :: LensArgInfo a => LensGet a Hiding
- setHidingArgInfo :: LensArgInfo a => LensSet a Hiding
- mapHidingArgInfo :: LensArgInfo a => LensMap a Hiding
- getModalityArgInfo :: LensArgInfo a => LensGet a Modality
- setModalityArgInfo :: LensArgInfo a => LensSet a Modality
- mapModalityArgInfo :: LensArgInfo a => LensMap a Modality
- getOriginArgInfo :: LensArgInfo a => LensGet a Origin
- setOriginArgInfo :: LensArgInfo a => LensSet a Origin
- mapOriginArgInfo :: LensArgInfo a => LensMap a Origin
- getFreeVariablesArgInfo :: LensArgInfo a => LensGet a FreeVariables
- setFreeVariablesArgInfo :: LensArgInfo a => LensSet a FreeVariables
- mapFreeVariablesArgInfo :: LensArgInfo a => LensMap a FreeVariables
- isInsertedHidden :: (LensHiding a, LensOrigin a) => a -> Bool
- withArgsFrom :: [a] -> [Arg b] -> [Arg a]
- withNamedArgsFrom :: [a] -> [NamedArg b] -> [NamedArg a]
- sameName :: NamedName -> NamedName -> Bool
- unnamed :: a -> Named name a
- isUnnamed :: Named name a -> Maybe a
- named :: name -> a -> Named name a
- userNamed :: Ranged ArgName -> a -> Named_ a
- getNameOf :: LensNamed a => a -> Maybe (NameOf a)
- setNameOf :: LensNamed a => Maybe (NameOf a) -> a -> a
- mapNameOf :: LensNamed a => (Maybe (NameOf a) -> Maybe (NameOf a)) -> a -> a
- bareNameOf :: (LensNamed a, NameOf a ~ NamedName) => a -> Maybe ArgName
- bareNameWithDefault :: (LensNamed a, NameOf a ~ NamedName) => ArgName -> a -> ArgName
- namedSame :: (LensNamed a, LensNamed b, NameOf a ~ NamedName, NameOf b ~ NamedName) => a -> b -> Bool
- fittingNamedArg :: (LensNamed arg, NameOf arg ~ NamedName, LensHiding arg, LensNamed dom, NameOf dom ~ NamedName, LensHiding dom) => arg -> dom -> Maybe Bool
- namedArg :: NamedArg a -> a
- defaultNamedArg :: a -> NamedArg a
- unnamedArg :: ArgInfo -> a -> NamedArg a
- updateNamedArg :: (a -> b) -> NamedArg a -> NamedArg b
- updateNamedArgA :: Applicative f => (a -> f b) -> NamedArg a -> f (NamedArg b)
- setNamedArg :: NamedArg a -> b -> NamedArg b
- argNameToString :: ArgName -> String
- stringToArgName :: String -> ArgName
- appendArgNames :: ArgName -> ArgName -> ArgName
- unranged :: a -> Ranged a
- rawNameToString :: RawName -> String
- stringToRawName :: String -> RawName
- bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin
- noModuleNameHash :: ModuleNameHash
- noPlaceholder :: e -> MaybePlaceholder e
- noFixity :: Fixity
- noFixity' :: Fixity'
- noNotation :: Notation
- _fixityAssoc :: Lens' Fixity Associativity
- _fixityLevel :: Lens' Fixity FixityLevel
- defaultImportDir :: ImportDirective' n m
- isDefaultImportDir :: ImportDirective' n m -> Bool
- mapUsing :: ([ImportedName' n1 m1] -> [ImportedName' n2 m2]) -> Using' n1 m1 -> Using' n2 m2
- setImportedName :: ImportedName' a a -> a -> ImportedName' a a
- data Induction
Documentation
Constructors
Hidden | |
Instance Overlappable | |
NotHidden |
Instances
LensHiding Hiding Source # | |
Pretty Hiding Source # | |
HasRange Hiding Source # | |
KillRange Hiding Source # | |
Defined in Agda.Syntax.Common Methods | |
Verbalize Hiding Source # | |
Defined in Agda.TypeChecking.Errors | |
ChooseFlex Hiding Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: Hiding -> Hiding -> FlexChoice Source # | |
EmbPrj Hiding Source # | |
Unquote Hiding Source # | |
Monoid Hiding Source # | |
Semigroup Hiding Source # |
|
Show Hiding Source # | |
NFData Hiding Source # | |
Defined in Agda.Syntax.Common | |
Eq Hiding Source # | |
Ord Hiding Source # | |
Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b) Source # | |
Instances
newtype InteractionId Source #
Constructors
InteractionId | |
Fields
|
Instances
We have a tuple of modalities, which might not be fully orthogonal. For example, irrelevant stuff is also run-time irrelevant.
Constructors
Modality | |
Fields
|
Instances
A "problem" consists of a set of constraints and the same constraint can be part of multiple problems.
Instances
EncodeTCM ProblemId Source # | |
Pretty ProblemId Source # | |
HasFresh ProblemId Source # | |
PrettyTCM ProblemId Source # | |
Defined in Agda.TypeChecking.Pretty | |
Enum ProblemId Source # | |
Defined in Agda.Syntax.Common | |
Num ProblemId Source # | |
Integral ProblemId Source # | |
Defined in Agda.Syntax.Common | |
Real ProblemId Source # | |
Defined in Agda.Syntax.Common Methods toRational :: ProblemId -> Rational | |
Show ProblemId Source # | |
NFData ProblemId Source # | |
Defined in Agda.Syntax.Common | |
Eq ProblemId Source # | |
Ord ProblemId Source # | |
Defined in Agda.Syntax.Common | |
ToJSON ProblemId Source # | |
Defined in Agda.Interaction.JSONTop | |
Monad m => MonadFresh ProblemId (PureConversionT m) Source # | |
Defined in Agda.TypeChecking.Conversion.Pure Methods fresh :: PureConversionT m ProblemId Source # |
Fixity of operators.
Constructors
Fixity | |
Fields
|
Instances
LensFixity Fixity Source # | |
Defined in Agda.Syntax.Common | |
Pretty Fixity Source # | |
HasRange Fixity Source # | |
KillRange Fixity Source # | |
Defined in Agda.Syntax.Common Methods | |
ToTerm Fixity Source # | |
EmbPrj Fixity Source # | |
Null Fixity Source # | |
Show Fixity Source # | |
NFData Fixity Source # | |
Defined in Agda.Syntax.Common | |
Eq Fixity Source # | |
Ord Fixity Source # | |
Meta-variable identifiers use the same structure as NameId
s.
Constructors
MetaId | |
Fields
|
Instances
Thing with range info.
Constructors
Ranged | |
Fields
|
Instances
data TerminationCheck m Source #
Termination check? (Default = TerminationCheck).
Constructors
TerminationCheck | Run the termination checker. |
NoTerminationCheck | Skip termination checking (unsafe). |
NonTerminating | Treat as non-terminating. |
Terminating | Treat as terminating (unsafe). Same effect as |
TerminationMeasure Range m | Skip termination checking but use measure instead. |
Instances
Functor TerminationCheck Source # | |
Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> TerminationCheck a -> TerminationCheck b (<$) :: a -> TerminationCheck b -> TerminationCheck a # | |
KillRange m => KillRange (TerminationCheck m) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (TerminationCheck m) Source # | |
Show m => Show (TerminationCheck m) Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> TerminationCheck m -> ShowS show :: TerminationCheck m -> String showList :: [TerminationCheck m] -> ShowS | |
NFData a => NFData (TerminationCheck a) Source # | |
Defined in Agda.Syntax.Common Methods rnf :: TerminationCheck a -> () | |
Eq m => Eq (TerminationCheck m) Source # | |
Defined in Agda.Syntax.Common Methods (==) :: TerminationCheck m -> TerminationCheck m -> Bool (/=) :: TerminationCheck m -> TerminationCheck m -> Bool |
type Notation = [NotationPart] Source #
Notation as provided by the syntax
declaration.
Constructors
IsNotLock | |
IsLock LockOrigin | In the future there might be different kinds of them. For now we assume lock weakening. |
Instances
LensLock Lock Source # | |
EmbPrj Lock Source # | |
Generic Lock Source # | |
Show Lock Source # | |
NFData Lock Source # | |
Defined in Agda.Syntax.Common | |
Eq Lock Source # | |
Ord Lock Source # | |
type Rep Lock Source # | |
Defined in Agda.Syntax.Common type Rep Lock = D1 ('MetaData "Lock" "Agda.Syntax.Common" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "IsNotLock" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsLock" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LockOrigin))) |
Variants of Cubical Agda.
Instances
EmbPrj Cubical Source # | |
Generic Cubical Source # | |
Show Cubical Source # | |
NFData Cubical Source # | |
Defined in Agda.Syntax.Common | |
Eq Cubical Source # | |
type Rep Cubical Source # | |
Defined in Agda.Syntax.Common type Rep Cubical = D1 ('MetaData "Cubical" "Agda.Syntax.Common" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "CErased" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CFull" 'PrefixI 'False) (U1 :: Type -> Type)) |
data ImportedName' n m Source #
An imported name can be a module or a defined name.
Constructors
ImportedModule m | Imported module name of type |
ImportedName n | Imported name of type |
Instances
Where does the ConP
or Con
come from?
Constructors
ConOSystem | Inserted by system or expanded from an implicit pattern. |
ConOCon | User wrote a constructor (pattern). |
ConORec | User wrote a record (pattern). |
ConOSplit | Generated by interactive case splitting. |
Instances
KillRange ConOrigin Source # | |
Defined in Agda.Syntax.Common Methods | |
EmbPrj ConOrigin Source # | |
Bounded ConOrigin Source # | |
Defined in Agda.Syntax.Common | |
Enum ConOrigin Source # | |
Defined in Agda.Syntax.Common | |
Generic ConOrigin Source # | |
Show ConOrigin Source # | |
NFData ConOrigin Source # | |
Defined in Agda.Syntax.Common | |
Eq ConOrigin Source # | |
Ord ConOrigin Source # | |
Defined in Agda.Syntax.Common | |
type Rep ConOrigin Source # | |
Defined in Agda.Syntax.Common type Rep ConOrigin = D1 ('MetaData "ConOrigin" "Agda.Syntax.Common" "Agda-2.6.3.20230930-inplace" 'False) ((C1 ('MetaCons "ConOSystem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConOCon" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ConORec" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConOSplit" 'PrefixI 'False) (U1 :: Type -> Type))) |
data ProjOrigin Source #
Where does a projection come from?
Constructors
ProjPrefix | User wrote a prefix projection. |
ProjPostfix | User wrote a postfix projection. |
ProjSystem | Projection was generated by the system. |
Instances
A function argument can be relevant or irrelevant. See Agda.TypeChecking.Irrelevance.
Constructors
Relevant | The argument is (possibly) relevant at compile-time. |
NonStrict | The argument may never flow into evaluation position. Therefore, it is irrelevant at run-time. It is treated relevantly during equality checking. The above comment is probably obsolete, as we currently have
erasure (at0, |
Irrelevant | The argument is irrelevant at compile- and runtime. |
Instances
The unique identifier of a name. Second argument is the top-level module identifier.
Constructors
NameId !Word64 !ModuleNameHash |
Instances
Pretty NameId Source # | |
KillRange NameId Source # | |
Defined in Agda.Syntax.Common Methods | |
HasFresh NameId Source # | |
EmbPrj NameId Source # | |
Enum NameId Source # | |
Defined in Agda.Syntax.Common | |
Generic NameId Source # | |
Show NameId Source # | |
NFData NameId Source # | |
Defined in Agda.Syntax.Common | |
Eq NameId Source # | |
Ord NameId Source # | |
Hashable NameId Source # | |
Defined in Agda.Syntax.Common | |
MonadFresh NameId AbsToCon Source # | |
Monad m => MonadFresh NameId (PureConversionT m) Source # | |
Defined in Agda.TypeChecking.Conversion.Pure Methods fresh :: PureConversionT m NameId Source # | |
type Rep NameId Source # | |
Defined in Agda.Syntax.Common type Rep NameId = D1 ('MetaData "NameId" "Agda.Syntax.Common" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "NameId" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Word64) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 ModuleNameHash))) |
data WithHiding a Source #
Decorating something with Hiding
information.
Constructors
WithHiding | |
Instances
data Associativity Source #
Associativity.
Constructors
NonAssoc | |
LeftAssoc | |
RightAssoc |
Instances
Constructors
Constr a |
Instances
ToConcrete (Constr Constructor) Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Constr Constructor) Source # Methods toConcrete :: Constr Constructor -> AbsToCon (ConOfAbs (Constr Constructor)) Source # bindToConcrete :: Constr Constructor -> (ConOfAbs (Constr Constructor) -> AbsToCon b) -> AbsToCon b Source # | |
type ConOfAbs (Constr Constructor) Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete |
data Overlappable Source #
Constructors
YesOverlap | |
NoOverlap |
Instances
Constructors
AgdaFileType | |
MdFileType | |
RstFileType | |
TexFileType | |
OrgFileType | |
TypstFileType |
Instances
Pretty FileType Source # | |
EmbPrj FileType Source # | |
Generic FileType Source # | |
Show FileType Source # | |
NFData FileType Source # | |
Defined in Agda.Syntax.Common | |
Eq FileType Source # | |
Ord FileType Source # | |
Defined in Agda.Syntax.Common | |
type Rep FileType Source # | |
Defined in Agda.Syntax.Common type Rep FileType = D1 ('MetaData "FileType" "Agda.Syntax.Common" "Agda-2.6.3.20230930-inplace" 'False) ((C1 ('MetaCons "AgdaFileType" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MdFileType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RstFileType" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "TexFileType" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OrgFileType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TypstFileType" 'PrefixI 'False) (U1 :: Type -> Type)))) |
Agda variants.
Only some variants are tracked.
Instances
KillRange Language Source # | |
Defined in Agda.Syntax.Common Methods | |
EmbPrj Language Source # | |
Generic Language Source # | |
Show Language Source # | |
NFData Language Source # | |
Defined in Agda.Syntax.Common | |
Eq Language Source # | |
type Rep Language Source # | |
Defined in Agda.Syntax.Common type Rep Language = D1 ('MetaData "Language" "Agda.Syntax.Common" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "WithoutK" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "WithK" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Cubical" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Cubical)))) |
data RecordDirectives' a Source #
Constructors
RecordDirectives | |
Fields
|
Instances
Does a record come with eta-equality?
Instances
CopatternMatchingAllowed HasEta Source # | |
Defined in Agda.Syntax.Common Methods copatternMatchingAllowed :: HasEta -> Bool Source # | |
PatternMatchingAllowed HasEta Source # | |
Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: HasEta -> Bool Source # | |
Foldable HasEta' Source # | |
Defined in Agda.Syntax.Common Methods fold :: Monoid m => HasEta' m -> m foldMap :: Monoid m => (a -> m) -> HasEta' a -> m foldMap' :: Monoid m => (a -> m) -> HasEta' a -> m foldr :: (a -> b -> b) -> b -> HasEta' a -> b foldr' :: (a -> b -> b) -> b -> HasEta' a -> b foldl :: (b -> a -> b) -> b -> HasEta' a -> b foldl' :: (b -> a -> b) -> b -> HasEta' a -> b foldr1 :: (a -> a -> a) -> HasEta' a -> a foldl1 :: (a -> a -> a) -> HasEta' a -> a elem :: Eq a => a -> HasEta' a -> Bool maximum :: Ord a => HasEta' a -> a minimum :: Ord a => HasEta' a -> a | |
Traversable HasEta' Source # | |
Functor HasEta' Source # | |
HasRange a => HasRange (HasEta' a) Source # | |
KillRange a => KillRange (HasEta' a) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (HasEta' a) Source # | |
EmbPrj a => EmbPrj (HasEta' a) Source # | |
Show a => Show (HasEta' a) Source # | |
NFData a => NFData (HasEta' a) Source # | |
Defined in Agda.Syntax.Common | |
Eq a => Eq (HasEta' a) Source # | |
Ord a => Ord (HasEta' a) Source # | |
Defined in Agda.Syntax.Common |
type HasEta = HasEta' PatternOrCopattern Source #
Pattern and copattern matching is allowed in the presence of eta.
In the absence of eta, we have to choose whether we want to allow matching on the constructor or copattern matching with the projections. Having both leads to breakage of subject reduction (issue #4560).
data PatternOrCopattern Source #
For a record without eta, which type of matching do we allow?
Constructors
PatternMatching | Can match on the record constructor. |
CopatternMatching | Can copattern match using the projections. (Default.) |
Instances
class PatternMatchingAllowed a where Source #
Can we pattern match on the record constructor?
Methods
patternMatchingAllowed :: a -> Bool Source #
Instances
PatternMatchingAllowed HasEta Source # | |
Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: HasEta -> Bool Source # | |
PatternMatchingAllowed PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: PatternOrCopattern -> Bool Source # | |
PatternMatchingAllowed Induction Source # | |
Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: Induction -> Bool Source # | |
PatternMatchingAllowed DataOrRecord Source # | |
Defined in Agda.Syntax.Internal Methods patternMatchingAllowed :: DataOrRecord -> Bool Source # | |
PatternMatchingAllowed EtaEquality Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods patternMatchingAllowed :: EtaEquality -> Bool Source # |
class CopatternMatchingAllowed a where Source #
Can we construct a record by copattern matching?
Methods
copatternMatchingAllowed :: a -> Bool Source #
Instances
CopatternMatchingAllowed HasEta Source # | |
Defined in Agda.Syntax.Common Methods copatternMatchingAllowed :: HasEta -> Bool Source # | |
CopatternMatchingAllowed PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods copatternMatchingAllowed :: PatternOrCopattern -> Bool Source # | |
CopatternMatchingAllowed ConHead Source # | |
Defined in Agda.Syntax.Internal Methods copatternMatchingAllowed :: ConHead -> Bool Source # | |
CopatternMatchingAllowed DataOrRecord Source # | |
Defined in Agda.Syntax.Internal Methods copatternMatchingAllowed :: DataOrRecord -> Bool Source # | |
CopatternMatchingAllowed EtaEquality Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods copatternMatchingAllowed :: EtaEquality -> Bool Source # |
class LensHiding a where Source #
A lens to access the Hiding
attribute in data structures.
Minimal implementation: getHiding
and mapHiding
or LensArgInfo
.
Minimal complete definition
Nothing
Methods
getHiding :: a -> Hiding Source #
default getHiding :: LensArgInfo a => a -> Hiding Source #
Instances
class LensArgInfo a where Source #
Minimal complete definition
Methods
getArgInfo :: a -> ArgInfo Source #
setArgInfo :: ArgInfo -> a -> a Source #
mapArgInfo :: (ArgInfo -> ArgInfo) -> a -> a Source #
Instances
LensArgInfo ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
LensArgInfo Definition Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods getArgInfo :: Definition -> ArgInfo Source # setArgInfo :: ArgInfo -> Definition -> Definition Source # mapArgInfo :: (ArgInfo -> ArgInfo) -> Definition -> Definition Source # | |
LensArgInfo (Arg a) Source # | |
Defined in Agda.Syntax.Common | |
LensArgInfo (FlexibleVar a) Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem Methods getArgInfo :: FlexibleVar a -> ArgInfo Source # setArgInfo :: ArgInfo -> FlexibleVar a -> FlexibleVar a Source # mapArgInfo :: (ArgInfo -> ArgInfo) -> FlexibleVar a -> FlexibleVar a Source # | |
LensArgInfo (Dom' t e) Source # | |
Defined in Agda.Syntax.Internal |
Something potentially carrying a name.
Constructors
Named | |
Fields
|
Instances
newtype UnderAddition t Source #
Type wrapper to indicate additive monoid/semigroup context.
Constructors
UnderAddition t |
Instances
newtype UnderComposition t Source #
Type wrapper to indicate composition or multiplicative monoid/semigroup context.
Constructors
UnderComposition t |
Instances
Quantity for linearity.
A quantity is a set of natural numbers, indicating possible semantic
uses of a variable. A singleton set {n}
requires that the
corresponding variable is used exactly n
times.
Constructors
Quantity0 Q0Origin | Zero uses |
Quantity1 Q1Origin | Linear use |
Quantityω QωOrigin | Unrestricted use |
Instances
Cohesion modalities see "Brouwer's fixed-point theorem in real-cohesive homotopy type theory" (arXiv:1509.07584) types are now given an additional topological layer which the modalities interact with.
Constructors
Flat | same points, discrete topology, idempotent comonad, box-like. |
Continuous | identity modality. | Sharp -- ^ same points, codiscrete topology, idempotent monad, diamond-like. |
Squash | single point space, artificially added for Flat left-composition. |
Instances
class LensModality a where Source #
Minimal complete definition
Nothing
Methods
getModality :: a -> Modality Source #
default getModality :: LensArgInfo a => a -> Modality Source #
setModality :: Modality -> a -> a Source #
mapModality :: (Modality -> Modality) -> a -> a Source #
default mapModality :: LensArgInfo a => (Modality -> Modality) -> a -> a Source #
Instances
class LensRelevance a where Source #
A lens to access the Relevance
attribute in data structures.
Minimal implementation: getRelevance
and mapRelevance
or LensModality
.
Minimal complete definition
Nothing
Methods
getRelevance :: a -> Relevance Source #
default getRelevance :: LensModality a => a -> Relevance Source #
setRelevance :: Relevance -> a -> a Source #
mapRelevance :: (Relevance -> Relevance) -> a -> a Source #
default mapRelevance :: LensModality a => (Relevance -> Relevance) -> a -> a Source #
Instances
class LensQuantity a where Source #
Minimal complete definition
Nothing
Methods
getQuantity :: a -> Quantity Source #
default getQuantity :: LensModality a => a -> Quantity Source #
setQuantity :: Quantity -> a -> a Source #
mapQuantity :: (Quantity -> Quantity) -> a -> a Source #
default mapQuantity :: LensModality a => (Quantity -> Quantity) -> a -> a Source #
Instances
class LensCohesion a where Source #
A lens to access the Cohesion
attribute in data structures.
Minimal implementation: getCohesion
and mapCohesion
or LensModality
.
Minimal complete definition
Nothing
Methods
getCohesion :: a -> Cohesion Source #
default getCohesion :: LensModality a => a -> Cohesion Source #
setCohesion :: Cohesion -> a -> a Source #
mapCohesion :: (Cohesion -> Cohesion) -> a -> a Source #
default mapCohesion :: LensModality a => (Cohesion -> Cohesion) -> a -> a Source #
Instances
LensCohesion ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
LensCohesion Cohesion Source # | |
Defined in Agda.Syntax.Common | |
LensCohesion Modality Source # | |
Defined in Agda.Syntax.Common | |
LensCohesion (Arg e) Source # | |
Defined in Agda.Syntax.Common | |
LensCohesion (Dom' t e) Source # | |
Defined in Agda.Syntax.Internal |
Origin of Quantity0
.
Constructors
Q0Inferred | User wrote nothing. |
Q0 Range | User wrote "@0". |
Q0Erased Range | User wrote "@erased". |
Instances
Pretty Q0Origin Source # | |
HasRange Q0Origin Source # | |
KillRange Q0Origin Source # | |
Defined in Agda.Syntax.Common Methods | |
SetRange Q0Origin Source # | |
EmbPrj Q0Origin Source # | |
Null Q0Origin Source # | |
Monoid Q0Origin Source # | |
Semigroup Q0Origin Source # | Right-biased composition, because the left quantity acts as context, and the right one as occurrence. |
Generic Q0Origin Source # | |
Show Q0Origin Source # | |
NFData Q0Origin Source # | |
Defined in Agda.Syntax.Common | |
Eq Q0Origin Source # | |
Ord Q0Origin Source # | |
Defined in Agda.Syntax.Common | |
type Rep Q0Origin Source # | |
Defined in Agda.Syntax.Common type Rep Q0Origin = D1 ('MetaData "Q0Origin" "Agda.Syntax.Common" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "Q0Inferred" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Q0" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Q0Erased" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) |
Origin of Quantity1
.
Constructors
Q1Inferred | User wrote nothing. |
Q1 Range | User wrote "@1". |
Q1Linear Range | User wrote "@linear". |
Instances
Pretty Q1Origin Source # | |
HasRange Q1Origin Source # | |
KillRange Q1Origin Source # | |
Defined in Agda.Syntax.Common Methods | |
SetRange Q1Origin Source # | |
EmbPrj Q1Origin Source # | |
Null Q1Origin Source # | |
Monoid Q1Origin Source # | |
Semigroup Q1Origin Source # | Right-biased composition, because the left quantity acts as context, and the right one as occurrence. |
Generic Q1Origin Source # | |
Show Q1Origin Source # | |
NFData Q1Origin Source # | |
Defined in Agda.Syntax.Common | |
Eq Q1Origin Source # | |
Ord Q1Origin Source # | |
Defined in Agda.Syntax.Common | |
type Rep Q1Origin Source # | |
Defined in Agda.Syntax.Common type Rep Q1Origin = D1 ('MetaData "Q1Origin" "Agda.Syntax.Common" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "Q1Inferred" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Q1" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Q1Linear" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) |
Origin of Quantityω
.
Constructors
QωInferred | User wrote nothing. |
Qω Range | User wrote "@ω". |
QωPlenty Range | User wrote "@plenty". |
Instances
Pretty QωOrigin Source # | |
HasRange QωOrigin Source # | |
KillRange QωOrigin Source # | |
Defined in Agda.Syntax.Common Methods | |
SetRange QωOrigin Source # | |
EmbPrj QωOrigin Source # | |
Null QωOrigin Source # | |
Monoid QωOrigin Source # | |
Semigroup QωOrigin Source # | Right-biased composition, because the left quantity acts as context, and the right one as occurrence. |
Generic QωOrigin Source # | |
Show QωOrigin Source # | |
NFData QωOrigin Source # | |
Defined in Agda.Syntax.Common | |
Eq QωOrigin Source # | |
Ord QωOrigin Source # | |
Defined in Agda.Syntax.Common | |
type Rep QωOrigin Source # | |
Defined in Agda.Syntax.Common type Rep QωOrigin = D1 ('MetaData "Q\969Origin" "Agda.Syntax.Common" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "Q\969Inferred" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Q\969" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Q\969Plenty" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) |
A special case of Quantity
: erased or not.
Note that the Ord
instance does *not* ignore the origin
arguments.
Instances
Pretty Erased Source # | |
HasRange Erased Source # | |
KillRange Erased Source # | |
Defined in Agda.Syntax.Common Methods | |
PrettyTCM Erased Source # | |
Defined in Agda.TypeChecking.Pretty | |
Generic Erased Source # | |
Show Erased Source # | |
NFData Erased Source # | |
Defined in Agda.Syntax.Common | |
Eq Erased Source # | |
Ord Erased Source # | |
Semigroup (UnderComposition Erased) Source # | |
Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Erased -> UnderComposition Erased -> UnderComposition Erased # sconcat :: NonEmpty (UnderComposition Erased) -> UnderComposition Erased stimes :: Integral b => b -> UnderComposition Erased -> UnderComposition Erased | |
type Rep Erased Source # | |
Defined in Agda.Syntax.Common type Rep Erased = D1 ('MetaData "Erased" "Agda.Syntax.Common" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "Erased" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Q0Origin)) :+: C1 ('MetaCons "NotErased" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QωOrigin))) |
data Annotation Source #
We have a tuple of annotations, which might not be fully orthogonal.
Constructors
Annotation | |
Instances
class LensAnnotation a where Source #
Minimal complete definition
Nothing
Methods
getAnnotation :: a -> Annotation Source #
default getAnnotation :: LensArgInfo a => a -> Annotation Source #
setAnnotation :: Annotation -> a -> a Source #
default setAnnotation :: LensArgInfo a => Annotation -> a -> a Source #
mapAnnotation :: (Annotation -> Annotation) -> a -> a Source #
Instances
data LockOrigin Source #
Instances
class LensLock a where Source #
Minimal complete definition
A function argument can be hidden and/or irrelevant.
Constructors
ArgInfo | |
Fields
|
Instances
Origin of arguments.
Constructors
UserWritten | From the source file / user input. (Preserve!) |
Inserted | E.g. inserted hidden arguments. |
Reflected | Produced by the reflection machinery. |
CaseSplit | Produced by an interactive case split. |
Substitution | Named application produced to represent a substitution. E.g. "?0 (x = n)" instead of "?0 n" |
ExpandedPun | An expanded hidden argument pun. |
Generalization | Inserted by the generalization process |
Instances
LensOrigin Origin Source # | |
HasRange Origin Source # | |
KillRange Origin Source # | |
Defined in Agda.Syntax.Common Methods | |
ChooseFlex Origin Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: Origin -> Origin -> FlexChoice Source # | |
EmbPrj Origin Source # | |
Show Origin Source # | |
NFData Origin Source # | |
Defined in Agda.Syntax.Common | |
Eq Origin Source # | |
Ord Origin Source # | |
data WithOrigin a Source #
Decorating something with Origin
information.
Constructors
WithOrigin | |
Instances
class LensOrigin a where Source #
A lens to access the Origin
attribute in data structures.
Minimal implementation: getOrigin
and mapOrigin
or LensArgInfo
.
Minimal complete definition
Nothing
Methods
getOrigin :: a -> Origin Source #
default getOrigin :: LensArgInfo a => a -> Origin Source #
Instances
LensOrigin ArgInfo Source # | |
LensOrigin Origin Source # | |
LensOrigin AppInfo Source # | |
LensOrigin (Arg e) Source # | |
LensOrigin (WithOrigin a) Source # | |
Defined in Agda.Syntax.Common Methods getOrigin :: WithOrigin a -> Origin Source # setOrigin :: Origin -> WithOrigin a -> WithOrigin a Source # mapOrigin :: (Origin -> Origin) -> WithOrigin a -> WithOrigin a Source # | |
LensOrigin (Elim' a) Source # | This instance cheats on |
LensOrigin (FlexibleVar a) Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem Methods getOrigin :: FlexibleVar a -> Origin Source # setOrigin :: Origin -> FlexibleVar a -> FlexibleVar a Source # mapOrigin :: (Origin -> Origin) -> FlexibleVar a -> FlexibleVar a Source # | |
LensOrigin (Dom' t e) Source # | |
data FreeVariables Source #
Constructors
UnknownFVs | |
KnownFVs IntSet |
Instances
class LensFreeVariables a where Source #
A lens to access the FreeVariables
attribute in data structures.
Minimal implementation: getFreeVariables
and mapFreeVariables
or LensArgInfo
.
Minimal complete definition
Nothing
Methods
getFreeVariables :: a -> FreeVariables Source #
default getFreeVariables :: LensArgInfo a => a -> FreeVariables Source #
setFreeVariables :: FreeVariables -> a -> a Source #
mapFreeVariables :: (FreeVariables -> FreeVariables) -> a -> a Source #
default mapFreeVariables :: LensArgInfo a => (FreeVariables -> FreeVariables) -> a -> a Source #
Instances
class Eq a => Underscore a where Source #
Minimal complete definition
Instances
Underscore Expr Source # | |
Defined in Agda.Syntax.Abstract | |
Underscore Doc Source # | |
Defined in Agda.Syntax.Common | |
Underscore Name Source # | |
Defined in Agda.Syntax.Concrete.Name | |
Underscore QName Source # | |
Defined in Agda.Syntax.Concrete.Name | |
Underscore ByteString Source # | |
Defined in Agda.Syntax.Common | |
Underscore String Source # | |
Defined in Agda.Syntax.Common |
class LensNamed a where Source #
Accessor/editor for the nameOf
component.
Minimal complete definition
Nothing
Methods
Functions can be defined in both infix and prefix style. See
LHS
.
Access modifier.
Constructors
PrivateAccess Origin | Store the |
PublicAccess |
data IsAbstract Source #
Abstract or concrete.
Constructors
AbstractDef | |
ConcreteDef |
Instances
class LensIsAbstract a where Source #
Methods
lensIsAbstract :: Lens' a IsAbstract Source #
Instances
LensIsAbstract IsAbstract Source # | |
Defined in Agda.Syntax.Common Methods | |
LensIsAbstract MetaInfo Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
LensIsAbstract TCEnv Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
LensIsAbstract (DefInfo' t) Source # | |
Defined in Agda.Syntax.Info Methods lensIsAbstract :: Lens' (DefInfo' t) IsAbstract Source # | |
LensIsAbstract (Closure a) Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods lensIsAbstract :: Lens' (Closure a) IsAbstract Source # |
class AnyIsAbstract a where Source #
Is any element of a collection an AbstractDef
.
Minimal complete definition
Nothing
Methods
anyIsAbstract :: a -> IsAbstract Source #
default anyIsAbstract :: (Foldable t, AnyIsAbstract b, t b ~ a) => a -> IsAbstract Source #
Instances
AnyIsAbstract IsAbstract Source # | |
Defined in Agda.Syntax.Common Methods anyIsAbstract :: IsAbstract -> IsAbstract Source # | |
AnyIsAbstract (DefInfo' t) Source # | |
Defined in Agda.Syntax.Info Methods anyIsAbstract :: DefInfo' t -> IsAbstract Source # | |
AnyIsAbstract a => AnyIsAbstract (Maybe a) Source # | |
Defined in Agda.Syntax.Common Methods anyIsAbstract :: Maybe a -> IsAbstract Source # | |
AnyIsAbstract a => AnyIsAbstract [a] Source # | |
Defined in Agda.Syntax.Common Methods anyIsAbstract :: [a] -> IsAbstract Source # |
data IsInstance Source #
Is this definition eligible for instance search?
Constructors
InstanceDef Range | Range of the |
NotInstanceDef |
Instances
HasRange IsInstance Source # | |
Defined in Agda.Syntax.Common Methods getRange :: IsInstance -> Range Source # | |
KillRange IsInstance Source # | |
Defined in Agda.Syntax.Common Methods | |
Show IsInstance Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> IsInstance -> ShowS show :: IsInstance -> String showList :: [IsInstance] -> ShowS | |
NFData IsInstance Source # | |
Defined in Agda.Syntax.Common Methods rnf :: IsInstance -> () | |
Eq IsInstance Source # | |
Defined in Agda.Syntax.Common | |
Ord IsInstance Source # | |
Defined in Agda.Syntax.Common Methods compare :: IsInstance -> IsInstance -> Ordering (<) :: IsInstance -> IsInstance -> Bool (<=) :: IsInstance -> IsInstance -> Bool (>) :: IsInstance -> IsInstance -> Bool (>=) :: IsInstance -> IsInstance -> Bool max :: IsInstance -> IsInstance -> IsInstance min :: IsInstance -> IsInstance -> IsInstance |
Is this a macro definition?
Constructors
MacroDef | |
NotMacroDef |
Instances
HasRange IsMacro Source # | |
KillRange IsMacro Source # | |
Defined in Agda.Syntax.Common Methods | |
Generic IsMacro Source # | |
Show IsMacro Source # | |
NFData IsMacro Source # | |
Defined in Agda.Syntax.Common | |
Eq IsMacro Source # | |
Ord IsMacro Source # | |
type Rep IsMacro Source # | |
Defined in Agda.Syntax.Common type Rep IsMacro = D1 ('MetaData "IsMacro" "Agda.Syntax.Common" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "MacroDef" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NotMacroDef" 'PrefixI 'False) (U1 :: Type -> Type)) |
Opaque or transparent.
Constructors
OpaqueDef !OpaqueId | This definition is opaque, and it is guarded by the given opaque block. |
TransparentDef |
Instances
AllAreOpaque IsOpaque Source # | |
Defined in Agda.Syntax.Common Methods jointOpacity :: IsOpaque -> JointOpacity Source # | |
LensIsOpaque IsOpaque Source # | |
Defined in Agda.Syntax.Common | |
KillRange IsOpaque Source # | |
Defined in Agda.Syntax.Common Methods | |
EmbPrj IsOpaque Source # | |
Generic IsOpaque Source # | |
Show IsOpaque Source # | |
NFData IsOpaque Source # | |
Defined in Agda.Syntax.Common | |
Eq IsOpaque Source # | |
Ord IsOpaque Source # | |
Defined in Agda.Syntax.Common | |
type Rep IsOpaque Source # | |
Defined in Agda.Syntax.Common type Rep IsOpaque = D1 ('MetaData "IsOpaque" "Agda.Syntax.Common" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "OpaqueDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 OpaqueId)) :+: C1 ('MetaCons "TransparentDef" 'PrefixI 'False) (U1 :: Type -> Type)) |
The unique identifier of an opaque block. Second argument is the top-level module identifier.
Constructors
OpaqueId !Word64 !ModuleNameHash |
Instances
Pretty OpaqueId Source # | |
KillRange OpaqueId Source # | |
Defined in Agda.Syntax.Common Methods | |
HasFresh OpaqueId Source # | |
EmbPrj OpaqueId Source # | |
Enum OpaqueId Source # | |
Defined in Agda.Syntax.Common | |
Generic OpaqueId Source # | |
Show OpaqueId Source # | |
NFData OpaqueId Source # | |
Defined in Agda.Syntax.Common | |
Eq OpaqueId Source # | |
Ord OpaqueId Source # | |
Defined in Agda.Syntax.Common | |
Hashable OpaqueId Source # | |
Defined in Agda.Syntax.Common | |
type Rep OpaqueId Source # | |
Defined in Agda.Syntax.Common type Rep OpaqueId = D1 ('MetaData "OpaqueId" "Agda.Syntax.Common" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "OpaqueId" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Word64) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 ModuleNameHash))) |
class LensIsOpaque a where Source #
Methods
lensIsOpaque :: Lens' a IsOpaque Source #
Instances
LensIsOpaque IsOpaque Source # | |
Defined in Agda.Syntax.Common | |
LensIsOpaque (DefInfo' t) Source # | |
Defined in Agda.Syntax.Info |
data JointOpacity Source #
Monoid representing the combined opaque blocks of a Foldable
containing possibly-opaque declarations.
Constructors
UniqueOpaque !OpaqueId | Every definition agrees on what opaque block they belong to. |
DifferentOpaque !(HashSet OpaqueId) | More than one opaque block was found. |
NoOpaque | Nothing here is opaque. |
Instances
Monoid JointOpacity Source # | |
Defined in Agda.Syntax.Common Methods mappend :: JointOpacity -> JointOpacity -> JointOpacity mconcat :: [JointOpacity] -> JointOpacity | |
Semigroup JointOpacity Source # | |
Defined in Agda.Syntax.Common Methods (<>) :: JointOpacity -> JointOpacity -> JointOpacity # sconcat :: NonEmpty JointOpacity -> JointOpacity stimes :: Integral b => b -> JointOpacity -> JointOpacity |
class AllAreOpaque a where Source #
Minimal complete definition
Nothing
Methods
jointOpacity :: a -> JointOpacity Source #
default jointOpacity :: (Foldable t, AllAreOpaque b, t b ~ a) => a -> JointOpacity Source #
Instances
AllAreOpaque IsOpaque Source # | |
Defined in Agda.Syntax.Common Methods jointOpacity :: IsOpaque -> JointOpacity Source # | |
AllAreOpaque (DefInfo' t) Source # | |
Defined in Agda.Syntax.Info Methods jointOpacity :: DefInfo' t -> JointOpacity Source # | |
AllAreOpaque a => AllAreOpaque (Maybe a) Source # | |
Defined in Agda.Syntax.Common Methods jointOpacity :: Maybe a -> JointOpacity Source # | |
AllAreOpaque a => AllAreOpaque [a] Source # | |
Defined in Agda.Syntax.Common Methods jointOpacity :: [a] -> JointOpacity Source # |
newtype ModuleNameHash Source #
Constructors
ModuleNameHash | |
Fields
|
Instances
data PositionInName Source #
The position of a name part or underscore in a name.
Constructors
Beginning | The following underscore is at the beginning of the name:
|
Middle | The following underscore is in the middle of the name:
|
End | The following underscore is at the end of the name: |
Instances
Show PositionInName Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> PositionInName -> ShowS show :: PositionInName -> String showList :: [PositionInName] -> ShowS | |
Eq PositionInName Source # | |
Defined in Agda.Syntax.Common Methods (==) :: PositionInName -> PositionInName -> Bool (/=) :: PositionInName -> PositionInName -> Bool | |
Ord PositionInName Source # | |
Defined in Agda.Syntax.Common Methods compare :: PositionInName -> PositionInName -> Ordering (<) :: PositionInName -> PositionInName -> Bool (<=) :: PositionInName -> PositionInName -> Bool (>) :: PositionInName -> PositionInName -> Bool (>=) :: PositionInName -> PositionInName -> Bool max :: PositionInName -> PositionInName -> PositionInName min :: PositionInName -> PositionInName -> PositionInName |
data MaybePlaceholder e Source #
Placeholders are used to represent the underscores in a section.
Constructors
Placeholder !PositionInName | |
NoPlaceholder !(Maybe PositionInName) e | The second argument is used only (but not always) for name parts other than underscores. |
Instances
type PrecedenceLevel = Double Source #
Precedence levels for operators.
data FixityLevel Source #
Constructors
Unrelated | No fixity declared. |
Related !PrecedenceLevel | Fixity level declared as the number. |
Instances
The notation is handled as the fixity in the renamer. Hence, they are grouped together in this type.
Constructors
Fixity' | |
Fields
|
Instances
LensFixity Fixity' Source # | |
Defined in Agda.Syntax.Common | |
LensFixity' Fixity' Source # | |
Defined in Agda.Syntax.Common | |
Pretty Fixity' Source # | |
KillRange Fixity' Source # | |
Defined in Agda.Syntax.Common Methods | |
PrimTerm Fixity' Source # | |
PrimType Fixity' Source # | |
ToTerm Fixity' Source # | |
EmbPrj Fixity' Source # | |
Null Fixity' Source # | |
Show Fixity' Source # | |
NFData Fixity' Source # | |
Defined in Agda.Syntax.Common | |
Eq Fixity' Source # | |
class LensFixity a where Source #
Methods
lensFixity :: Lens' a Fixity Source #
Instances
LensFixity Name Source # | |
Defined in Agda.Syntax.Abstract.Name | |
LensFixity QName Source # | |
Defined in Agda.Syntax.Abstract.Name | |
LensFixity Fixity Source # | |
Defined in Agda.Syntax.Common | |
LensFixity Fixity' Source # | |
Defined in Agda.Syntax.Common | |
LensFixity NewNotation Source # | |
Defined in Agda.Syntax.Notation Methods | |
LensFixity AbstractName Source # | |
Defined in Agda.Syntax.Scope.Base Methods | |
LensFixity (ThingWithFixity a) Source # | |
Defined in Agda.Syntax.Fixity Methods lensFixity :: Lens' (ThingWithFixity a) Fixity Source # |
class LensFixity' a where Source #
Methods
lensFixity' :: Lens' a Fixity' Source #
Instances
LensFixity' Name Source # | |
Defined in Agda.Syntax.Abstract.Name | |
LensFixity' QName Source # | |
Defined in Agda.Syntax.Abstract.Name | |
LensFixity' Fixity' Source # | |
Defined in Agda.Syntax.Common | |
LensFixity' (ThingWithFixity a) Source # | |
Defined in Agda.Syntax.Fixity Methods lensFixity' :: Lens' (ThingWithFixity a) Fixity' Source # |
data ImportDirective' n m Source #
The things you are allowed to say when you shuffle names between name
spaces (i.e. in import
, namespace
, or open
declarations).
Constructors
ImportDirective | |
Fields
|
Instances
The using
clause of import directive.
Constructors
UseEverything | No |
Using [ImportedName' n m] |
|
Instances
(Pretty a, Pretty b) => Pretty (Using' a b) Source # | |
(HasRange a, HasRange b) => HasRange (Using' a b) Source # | |
(KillRange a, KillRange b) => KillRange (Using' a b) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Using' a b) Source # | |
Null (Using' n m) Source # | |
Monoid (Using' n m) Source # | |
Semigroup (Using' n m) Source # | |
(Show a, Show b) => Show (Using' a b) | |
(NFData a, NFData b) => NFData (Using' a b) Source # | |
Defined in Agda.Syntax.Common | |
(Eq m, Eq n) => Eq (Using' n m) Source # | |
type HidingDirective' n m = [ImportedName' n m] Source #
type RenamingDirective' n m = [Renaming' n m] Source #
Constructors
Renaming | |
Fields
|
Instances
(Pretty a, Pretty b) => Pretty (Renaming' a b) Source # | |
(HasRange a, HasRange b) => HasRange (Renaming' a b) Source # | |
(KillRange a, KillRange b) => KillRange (Renaming' a b) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Renaming' a b) Source # | |
(Show a, Show b) => Show (Renaming' a b) | |
(NFData a, NFData b) => NFData (Renaming' a b) Source # | Ranges are not forced. |
Defined in Agda.Syntax.Common | |
(Eq m, Eq n) => Eq (Renaming' n m) Source # | |
data PositivityCheck Source #
Positivity check? (Default = True).
Constructors
YesPositivityCheck | |
NoPositivityCheck |
Instances
data UniverseCheck Source #
Universe check? (Default is yes).
Constructors
YesUniverseCheck | |
NoUniverseCheck |
Instances
data CoverageCheck Source #
Coverage check? (Default is yes).
Constructors
YesCoverageCheck | |
NoCoverageCheck |
Instances
data RewriteEqn' qn nm p e Source #
RewriteEqn' qn p e
represents the rewrite
and irrefutable with
clauses of the LHS.
qn
stands for the QName of the auxiliary function generated to implement the feature
nm
is the type of names for pattern variables
p
is the type of patterns
e
is the type of expressions
Instances
data ExpandedEllipsis Source #
Constructors
ExpandedEllipsis | |
Fields
| |
NoEllipsis |
Instances
data NotationPart Source #
Notation parts.
Constructors
IdPart RString | An identifier part. For instance, for |
HolePart Range (NamedArg (Ranged Int)) | A hole: a place where argument expressions can be written.
For instance, for |
VarPart Range (Ranged BoundVariablePosition) | A bound variable. The first range is the range of the variable in the right-hand side of the syntax declaration, and the second range is the range of the variable in the left-hand side. |
WildPart (Ranged BoundVariablePosition) | A wildcard (an underscore in binding position). |
Instances
data BoundVariablePosition Source #
Positions of variables in syntax declarations.
Constructors
BoundVariablePosition | |
Fields
|
Instances
fromImportedName :: ImportedName' a a -> a Source #
partitionImportedNames :: [ImportedName' n m] -> ([n], [m]) Source #
Like partitionEithers
.
defaultArg :: a -> Arg a Source #
hasQuantity0 :: LensQuantity a => a -> Bool Source #
Check for Quantity0
.
isInstance :: LensHiding a => a -> Bool Source #
hidingToString :: Hiding -> String Source #
mergeHiding :: LensHiding a => WithHiding a -> a Source #
Monoidal composition of Hiding
information in some data.
visible :: LensHiding a => a -> Bool Source #
NotHidden
arguments are visible
.
notVisible :: LensHiding a => a -> Bool Source #
LensHiding a => a -> Bool Source #
::Hidden
arguments are hidden
.
hide :: LensHiding a => a -> a Source #
hideOrKeepInstance :: LensHiding a => a -> a Source #
makeInstance :: LensHiding a => a -> a Source #
makeInstance' :: LensHiding a => Overlappable -> a -> a Source #
isOverlappable :: LensHiding a => a -> Bool Source #
sameHiding :: (LensHiding a, LensHiding b) => a -> b -> Bool Source #
Ignores Overlappable
.
composeModality :: Modality -> Modality -> Modality Source #
Multiplicative monoid (standard monoid).
unitModality :: Modality Source #
Identity under composition
inverseComposeModality :: Modality -> Modality -> Modality Source #
inverseComposeModality r x
returns the least modality y
such that forall x
, y
we have
x `moreUsableModality` (r `composeModality` y)
iff
(r `inverseComposeModality` x) `moreUsableModality` y
(Galois connection).
zeroModality :: Modality Source #
Identity under addition
moreUsableModality :: Modality -> Modality -> Bool Source #
m
means that an moreUsableModality
m'm
can be used
where ever an m'
is required.
usableModality :: LensModality a => a -> Bool Source #
usableRelevance :: LensRelevance a => a -> Bool Source #
usableRelevance rel == False
iff we cannot use a variable of rel
.
usableQuantity :: LensQuantity a => a -> Bool Source #
A thing of quantity 0 is unusable, all others are usable.
usableCohesion :: LensCohesion a => a -> Bool Source #
usableCohesion rel == False
iff we cannot use a variable of rel
.
composeRelevance :: Relevance -> Relevance -> Relevance Source #
Relevance
composition.
Irrelevant
is dominant, Relevant
is neutral.
Composition coincides with max
.
composeCohesion :: Cohesion -> Cohesion -> Cohesion Source #
Cohesion
composition.
Squash
is dominant, Continuous
is neutral.
applyModality :: LensModality a => Modality -> a -> a Source #
Compose with modality flag from the left.
This function is e.g. used to update the modality information
on pattern variables a
after a match against something of modality q
.
inverseComposeRelevance :: Relevance -> Relevance -> Relevance Source #
inverseComposeRelevance r x
returns the most irrelevant y
such that forall x
, y
we have
x `moreRelevant` (r `composeRelevance` y)
iff
(r `inverseComposeRelevance` x) `moreRelevant` y
(Galois connection).
inverseComposeQuantity :: Quantity -> Quantity -> Quantity Source #
inverseComposeQuantity r x
returns the least quantity y
such that forall x
, y
we have
x `moreQuantity` (r `composeQuantity` y)
iff
(r `inverseComposeQuantity` x) `moreQuantity` y
(Galois connection).
inverseComposeCohesion :: Cohesion -> Cohesion -> Cohesion Source #
inverseComposeCohesion r x
returns the least y
such that forall x
, y
we have
x `moreCohesion` (r `composeCohesion` y)
iff
(r `inverseComposeCohesion` x) `moreCohesion` y
(Galois connection).
The above law fails for r = Squash
.
inverseApplyModalityButNotQuantity :: LensModality a => Modality -> a -> a Source #
Left division by a Modality
.
Used e.g. to modify context when going into a m
argument.
Note that this function does not change quantities.
addRelevance :: Relevance -> Relevance -> Relevance Source #
Combine inferred Relevance
.
The unit is Irrelevant
.
addQuantity :: Quantity -> Quantity -> Quantity Source #
Quantity
forms an additive monoid with zero Quantity0.
zeroRelevance :: Relevance Source #
Relevance
forms a monoid under addition, and even a semiring.
zeroQuantity :: Quantity Source #
Identity element under addition
zeroCohesion :: Cohesion Source #
Cohesion
forms a monoid under addition, and even a semiring.
unitRelevance :: Relevance Source #
Identity element under composition
unitQuantity :: Quantity Source #
Identity element under composition
unitCohesion :: Cohesion Source #
Identity under composition
topModality :: Modality Source #
Absorptive element under addition.
topRelevance :: Relevance Source #
Absorptive element under addition.
topQuantity :: Quantity Source #
Absorptive element is ω.
topCohesion :: Cohesion Source #
Absorptive element under addition.
defaultModality :: Modality Source #
The default Modality Beware that this is neither the additive unit nor the unit under composition, because the default quantity is ω.
defaultRelevance :: Relevance Source #
Default Relevance is the identity element under composition
defaultQuantity :: Quantity Source #
Absorptive element! This differs from Relevance and Cohesion whose default is the multiplicative unit.
defaultCohesion :: Cohesion Source #
Default Cohesion is the identity element under composition
sameModality :: (LensModality a, LensModality b) => a -> b -> Bool Source #
Equality ignoring origin.
sameRelevance :: Relevance -> Relevance -> Bool Source #
Equality ignoring origin.
sameQuantity :: Quantity -> Quantity -> Bool Source #
Equality ignoring origin.
sameCohesion :: Cohesion -> Cohesion -> Bool Source #
Equality ignoring origin.
getRelevanceMod :: LensModality a => LensGet a Relevance Source #
setRelevanceMod :: LensModality a => LensSet a Relevance Source #
mapRelevanceMod :: LensModality a => LensMap a Relevance Source #
getQuantityMod :: LensModality a => LensGet a Quantity Source #
setQuantityMod :: LensModality a => LensSet a Quantity Source #
mapQuantityMod :: LensModality a => LensMap a Quantity Source #
getCohesionMod :: LensModality a => LensGet a Cohesion Source #
setCohesionMod :: LensModality a => LensSet a Cohesion Source #
mapCohesionMod :: LensModality a => LensMap a Cohesion Source #
moreQuantity :: Quantity -> Quantity -> Bool Source #
m
means that an moreUsableQuantity
m'm
can be used
where ever an m'
is required.
applyQuantity :: LensQuantity a => Quantity -> a -> a Source #
Compose with quantity flag from the left.
This function is e.g. used to update the quantity information
on pattern variables a
after a match against something of quantity q
.
inverseApplyQuantity :: LensQuantity a => Quantity -> a -> a Source #
Left division by a Quantity
.
Used e.g. to modify context when going into a q
argument.
hasQuantity1 :: LensQuantity a => a -> Bool Source #
Check for Quantity1
.
hasQuantityω :: LensQuantity a => a -> Bool Source #
Check for Quantityω
.
noUserQuantity :: LensQuantity a => a -> Bool Source #
Did the user supply a quantity annotation?
defaultErased :: Erased Source #
The default value of type Erased
: not erased.
sameErased :: Erased -> Erased -> Bool Source #
Equality ignoring origin.
allRelevances :: [Relevance] Source #
isRelevant :: LensRelevance a => a -> Bool Source #
isIrrelevant :: LensRelevance a => a -> Bool Source #
isNonStrict :: LensRelevance a => a -> Bool Source #
moreRelevant :: Relevance -> Relevance -> Bool Source #
Information ordering.
Relevant `moreRelevant`
NonStrict `moreRelevant`
Irrelevant
applyRelevance :: LensRelevance a => Relevance -> a -> a Source #
Compose with relevance flag from the left.
This function is e.g. used to update the relevance information
on pattern variables a
after a match against something rel
.
inverseApplyRelevance :: LensRelevance a => Relevance -> a -> a Source #
Left division by a Relevance
.
Used e.g. to modify context when going into a rel
argument.
irrToNonStrict :: Relevance -> Relevance Source #
Irrelevant function arguments may appear non-strictly in the codomain type.
nonStrictToRel :: Relevance -> Relevance Source #
Applied when working on types (unless --experimental-irrelevance).
nonStrictToIrr :: Relevance -> Relevance Source #
defaultLock :: Lock Source #
allCohesions :: [Cohesion] Source #
moreCohesion :: Cohesion -> Cohesion -> Bool Source #
Information ordering.
Flat `moreCohesion`
Continuous `moreCohesion`
Sharp `moreCohesion`
Squash
applyCohesion :: LensCohesion a => Cohesion -> a -> a Source #
Compose with cohesion flag from the left.
This function is e.g. used to update the cohesion information
on pattern variables a
after a match against something of cohesion rel
.
inverseApplyCohesion :: LensCohesion a => Cohesion -> a -> a Source #
Left division by a Cohesion
.
Used e.g. to modify context when going into a rel
argument.
oneFreeVariable :: Int -> FreeVariables Source #
freeVariablesFromList :: [Int] -> FreeVariables Source #
hasNoFreeVariables :: LensFreeVariables a => a -> Bool Source #
getHidingArgInfo :: LensArgInfo a => LensGet a Hiding Source #
setHidingArgInfo :: LensArgInfo a => LensSet a Hiding Source #
mapHidingArgInfo :: LensArgInfo a => LensMap a Hiding Source #
getModalityArgInfo :: LensArgInfo a => LensGet a Modality Source #
setModalityArgInfo :: LensArgInfo a => LensSet a Modality Source #
mapModalityArgInfo :: LensArgInfo a => LensMap a Modality Source #
getOriginArgInfo :: LensArgInfo a => LensGet a Origin Source #
setOriginArgInfo :: LensArgInfo a => LensSet a Origin Source #
mapOriginArgInfo :: LensArgInfo a => LensMap a Origin Source #
isInsertedHidden :: (LensHiding a, LensOrigin a) => a -> Bool Source #
withArgsFrom :: [a] -> [Arg b] -> [Arg a] Source #
withNamedArgsFrom :: [a] -> [NamedArg b] -> [NamedArg a] Source #
namedSame :: (LensNamed a, LensNamed b, NameOf a ~ NamedName, NameOf b ~ NamedName) => a -> b -> Bool Source #
fittingNamedArg :: (LensNamed arg, NameOf arg ~ NamedName, LensHiding arg, LensNamed dom, NameOf dom ~ NamedName, LensHiding dom) => arg -> dom -> Maybe Bool Source #
Does an argument arg
fit the shape dom
of the next expected argument?
The hiding has to match, and if the argument has a name, it should match the name of the domain.
Nothing
should be __IMPOSSIBLE__
, so use as
@
fromMaybe IMPOSSIBLE $ fittingNamedArg arg dom
@
defaultNamedArg :: a -> NamedArg a Source #
unnamedArg :: ArgInfo -> a -> NamedArg a Source #
updateNamedArg :: (a -> b) -> NamedArg a -> NamedArg b Source #
The functor instance for NamedArg
would be ambiguous,
so we give it another name here.
updateNamedArgA :: Applicative f => (a -> f b) -> NamedArg a -> f (NamedArg b) Source #
setNamedArg :: NamedArg a -> b -> NamedArg b Source #
setNamedArg a b = updateNamedArg (const b) a
argNameToString :: ArgName -> String Source #
stringToArgName :: String -> ArgName Source #
rawNameToString :: RawName -> String Source #
stringToRawName :: String -> RawName Source #
bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin Source #
Prefer user-written over system-inserted.
noPlaceholder :: e -> MaybePlaceholder e Source #
An abbreviation: noPlaceholder =
.NoPlaceholder
Nothing
defaultImportDir :: ImportDirective' n m Source #
Default is directive is private
(use everything, but do not export).
isDefaultImportDir :: ImportDirective' n m -> Bool Source #
isDefaultImportDir
implies null
, but not the other way round.
mapUsing :: ([ImportedName' n1 m1] -> [ImportedName' n2 m2]) -> Using' n1 m1 -> Using' n2 m2 Source #
setImportedName :: ImportedName' a a -> a -> ImportedName' a a Source #
Constructors
Inductive | |
CoInductive |
Instances
PatternMatchingAllowed Induction Source # | |
Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: Induction -> Bool Source # | |
Pretty Induction Source # | |
HasRange Induction Source # | |
KillRange Induction Source # | |
Defined in Agda.Syntax.Common Methods | |
EmbPrj Induction Source # | |
Show Induction Source # | |
NFData Induction Source # | |
Defined in Agda.Syntax.Common.Aspect | |
Eq Induction Source # | |
Ord Induction Source # | |
Defined in Agda.Syntax.Common.Aspect |