| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Common
Contents
Description
Some common syntactic entities are defined in this module.
Synopsis
- type Arity = Nat
- data Overlappable
- type Nat = Int
- data Associativity
- data Fixity = Fixity {}
- newtype Constr a = Constr a
- data Arg e = Arg {}
- data FileType
- data IsMain
- newtype InteractionId = InteractionId {
- interactionId :: Nat
- data Modality = Modality {}
- newtype ProblemId = ProblemId Nat
- data MetaId = MetaId {
- metaId :: !Word64
- metaModule :: !ModuleNameHash
- data Ranged a = Ranged {
- rangeOf :: Range
- rangedThing :: a
- data ArgInfo = ArgInfo {}
- data Origin
- data ConOrigin
- data Hiding
- data NameId = NameId !Word64 !ModuleNameHash
- data ProjOrigin
- data TerminationCheck m
- type Notation = [NotationPart]
- data Lock
- data Cubical
- type NamedArg a = Arg (Named_ a)
- data IsOpaque
- data ImportedName' n m
- = ImportedModule m
- | ImportedName n
- data Relevance
- data WithHiding a = WithHiding {}
- data Language
- data RecordDirectives' a = RecordDirectives {
- recInductive :: Maybe (Ranged Induction)
- recHasEta :: Maybe (Ranged 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
- data OverlapMode
- class HasOverlapMode a where
- 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 WithOrigin a = WithOrigin {}
- class LensOrigin a where
- data FreeVariables
- 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 OpaqueId = OpaqueId !Word64 !ModuleNameHash
- class LensIsOpaque a where
- lensIsOpaque :: Lens' a IsOpaque
- data JointOpacity
- class AllAreOpaque a where
- jointOpacity :: a -> JointOpacity
- data PositionInName
- data MaybePlaceholder 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 KwRange
- 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 { }
- | NoEllipsis
- data NotationPart
- data BoundVariablePosition = BoundVariablePosition {
- holeNumber :: !Int
- varNumber :: !Int
- hidden :: LensHiding a => a -> Bool
- isInstance :: LensHiding a => a -> Bool
- defaultFixity :: Fixity
- defaultArgInfo :: ArgInfo
- visible :: LensHiding a => a -> Bool
- fromImportedName :: ImportedName' a a -> a
- partitionImportedNames :: [ImportedName' n m] -> ([n], [m])
- defaultArg :: a -> Arg a
- hasQuantity0 :: LensQuantity a => a -> Bool
- emptyRecordDirectives :: RecordDirectives' a
- isIncoherent :: HasOverlapMode a => a -> Bool
- isOverlappable :: HasOverlapMode a => a -> Bool
- isOverlapping :: HasOverlapMode a => a -> Bool
- hidingToString :: Hiding -> String
- mergeHiding :: LensHiding a => WithHiding a -> a
- notVisible :: 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
- isYesOverlap :: 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
- isQuantityω :: 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]
- isContinuous :: LensCohesion a => a -> Bool
- 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
- privateAccessInserted :: Access
- 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
- module Agda.Syntax.Common.KeywordRange
- module Agda.Syntax.TopLevelModuleName.Boot
- data Induction
Documentation
data Overlappable Source #
Constructors
| YesOverlap | |
| NoOverlap |
Instances
data Associativity Source #
Associativity.
Constructors
| NonAssoc | |
| LeftAssoc | |
| RightAssoc |
Instances
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 # | |
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 | |
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.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" '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)))) | |
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
Meta-variable identifiers use the same structure as NameIds.
Constructors
| MetaId | |
Fields
| |
Instances
Thing with range info.
Constructors
| Ranged | |
Fields
| |
Instances
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 # | |
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
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 # | |
| ChooseFlex Hiding Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: Hiding -> Hiding -> FlexChoice Source # | |
| EmbPrj Hiding Source # | |
| Unquote Hiding Source # | |
| Null 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 # | |
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.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" '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 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
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 # | |
| Pretty 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.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" '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.
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.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (C1 ('MetaCons "OpaqueDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 OpaqueId)) :+: C1 ('MetaCons "TransparentDef" '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
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
data WithHiding a Source #
Decorating something with Hiding information.
Constructors
| WithHiding | |
Instances
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.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" '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
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.) |