Safe Haskell | None |
---|---|
Language | Haskell2010 |
- Delayed
- Eta-equality
- Induction
- Hiding
- Modalities
- Quantities
- Relevance
- Origin of arguments (user-written, inserted or reflected)
- Free variable annotations
- Argument decoration
- Arguments
- Names
- Function type domain
- Named arguments
- Range decoration.
- Raw names (before parsing into name parts).
- Further constructor and projection info
- Infixity, access, abstract, etc.
- NameId
- Meta variables
- Placeholders (used to parse sections)
- Interaction meta variables
- Import directive
- Termination
- Positivity
Some common syntactic entities are defined in this module.
Synopsis
- data Delayed
- data HasEta
- data Induction
- data Overlappable
- data Hiding
- data WithHiding a = WithHiding {}
- class LensHiding a where
- 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
- isInstance :: LensHiding a => a -> Bool
- sameHiding :: (LensHiding a, LensHiding b) => a -> b -> Bool
- data Modality = Modality {}
- defaultModality :: Modality
- class LensModality a where
- getRelevanceMod :: LensModality a => LensGet Relevance a
- setRelevanceMod :: LensModality a => LensSet Relevance a
- mapRelevanceMod :: LensModality a => LensMap Relevance a
- getQuantityMod :: LensModality a => LensGet Quantity a
- setQuantityMod :: LensModality a => LensSet Quantity a
- mapQuantityMod :: LensModality a => LensMap Quantity a
- data Quantity
- defaultQuantity :: Quantity
- class LensQuantity a where
- data Relevance
- allRelevances :: [Relevance]
- defaultRelevance :: Relevance
- class LensRelevance a where
- isRelevant :: LensRelevance a => a -> Bool
- isIrrelevant :: LensRelevance a => a -> Bool
- isNonStrict :: LensRelevance a => a -> Bool
- moreRelevant :: Relevance -> Relevance -> Bool
- unusableRelevance :: LensRelevance a => a -> Bool
- composeRelevance :: Relevance -> Relevance -> Relevance
- inverseComposeRelevance :: Relevance -> Relevance -> Relevance
- irrToNonStrict :: Relevance -> Relevance
- nonStrictToRel :: Relevance -> Relevance
- nonStrictToIrr :: Relevance -> Relevance
- data Origin
- data WithOrigin a = WithOrigin {}
- class LensOrigin a where
- data FreeVariables
- unknownFreeVariables :: FreeVariables
- noFreeVariables :: FreeVariables
- oneFreeVariable :: Int -> FreeVariables
- freeVariablesFromList :: [Int] -> FreeVariables
- class LensFreeVariables a where
- hasNoFreeVariables :: LensFreeVariables a => a -> Bool
- data ArgInfo = ArgInfo {}
- class LensArgInfo a where
- defaultArgInfo :: ArgInfo
- getHidingArgInfo :: LensArgInfo a => LensGet Hiding a
- setHidingArgInfo :: LensArgInfo a => LensSet Hiding a
- mapHidingArgInfo :: LensArgInfo a => LensMap Hiding a
- getModalityArgInfo :: LensArgInfo a => LensGet Modality a
- setModalityArgInfo :: LensArgInfo a => LensSet Modality a
- mapModalityArgInfo :: LensArgInfo a => LensMap Modality a
- getOriginArgInfo :: LensArgInfo a => LensGet Origin a
- setOriginArgInfo :: LensArgInfo a => LensSet Origin a
- mapOriginArgInfo :: LensArgInfo a => LensMap Origin a
- getFreeVariablesArgInfo :: LensArgInfo a => LensGet FreeVariables a
- setFreeVariablesArgInfo :: LensArgInfo a => LensSet FreeVariables a
- mapFreeVariablesArgInfo :: LensArgInfo a => LensMap FreeVariables a
- data Arg e = Arg {}
- defaultArg :: a -> Arg a
- withArgsFrom :: [a] -> [Arg b] -> [Arg a]
- withNamedArgsFrom :: [a] -> [NamedArg b] -> [NamedArg a]
- class Eq a => Underscore a where
- data Dom e = Dom {}
- argFromDom :: Dom a -> Arg a
- domFromArg :: Arg a -> Dom a
- defaultDom :: a -> Dom a
- data Named name a = Named {
- nameOf :: Maybe name
- namedThing :: a
- type Named_ = Named RString
- unnamed :: a -> Named name a
- named :: name -> a -> Named name a
- type NamedArg a = Arg (Named_ a)
- namedArg :: NamedArg a -> a
- defaultNamedArg :: a -> NamedArg a
- updateNamedArg :: (a -> b) -> NamedArg a -> NamedArg b
- setNamedArg :: NamedArg a -> b -> NamedArg b
- data Ranged a = Ranged {
- rangeOf :: Range
- rangedThing :: a
- unranged :: a -> Ranged a
- type RawName = String
- rawNameToString :: RawName -> String
- stringToRawName :: String -> RawName
- type RString = Ranged RawName
- data ConOrigin
- bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin
- data ProjOrigin
- data DataOrRecord
- data IsInfix
- data Access
- data IsAbstract
- data IsInstance
- data IsMacro
- type Nat = Int
- type Arity = Nat
- data NameId = NameId !Word64 !Word64
- newtype MetaId = MetaId {}
- newtype Constr a = Constr a
- data PositionInName
- data MaybePlaceholder e
- noPlaceholder :: e -> MaybePlaceholder e
- newtype InteractionId = InteractionId {
- interactionId :: Nat
- data ImportDirective' a b = ImportDirective {
- importDirRange :: Range
- using :: Using' a b
- hiding :: [ImportedName' a b]
- impRenaming :: [Renaming' a b]
- publicOpen :: Bool
- data Using' a b
- = UseEverything
- | Using [ImportedName' a b]
- defaultImportDir :: ImportDirective' a b
- isDefaultImportDir :: ImportDirective' a b -> Bool
- data ImportedName' a b
- = ImportedModule b
- | ImportedName a
- setImportedName :: ImportedName' a a -> a -> ImportedName' a a
- data Renaming' a b = Renaming {
- renFrom :: ImportedName' a b
- renTo :: ImportedName' a b
- renToRange :: Range
- data TerminationCheck m
- type PositivityCheck = Bool
Delayed
Used to specify whether something should be delayed.
Instances
Eq Delayed Source # | |
Data Delayed Source # | |
Defined in Agda.Syntax.Common gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Delayed -> c Delayed # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Delayed # toConstr :: Delayed -> Constr # dataTypeOf :: Delayed -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Delayed) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Delayed) # gmapT :: (forall b. Data b => b -> b) -> Delayed -> Delayed # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Delayed -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Delayed -> r # gmapQ :: (forall d. Data d => d -> u) -> Delayed -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Delayed -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Delayed -> m Delayed # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Delayed -> m Delayed # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Delayed -> m Delayed # | |
Ord Delayed Source # | |
Show Delayed Source # | |
KillRange Delayed Source # | |
Defined in Agda.Syntax.Common | |
EmbPrj Delayed Source # | |
Eta-equality
Instances
Eq HasEta Source # | |
Data HasEta Source # | |
Defined in Agda.Syntax.Common gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HasEta -> c HasEta # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HasEta # toConstr :: HasEta -> Constr # dataTypeOf :: HasEta -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HasEta) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HasEta) # gmapT :: (forall b. Data b => b -> b) -> HasEta -> HasEta # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HasEta -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HasEta -> r # gmapQ :: (forall d. Data d => d -> u) -> HasEta -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> HasEta -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> HasEta -> m HasEta # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HasEta -> m HasEta # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HasEta -> m HasEta # | |
Ord HasEta Source # | |
Show HasEta Source # | |
NFData HasEta Source # | |
Defined in Agda.Syntax.Common | |
KillRange HasEta Source # | |
Defined in Agda.Syntax.Common | |
HasRange HasEta Source # | |
EmbPrj HasEta Source # | |
Induction
Instances
Eq Induction Source # | |
Data Induction Source # | |
Defined in Agda.Syntax.Common gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Induction -> c Induction # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Induction # toConstr :: Induction -> Constr # dataTypeOf :: Induction -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Induction) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Induction) # gmapT :: (forall b. Data b => b -> b) -> Induction -> Induction # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Induction -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Induction -> r # gmapQ :: (forall d. Data d => d -> u) -> Induction -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Induction -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Induction -> m Induction # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Induction -> m Induction # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Induction -> m Induction # | |
Ord Induction Source # | |
Defined in Agda.Syntax.Common | |
Show Induction Source # | |
NFData Induction Source # | |
Defined in Agda.Syntax.Common | |
Pretty Induction Source # | |
KillRange Induction Source # | |
Defined in Agda.Syntax.Common | |
HasRange Induction Source # | |
EmbPrj Induction Source # | |
Hiding
data Overlappable Source #
Instances
Instances
Eq Hiding Source # | |
Data Hiding Source # | |
Defined in Agda.Syntax.Common gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Hiding -> c Hiding # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Hiding # toConstr :: Hiding -> Constr # dataTypeOf :: Hiding -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Hiding) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Hiding) # gmapT :: (forall b. Data b => b -> b) -> Hiding -> Hiding # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Hiding -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Hiding -> r # gmapQ :: (forall d. Data d => d -> u) -> Hiding -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Hiding -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Hiding -> m Hiding # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Hiding -> m Hiding # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Hiding -> m Hiding # | |
Ord Hiding Source # | |
Show Hiding Source # | |
Semigroup Hiding Source # |
|
Monoid Hiding Source # | |
NFData Hiding Source # | |
Defined in Agda.Syntax.Common | |
KillRange Hiding Source # | |
Defined in Agda.Syntax.Common | |
LensHiding Hiding Source # | |
EmbPrj Hiding Source # | |
ChooseFlex Hiding Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem chooseFlex :: Hiding -> Hiding -> FlexChoice Source # | |
Unquote Hiding Source # | |
Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b) Source # | |
data WithHiding a Source #
Decorating something with Hiding
information.
Instances
class LensHiding a where Source #
A lens to access the Hiding
attribute in data structures.
Minimal implementation: getHiding
and one of setHiding
or mapHiding
.
Instances
mergeHiding :: LensHiding a => WithHiding a -> a Source #
Monoidal composition of Hiding
information in some data.
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 #
isInstance :: LensHiding a => a -> Bool Source #
sameHiding :: (LensHiding a, LensHiding b) => a -> b -> Bool Source #
Ignores Overlappable
.
Modalities
We have a tuple of modalities, which might not be fully orthogonal. For instance, irrelevant stuff is also run-time irrelevant.
Modality | |
|
Instances
class LensModality a where Source #
getModality :: a -> Modality Source #
setModality :: Modality -> a -> a Source #
mapModality :: (Modality -> Modality) -> a -> a Source #
Instances
LensModality ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
LensModality Modality Source # | |
Defined in Agda.Syntax.Common | |
LensModality (Dom e) Source # | |
Defined in Agda.Syntax.Common | |
LensModality (Arg e) Source # | |
Defined in Agda.Syntax.Common |
getRelevanceMod :: LensModality a => LensGet Relevance a Source #
setRelevanceMod :: LensModality a => LensSet Relevance a Source #
mapRelevanceMod :: LensModality a => LensMap Relevance a Source #
getQuantityMod :: LensModality a => LensGet Quantity a Source #
setQuantityMod :: LensModality a => LensSet Quantity a Source #
mapQuantityMod :: LensModality a => LensMap Quantity a Source #
Quantities
Quantity for linearity.
Quantity0 | Zero uses, erased at runtime. TODO: | Quantity1 -- ^ Linear use (could be updated destructively). (needs postponable constraints between quantities to compute uses). |
Quantityω | Unrestricted use. |
Instances
Bounded Quantity Source # | |
Enum Quantity Source # | |
Eq Quantity Source # | |
Data Quantity Source # | |
Defined in Agda.Syntax.Common gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Quantity -> c Quantity # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Quantity # toConstr :: Quantity -> Constr # dataTypeOf :: Quantity -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Quantity) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quantity) # gmapT :: (forall b. Data b => b -> b) -> Quantity -> Quantity # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quantity -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quantity -> r # gmapQ :: (forall d. Data d => d -> u) -> Quantity -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Quantity -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Quantity -> m Quantity # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Quantity -> m Quantity # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Quantity -> m Quantity # | |
Ord Quantity Source # | Note that the order is |
Defined in Agda.Syntax.Common | |
Show Quantity Source # | |
Generic Quantity Source # | |
Semigroup Quantity Source # | Composition of quantities (multiplication).
|
Monoid Quantity Source # | In the absense of finite quantities besides 0, ω is the unit. |
NFData Quantity Source # | |
Defined in Agda.Syntax.Common | |
PartialOrd Quantity Source # | |
Defined in Agda.Syntax.Common | |
POMonoid Quantity Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup Quantity Source # | |
Defined in Agda.Syntax.Common | |
KillRange Quantity Source # | |
Defined in Agda.Syntax.Common | |
LensQuantity Quantity Source # | |
Defined in Agda.Syntax.Common | |
EmbPrj Quantity Source # | |
type Rep Quantity Source # | |
class LensQuantity a where Source #
getQuantity :: a -> Quantity Source #
setQuantity :: Quantity -> a -> a Source #
mapQuantity :: (Quantity -> Quantity) -> a -> a Source #
Instances
LensQuantity ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
LensQuantity Quantity Source # | |
Defined in Agda.Syntax.Common | |
LensQuantity Modality Source # | |
Defined in Agda.Syntax.Common | |
LensQuantity (Dom e) Source # | |
Defined in Agda.Syntax.Common | |
LensQuantity (Arg e) Source # | |
Defined in Agda.Syntax.Common |
Relevance
A function argument can be relevant or irrelevant. See Agda.TypeChecking.Irrelevance.
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. |
Irrelevant | The argument is irrelevant at compile- and runtime. |
Instances
allRelevances :: [Relevance] Source #
class LensRelevance a where Source #
A lens to access the Relevance
attribute in data structures.
Minimal implementation: getRelevance
and one of setRelevance
or mapRelevance
.
getRelevance :: a -> Relevance Source #
setRelevance :: Relevance -> a -> a Source #
mapRelevance :: (Relevance -> Relevance) -> a -> a Source #
Instances
LensRelevance ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
LensRelevance Relevance Source # | |
Defined in Agda.Syntax.Common | |
LensRelevance Modality Source # | |
Defined in Agda.Syntax.Common | |
LensRelevance TypedBindings Source # | |
Defined in Agda.Syntax.Concrete getRelevance :: TypedBindings -> Relevance Source # setRelevance :: Relevance -> TypedBindings -> TypedBindings Source # mapRelevance :: (Relevance -> Relevance) -> TypedBindings -> TypedBindings Source # | |
LensRelevance VarOcc Source # | |
Defined in Agda.TypeChecking.Free.Lazy | |
LensRelevance (Dom e) Source # | |
Defined in Agda.Syntax.Common | |
LensRelevance (Arg e) Source # | |
Defined in Agda.Syntax.Common |
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
unusableRelevance :: LensRelevance a => a -> Bool Source #
unusableRelevance rel == True
iff we cannot use a variable of rel
.
composeRelevance :: Relevance -> Relevance -> Relevance Source #
Relevance
composition.
Irrelevant
is dominant, Relevant
is neutral.
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).
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 #
Origin of arguments (user-written, inserted or reflected)
Origin of arguments.
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. |
Instances
Eq Origin Source # | |
Data Origin Source # | |
Defined in Agda.Syntax.Common gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Origin -> c Origin # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Origin # toConstr :: Origin -> Constr # dataTypeOf :: Origin -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Origin) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Origin) # gmapT :: (forall b. Data b => b -> b) -> Origin -> Origin # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Origin -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Origin -> r # gmapQ :: (forall d. Data d => d -> u) -> Origin -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Origin -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Origin -> m Origin # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Origin -> m Origin # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Origin -> m Origin # | |
Ord Origin Source # | |
Show Origin Source # | |
NFData Origin Source # | |
Defined in Agda.Syntax.Common | |
KillRange Origin Source # | |
Defined in Agda.Syntax.Common | |
LensOrigin Origin Source # | |
EmbPrj Origin Source # | |
ChooseFlex Origin Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem chooseFlex :: Origin -> Origin -> FlexChoice Source # |
data WithOrigin a Source #
Decorating something with Origin
information.
Instances
class LensOrigin a where Source #
A lens to access the Origin
attribute in data structures.
Minimal implementation: getOrigin
and one of setOrigin
or mapOrigin
.
Instances
LensOrigin ArgInfo Source # | |
LensOrigin Origin Source # | |
LensOrigin AppInfo Source # | |
LensOrigin (Dom e) Source # | |
LensOrigin (Arg e) Source # | |
LensOrigin (WithOrigin a) Source # | |
Defined in Agda.Syntax.Common 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 getOrigin :: FlexibleVar a -> Origin Source # setOrigin :: Origin -> FlexibleVar a -> FlexibleVar a Source # mapOrigin :: (Origin -> Origin) -> FlexibleVar a -> FlexibleVar a Source # |
Free variable annotations
data FreeVariables Source #
Instances
oneFreeVariable :: Int -> FreeVariables Source #
freeVariablesFromList :: [Int] -> FreeVariables Source #
class LensFreeVariables a where Source #
A lens to access the FreeVariables
attribute in data structures.
Minimal implementation: getFreeVariables
and one of setFreeVariables
or mapFreeVariables
.
getFreeVariables :: a -> FreeVariables Source #
setFreeVariables :: FreeVariables -> a -> a Source #
mapFreeVariables :: (FreeVariables -> FreeVariables) -> a -> a Source #
Instances
LensFreeVariables ArgInfo Source # | |
Defined in Agda.Syntax.Common getFreeVariables :: ArgInfo -> FreeVariables Source # setFreeVariables :: FreeVariables -> ArgInfo -> ArgInfo Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> ArgInfo -> ArgInfo Source # | |
LensFreeVariables FreeVariables Source # | |
Defined in Agda.Syntax.Common | |
LensFreeVariables (Dom e) Source # | |
Defined in Agda.Syntax.Common getFreeVariables :: Dom e -> FreeVariables Source # setFreeVariables :: FreeVariables -> Dom e -> Dom e Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> Dom e -> Dom e Source # | |
LensFreeVariables (Arg e) Source # | |
Defined in Agda.Syntax.Common getFreeVariables :: Arg e -> FreeVariables Source # setFreeVariables :: FreeVariables -> Arg e -> Arg e Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> Arg e -> Arg e Source # |
hasNoFreeVariables :: LensFreeVariables a => a -> Bool Source #
Argument decoration
A function argument can be hidden and/or irrelevant.
Instances
class LensArgInfo a where Source #
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 (Dom e) Source # | |
Defined in Agda.Syntax.Common | |
LensArgInfo (Arg a) Source # | |
Defined in Agda.Syntax.Common |
getHidingArgInfo :: LensArgInfo a => LensGet Hiding a Source #
setHidingArgInfo :: LensArgInfo a => LensSet Hiding a Source #
mapHidingArgInfo :: LensArgInfo a => LensMap Hiding a Source #
getModalityArgInfo :: LensArgInfo a => LensGet Modality a Source #
setModalityArgInfo :: LensArgInfo a => LensSet Modality a Source #
mapModalityArgInfo :: LensArgInfo a => LensMap Modality a Source #
getOriginArgInfo :: LensArgInfo a => LensGet Origin a Source #
setOriginArgInfo :: LensArgInfo a => LensSet Origin a Source #
mapOriginArgInfo :: LensArgInfo a => LensMap Origin a Source #
Arguments
Instances
defaultArg :: a -> Arg a Source #
withArgsFrom :: [a] -> [Arg b] -> [Arg a] Source #
withNamedArgsFrom :: [a] -> [NamedArg b] -> [NamedArg a] Source #
Names
class Eq a => Underscore a where Source #
underscore :: a Source #
isUnderscore :: a -> Bool Source #
Instances
Underscore String Source # | |
Defined in Agda.Syntax.Common underscore :: String Source # isUnderscore :: String -> Bool Source # | |
Underscore ByteString Source # | |
Defined in Agda.Syntax.Common underscore :: ByteString Source # isUnderscore :: ByteString -> Bool Source # | |
Underscore Doc Source # | |
Defined in Agda.Syntax.Common underscore :: Doc Source # isUnderscore :: Doc -> Bool Source # | |
Underscore QName Source # | |
Defined in Agda.Syntax.Concrete.Name underscore :: QName Source # isUnderscore :: QName -> Bool Source # | |
Underscore Name Source # | |
Defined in Agda.Syntax.Concrete.Name underscore :: Name Source # isUnderscore :: Name -> Bool Source # | |
Underscore Expr Source # | |
Defined in Agda.Syntax.Abstract underscore :: Expr Source # isUnderscore :: Expr -> Bool Source # |
Function type domain
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.
Instances
argFromDom :: Dom a -> Arg a Source #
domFromArg :: Arg a -> Dom a Source #
defaultDom :: a -> Dom a Source #
Named arguments
Something potentially carrying a name.
Named | |
|
Instances
defaultNamedArg :: 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.
setNamedArg :: NamedArg a -> b -> NamedArg b Source #
setNamedArg a b = updateNamedArg (const b) a
Range decoration.
Thing with range info.
Ranged | |
|
Instances
Functor Ranged Source # | |
Foldable Ranged Source # | |
Defined in Agda.Syntax.Common fold :: Monoid m => Ranged m -> m # foldMap :: Monoid m => (a -> m) -> Ranged a -> m # foldr :: (a -> b -> b) -> b -> Ranged a -> b # foldr' :: (a -> b -> b) -> b -> Ranged a -> b # foldl :: (b -> a -> b) -> b -> Ranged a -> b # foldl' :: (b -> a -> b) -> b -> Ranged a -> b # foldr1 :: (a -> a -> a) -> Ranged a -> a # foldl1 :: (a -> a -> a) -> Ranged a -> a # elem :: Eq a => a -> Ranged a -> Bool # maximum :: Ord a => Ranged a -> a # minimum :: Ord a => Ranged a -> a # | |
Traversable Ranged Source # | |
Decoration Ranged Source # | |
MapNamedArgPattern NAP Source # | |
Defined in Agda.Syntax.Abstract.Pattern | |
UniverseBi Declaration RString | |
Defined in Agda.Syntax.Abstract universeBi :: Declaration -> [RString] | |
PatternVars a (NamedArg (Pattern' a)) Source # | |
Defined in Agda.Syntax.Internal | |
MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of Note: the |
Eq a => Eq (Ranged a) Source # | |
Data a => Data (Ranged a) Source # | |
Defined in Agda.Syntax.Common gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Ranged a -> c (Ranged a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Ranged a) # toConstr :: Ranged a -> Constr # dataTypeOf :: Ranged a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Ranged a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Ranged a)) # gmapT :: (forall b. Data b => b -> b) -> Ranged a -> Ranged a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ranged a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ranged a -> r # gmapQ :: (forall d. Data d => d -> u) -> Ranged a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Ranged a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a) # | |
Ord a => Ord (Ranged a) Source # | |
Defined in Agda.Syntax.Common | |
Show a => Show (Ranged a) Source # | |
Show a => Show (Named_ a) Source # | |
NFData a => NFData (Ranged a) Source # | Ranges are not forced. |
Defined in Agda.Syntax.Common | |
Pretty e => Pretty (Named_ e) Source # | |
KillRange (Ranged a) Source # | |
Defined in Agda.Syntax.Common killRange :: KillRangeT (Ranged a) Source # | |
HasRange (Ranged a) Source # | |
Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns. |
EmbPrj a => EmbPrj (Ranged a) Source # | |
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a) Source # | |
NormaliseProjP a => NormaliseProjP (Named_ a) Source # | |
Defined in Agda.TypeChecking.Records normaliseProjP :: HasConstInfo m => Named_ a -> m (Named_ a) Source # | |
ToAbstract [Arg Term] [NamedArg Expr] Source # | |
Defined in Agda.Syntax.Translation.ReflectedToAbstract | |
ToAbstract r a => ToAbstract (Arg r) (NamedArg a) Source # | |
Defined in Agda.Syntax.Translation.ReflectedToAbstract |
Raw names (before parsing into name parts).
rawNameToString :: RawName -> String Source #
stringToRawName :: String -> RawName Source #
Further constructor and projection info
Where does the ConP
or Con
come from?
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
bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin Source #
Prefer user-written over system-inserted.
data ProjOrigin Source #
Where does a projection come from?
ProjPrefix | User wrote a prefix projection. |
ProjPostfix | User wrote a postfix projection. |
ProjSystem | Projection was generated by the system. |
Instances
data DataOrRecord Source #
Instances
Infixity, access, abstract, etc.
Functions can be defined in both infix and prefix style. See
LHS
.
Instances
Eq IsInfix Source # | |
Data IsInfix Source # | |
Defined in Agda.Syntax.Common gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsInfix -> c IsInfix # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsInfix # toConstr :: IsInfix -> Constr # dataTypeOf :: IsInfix -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsInfix) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsInfix) # gmapT :: (forall b. Data b => b -> b) -> IsInfix -> IsInfix # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsInfix -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsInfix -> r # gmapQ :: (forall d. Data d => d -> u) -> IsInfix -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> IsInfix -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsInfix -> m IsInfix # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInfix -> m IsInfix # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInfix -> m IsInfix # | |
Ord IsInfix Source # | |
Show IsInfix Source # | |
Access modifier.
PrivateAccess Origin | Store the |
PublicAccess | |
OnlyQualified | Visible from outside, but not exported when opening the module Used for qualified constructors. |
Instances
Eq Access Source # | |
Data Access Source # | |
Defined in Agda.Syntax.Common gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Access -> c Access # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Access # toConstr :: Access -> Constr # dataTypeOf :: Access -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Access) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Access) # gmapT :: (forall b. Data b => b -> b) -> Access -> Access # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Access -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Access -> r # gmapQ :: (forall d. Data d => d -> u) -> Access -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Access -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Access -> m Access # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Access -> m Access # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Access -> m Access # | |
Ord Access Source # | |
Show Access Source # | |
NFData Access Source # | |
Defined in Agda.Syntax.Common | |
Pretty Access Source # | |
KillRange Access Source # | |
Defined in Agda.Syntax.Common | |
HasRange Access Source # | |
EmbPrj Access Source # | |
data IsAbstract Source #
Abstract or concrete
Instances
data IsInstance Source #
Is this definition eligible for instance search?
Instances
Is this a macro definition?
Instances
Eq IsMacro Source # | |
Data IsMacro Source # | |
Defined in Agda.Syntax.Common gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsMacro -> c IsMacro # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsMacro # toConstr :: IsMacro -> Constr # dataTypeOf :: IsMacro -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsMacro) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsMacro) # gmapT :: (forall b. Data b => b -> b) -> IsMacro -> IsMacro # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsMacro -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsMacro -> r # gmapQ :: (forall d. Data d => d -> u) -> IsMacro -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> IsMacro -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsMacro -> m IsMacro # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsMacro -> m IsMacro # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsMacro -> m IsMacro # | |
Ord IsMacro Source # | |
Show IsMacro Source # | |
KillRange IsMacro Source # | |
Defined in Agda.Syntax.Common | |
HasRange IsMacro Source # | |
NameId
The unique identifier of a name. Second argument is the top-level module identifier.
Instances
Enum NameId Source # | |
Defined in Agda.Syntax.Common | |
Eq NameId Source # | |
Data NameId Source # | |
Defined in Agda.Syntax.Common gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NameId -> c NameId # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NameId # toConstr :: NameId -> Constr # dataTypeOf :: NameId -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NameId) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NameId) # gmapT :: (forall b. Data b => b -> b) -> NameId -> NameId # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NameId -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NameId -> r # gmapQ :: (forall d. Data d => d -> u) -> NameId -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> NameId -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> NameId -> m NameId # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NameId -> m NameId # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NameId -> m NameId # | |
Ord NameId Source # | |
Show NameId Source # | |
Generic NameId Source # | |
NFData NameId Source # | |
Defined in Agda.Syntax.Common | |
Hashable NameId Source # | |
Defined in Agda.Syntax.Common | |
Pretty NameId Source # | |
KillRange NameId Source # | |
Defined in Agda.Syntax.Common | |
HasFresh NameId Source # | |
EmbPrj NameId Source # | |
type Rep NameId Source # | |
Defined in Agda.Syntax.Common type Rep NameId = D1 (MetaData "NameId" "Agda.Syntax.Common" "Agda-2.5.4-KW6aUUUGirkK5xqjcQ2M8W" 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 Word64))) |
Meta variables
A meta variable identifier is just a natural number.
Instances
Constr a |
Instances
ToConcrete (Constr Constructor) Declaration Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete toConcrete :: Constr Constructor -> AbsToCon Declaration Source # bindToConcrete :: Constr Constructor -> (Declaration -> AbsToCon b) -> AbsToCon b Source # |
Placeholders (used to parse sections)
data PositionInName Source #
The position of a name part or underscore in a name.
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
data MaybePlaceholder e Source #
Placeholders are used to represent the underscores in a section.
Placeholder !PositionInName | |
NoPlaceholder !(Maybe PositionInName) e | The second argument is used only (but not always) for name parts other than underscores. |
Instances
noPlaceholder :: e -> MaybePlaceholder e Source #
An abbreviation: noPlaceholder =
.NoPlaceholder
Nothing
Interaction meta variables
newtype InteractionId Source #
Instances
Import directive
data ImportDirective' a b Source #
The things you are allowed to say when you shuffle names between name
spaces (i.e. in import
, namespace
, or open
declarations).
ImportDirective | |
|
Instances
UseEverything | |
Using [ImportedName' a b] |
Instances
(Eq b, Eq a) => Eq (Using' a b) Source # | |
(Data a, Data b) => Data (Using' a b) Source # | |
Defined in Agda.Syntax.Common gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> Using' a b -> c (Using' a b) # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Using' a b) # toConstr :: Using' a b -> Constr # dataTypeOf :: Using' a b -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Using' a b)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Using' a b)) # gmapT :: (forall b0. Data b0 => b0 -> b0) -> Using' a b -> Using' a b # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Using' a b -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Using' a b -> r # gmapQ :: (forall d. Data d => d -> u) -> Using' a b -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Using' a b -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Using' a b -> m (Using' a b) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Using' a b -> m (Using' a b) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Using' a b -> m (Using' a b) # | |
Semigroup (Using' a b) Source # | |
Monoid (Using' a b) Source # | |
(NFData a, NFData b) => NFData (Using' a b) Source # | |
Defined in Agda.Syntax.Common | |
(Pretty a, Pretty b) => Pretty (Using' a b) Source # | |
(KillRange a, KillRange b) => KillRange (Using' a b) Source # | |
Defined in Agda.Syntax.Common killRange :: KillRangeT (Using' a b) Source # | |
(HasRange a, HasRange b) => HasRange (Using' a b) Source # | |
defaultImportDir :: ImportDirective' a b Source #
Default is directive is private
(use everything, but do not export).
isDefaultImportDir :: ImportDirective' a b -> Bool Source #
data ImportedName' a b Source #
An imported name can be a module or a defined name
Instances
setImportedName :: ImportedName' a a -> a -> ImportedName' a a Source #
Renaming | |
|
Instances
(Eq b, Eq a) => Eq (Renaming' a b) Source # | |
(Data a, Data b) => Data (Renaming' a b) Source # | |
Defined in Agda.Syntax.Common gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> Renaming' a b -> c (Renaming' a b) # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Renaming' a b) # toConstr :: Renaming' a b -> Constr # dataTypeOf :: Renaming' a b -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Renaming' a b)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Renaming' a b)) # gmapT :: (forall b0. Data b0 => b0 -> b0) -> Renaming' a b -> Renaming' a b # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Renaming' a b -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Renaming' a b -> r # gmapQ :: (forall d. Data d => d -> u) -> Renaming' a b -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Renaming' a b -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Renaming' a b -> m (Renaming' a b) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Renaming' a b -> m (Renaming' a b) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Renaming' a b -> m (Renaming' a b) # | |
(NFData a, NFData b) => NFData (Renaming' a b) Source # | Ranges are not forced. |
Defined in Agda.Syntax.Common | |
(KillRange a, KillRange b) => KillRange (Renaming' a b) Source # | |
Defined in Agda.Syntax.Common killRange :: KillRangeT (Renaming' a b) Source # | |
(HasRange a, HasRange b) => HasRange (Renaming' a b) Source # | |
HasRange instances
KillRange instances
NFData instances
Termination
data TerminationCheck m Source #
Termination check? (Default = TerminationCheck).
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
Positivity
type PositivityCheck = Bool Source #
Positivity check? (Default = True).