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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Syntax.Concrete.Definitions.Types

Synopsis

- data NiceDeclaration
  - = Axiom Range Access IsAbstract IsInstance ArgInfo Name Expr
  - | NiceField Range Access IsAbstract IsInstance TacticAttribute Name (Arg Expr)
  - | PrimitiveFunction Range Access IsAbstract Name (Arg Expr)
  - | NiceMutual Range TerminationCheck CoverageCheck PositivityCheck [NiceDeclaration]
  - | NiceModule Range Access IsAbstract QName Telescope [Declaration]
  - | NiceModuleMacro Range Access Name ModuleApplication OpenShortHand ImportDirective
  - | NiceOpen Range QName ImportDirective
  - | NiceImport Range QName (Maybe AsName) OpenShortHand ImportDirective
  - | NicePragma Range Pragma
  - | NiceRecSig Range Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr
  - | NiceDataSig Range Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr
  - | NiceFunClause Range Access IsAbstract TerminationCheck CoverageCheck Catchall Declaration
  - | FunSig Range Access IsAbstract IsInstance IsMacro ArgInfo TerminationCheck CoverageCheck Name Expr
  - | FunDef Range [Declaration] IsAbstract IsInstance TerminationCheck CoverageCheck Name [Clause]
  - | NiceDataDef Range Origin IsAbstract PositivityCheck UniverseCheck Name [LamBinding] [NiceConstructor]
  - | NiceLoneConstructor Range [NiceConstructor]
  - | NiceRecDef Range Origin IsAbstract PositivityCheck UniverseCheck Name RecordDirectives [LamBinding] [Declaration]
  - | NicePatternSyn Range Access Name [Arg Name] Pattern
  - | NiceGeneralize Range Access ArgInfo TacticAttribute Name Expr
  - | NiceUnquoteDecl Range Access IsAbstract IsInstance TerminationCheck CoverageCheck [Name] Expr
  - | NiceUnquoteDef Range Access IsAbstract TerminationCheck CoverageCheck [Name] Expr
- type TerminationCheck = TerminationCheck Measure
- type Measure = Name
- type Catchall = Bool
- type NiceConstructor = NiceTypeSignature
- type NiceTypeSignature = NiceDeclaration
- data Clause = Clause Name Catchall LHS RHS WhereClause [Clause]
- data MutualChecks = MutualChecks {
  - mutualTermination :: [TerminationCheck]
  - mutualCoverage :: [CoverageCheck]
  - mutualPositivity :: [PositivityCheck]
  }
- data InferredMutual = InferredMutual {
  - inferredChecks :: MutualChecks
  - inferredBlock :: [NiceDeclaration]
  - inferredLeftovers :: [NiceDeclaration]
  }
- extendInferredBlock :: NiceDeclaration -> InferredMutual -> InferredMutual
- type InterleavedMutual = Map Name InterleavedDecl
- data InterleavedDecl
  - = InterleavedData {
    - interleavedDeclNum :: DeclNum
    - interleavedDeclSig :: NiceDeclaration
    - interleavedDataCons :: Maybe (DeclNum, List1 [NiceConstructor])
    }
  - | InterleavedFun {
    - interleavedDeclNum :: DeclNum
    - interleavedDeclSig :: NiceDeclaration
    - interleavedFunClauses :: Maybe (DeclNum, List1 ([Declaration], [Clause]))
    }
- type DeclNum = Int
- isInterleavedFun :: InterleavedDecl -> Maybe ()
- isInterleavedData :: InterleavedDecl -> Maybe ()
- interleavedDecl :: Name -> InterleavedDecl -> [(DeclNum, NiceDeclaration)]
- data KindOfBlock
  - = PostulateBlock
  - | PrimitiveBlock
  - | InstanceBlock
  - | FieldBlock
  - | DataBlock
  - | ConstructorBlock
- declName :: NiceDeclaration -> String
- data InMutual
  - = InMutual
  - | NotInMutual
- data DataRecOrFun
  - = DataName {
    - _kindPosCheck :: PositivityCheck
    - _kindUniCheck :: UniverseCheck
    }
  - | RecName {
    - _kindPosCheck :: PositivityCheck
    - _kindUniCheck :: UniverseCheck
    }
  - | FunName TerminationCheck CoverageCheck
- isFunName :: DataRecOrFun -> Bool
- sameKind :: DataRecOrFun -> DataRecOrFun -> Bool
- terminationCheck :: DataRecOrFun -> TerminationCheck
- coverageCheck :: DataRecOrFun -> CoverageCheck
- positivityCheck :: DataRecOrFun -> PositivityCheck
- mutualChecks :: DataRecOrFun -> MutualChecks
- universeCheck :: DataRecOrFun -> UniverseCheck

# Documentation

data NiceDeclaration Source #

The nice declarations. No fixity declarations and function definitions are contained in a single constructor instead of spread out between type signatures and clauses. The `private`, `postulate`, `abstract` and `instance` modifiers have been distributed to the individual declarations.

Observe the order of components:

Range Fixity' Access IsAbstract IsInstance TerminationCheck PositivityCheck

further attributes

(Q)Name

content (Expr, Declaration ...)

Constructors

Axiom Range Access IsAbstract IsInstance ArgInfo Name Expr | `IsAbstract` argument: We record whether a declaration was made in an `abstract` block. `ArgInfo` argument: Axioms and functions can be declared irrelevant. (`Hiding` should be `NotHidden`.)
NiceField Range Access IsAbstract IsInstance TacticAttribute Name (Arg Expr) |
PrimitiveFunction Range Access IsAbstract Name (Arg Expr) |
NiceMutual Range TerminationCheck CoverageCheck PositivityCheck [NiceDeclaration] |
NiceModule Range Access IsAbstract QName Telescope [Declaration] |
NiceModuleMacro Range Access Name ModuleApplication OpenShortHand ImportDirective |
NiceOpen Range QName ImportDirective |
NiceImport Range QName (Maybe AsName) OpenShortHand ImportDirective |
NicePragma Range Pragma |
NiceRecSig Range Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr |
NiceDataSig Range Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr |
NiceFunClause Range Access IsAbstract TerminationCheck CoverageCheck Catchall Declaration | An uncategorized function clause, could be a function clause without type signature or a pattern lhs (e.g. for irrefutable let). The `Declaration` is the actual `FunClause`.
FunSig Range Access IsAbstract IsInstance IsMacro ArgInfo TerminationCheck CoverageCheck Name Expr |

FunDef Range [Declaration] IsAbstract IsInstance TerminationCheck CoverageCheck Name [Clause]

Block of function clauses (we have seen the type signature before). The `Declaration`s are the original declarations that were processed into this `FunDef` and are only used in `notSoNiceDeclaration`. Andreas, 2017-01-01: Because of issue #2372, we add `IsInstance` here. An alias should know that it is an instance.

NiceDataDef Range Origin IsAbstract PositivityCheck UniverseCheck Name [LamBinding] [NiceConstructor] |
NiceLoneConstructor Range [NiceConstructor] |
NiceRecDef Range Origin IsAbstract PositivityCheck UniverseCheck Name RecordDirectives [LamBinding] [Declaration] | `(Maybe Range)` gives range of the 'pattern' declaration.
NicePatternSyn Range Access Name [Arg Name] Pattern |
NiceGeneralize Range Access ArgInfo TacticAttribute Name Expr |
NiceUnquoteDecl Range Access IsAbstract IsInstance TerminationCheck CoverageCheck [Name] Expr |
NiceUnquoteDef Range Access IsAbstract TerminationCheck CoverageCheck [Name] Expr |

#### Instances

Instances details

HasRange NiceDeclaration Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods getRange :: NiceDeclaration -> Range Source #
ToAbstract NiceDeclaration Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon NiceDeclaration Source # Methods toAbstract :: NiceDeclaration -> ScopeM (AbsOfCon NiceDeclaration) Source #
Pretty NiceDeclaration Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods pretty :: NiceDeclaration -> Doc Source # prettyPrec :: Int -> NiceDeclaration -> Doc Source # prettyList :: [NiceDeclaration] -> Doc Source #
Data NiceDeclaration Source # |

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NiceDeclaration -> c NiceDeclaration Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NiceDeclaration Source #

toConstr :: NiceDeclaration -> Constr Source #

dataTypeOf :: NiceDeclaration -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NiceDeclaration) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NiceDeclaration) Source #

gmapT :: (forall b. Data b => b -> b) -> NiceDeclaration -> NiceDeclaration Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> NiceDeclaration -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> NiceDeclaration -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NiceDeclaration -> m NiceDeclaration Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NiceDeclaration -> m NiceDeclaration Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NiceDeclaration -> m NiceDeclaration Source #

Generic NiceDeclaration Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Associated Types type Rep NiceDeclaration :: Type -> Type Source # Methods from :: NiceDeclaration -> Rep NiceDeclaration x Source # to :: Rep NiceDeclaration x -> NiceDeclaration Source #
Show NiceDeclaration Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods showsPrec :: Int -> NiceDeclaration -> ShowS Source # show :: NiceDeclaration -> String Source # showList :: [NiceDeclaration] -> ShowS Source #
NFData NiceDeclaration Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods rnf :: NiceDeclaration -> () Source #
type AbsOfCon NiceDeclaration Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon NiceDeclaration = Declaration
type Rep NiceDeclaration Source # |

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

type Rep NiceDeclaration = D1 ('MetaData "NiceDeclaration" "Agda.Syntax.Concrete.Definitions.Types" "Agda-2.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) ((((C1 ('MetaCons "Axiom" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsInstance) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: C1 ('MetaCons "NiceField" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsInstance) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TacticAttribute)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Expr)))))) :+: (C1 ('MetaCons "PrimitiveFunction" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Expr))))) :+: (C1 ('MetaCons "NiceMutual" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TerminationCheck)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoverageCheck) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PositivityCheck) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NiceDeclaration])))) :+: C1 ('MetaCons "NiceModule" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration]))))))) :+: ((C1 ('MetaCons "NiceModuleMacro" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleApplication) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpenShortHand) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective)))) :+: C1 ('MetaCons "NiceOpen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective)))) :+: (C1 ('MetaCons "NiceImport" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe AsName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpenShortHand) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective)))) :+: (C1 ('MetaCons "NicePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pragma)) :+: C1 ('MetaCons "NiceRecSig" 'PrefixI 'False) (((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PositivityCheck))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LamBinding]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))))))) :+: (((C1 ('MetaCons "NiceDataSig" 'PrefixI 'False) (((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PositivityCheck))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LamBinding]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: C1 ('MetaCons "NiceFunClause" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TerminationCheck) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoverageCheck)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Catchall) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Declaration))))) :+: (C1 ('MetaCons "FunSig" 'PrefixI 'False) (((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsInstance) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsMacro)))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TerminationCheck)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoverageCheck) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))) :+: (C1 ('MetaCons "FunDef" 'PrefixI 'False) (((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsInstance))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TerminationCheck) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoverageCheck)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause])))) :+: C1 ('MetaCons "NiceDataDef" 'PrefixI 'False) (((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Origin)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PositivityCheck))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LamBinding]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NiceConstructor]))))))) :+: ((C1 ('MetaCons "NiceLoneConstructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NiceConstructor])) :+: (C1 ('MetaCons "NiceRecDef" 'PrefixI 'False) (((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Origin)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PositivityCheck))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RecordDirectives) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LamBinding]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration]))))) :+: C1 ('MetaCons "NicePatternSyn" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Arg Name]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern)))))) :+: (C1 ('MetaCons "NiceGeneralize" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TacticAttribute) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: (C1 ('MetaCons "NiceUnquoteDecl" 'PrefixI 'False) (((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsInstance))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TerminationCheck) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoverageCheck)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: C1 ('MetaCons "NiceUnquoteDef" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TerminationCheck) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoverageCheck)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))))))))

type TerminationCheck = TerminationCheck Measure Source #

type Measure = Name Source #

Termination measure is, for now, a variable name.

type Catchall = Bool Source #

type NiceConstructor = NiceTypeSignature Source #

Only `Axiom`s.

type NiceTypeSignature = NiceDeclaration Source #

Only `Axiom`s.

data Clause Source #

One clause in a function definition. There is no guarantee that the `LHS` actually declares the `Name`. We will have to check that later.

Constructors

Clause Name Catchall LHS RHS WhereClause [Clause] |

#### Instances

Instances details

ToAbstract Clause Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon Clause Source # Methods toAbstract :: Clause -> ScopeM (AbsOfCon Clause) Source #
Data Clause Source # |

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Clause -> c Clause Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Clause Source #

toConstr :: Clause -> Constr Source #

dataTypeOf :: Clause -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Clause) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Clause) Source #

gmapT :: (forall b. Data b => b -> b) -> Clause -> Clause Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Clause -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Clause -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Clause -> m Clause Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause -> m Clause Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause -> m Clause Source #

Generic Clause Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Associated Types type Rep Clause :: Type -> Type Source # Methods from :: Clause -> Rep Clause x Source # to :: Rep Clause x -> Clause Source #
Show Clause Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods showsPrec :: Int -> Clause -> ShowS Source # show :: Clause -> String Source # showList :: [Clause] -> ShowS Source #
NFData Clause Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods rnf :: Clause -> () Source #
type AbsOfCon Clause Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon Clause = Clause
type Rep Clause Source # |

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

type Rep Clause = D1 ('MetaData "Clause" "Agda.Syntax.Concrete.Definitions.Types" "Agda-2.6.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) (C1 ('MetaCons "Clause" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Catchall) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHS))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RHS) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhereClause) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause])))))

data MutualChecks Source #

When processing a mutual block we collect the various checks present in the block before combining them.

Constructors

MutualChecks |

Fields

- mutualTermination :: [TerminationCheck]
- mutualCoverage :: [CoverageCheck]
- mutualPositivity :: [PositivityCheck]

#### Instances

Instances details

Monoid MutualChecks Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods mempty :: MutualChecks Source # mappend :: MutualChecks -> MutualChecks -> MutualChecks Source # mconcat :: [MutualChecks] -> MutualChecks Source #
Semigroup MutualChecks Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods (<>) :: MutualChecks -> MutualChecks -> MutualChecks Source # sconcat :: NonEmpty MutualChecks -> MutualChecks Source # stimes :: Integral b => b -> MutualChecks -> MutualChecks Source #

data InferredMutual Source #

In an inferred `mutual` block we keep accumulating nice declarations until all of the lone signatures have an attached definition. The type is therefore a bit span-like: we return an initial segment (the inferred mutual block) together with leftovers.

Constructors

InferredMutual |

Fields

- inferredChecks :: MutualChecks
- inferredBlock :: [NiceDeclaration]
- inferredLeftovers :: [NiceDeclaration]

extendInferredBlock :: NiceDeclaration -> InferredMutual -> InferredMutual Source #

type InterleavedMutual = Map Name InterleavedDecl Source #

In an `interleaved mutual' block we collect the data signatures, function signatures, as well as their associated constructors and function clauses respectively. Each signature is given a position in the block (from 0 onwards) and each set of constructor / clauses is given a *distinct* one. This allows for interleaved forward declarations similar to what one gets in a new-style mutual block.

data InterleavedDecl Source #

Constructors

InterleavedData |

Fields

- interleavedDeclNum :: DeclNum

  Internal number of the data signature.

- interleavedDeclSig :: NiceDeclaration

  The data signature.

- interleavedDataCons :: Maybe (DeclNum, List1 [NiceConstructor])

  Constructors associated to the data signature.

InterleavedFun |

Fields

- interleavedDeclNum :: DeclNum

  Internal number of the data signature.

- interleavedDeclSig :: NiceDeclaration

  The data signature.

- interleavedFunClauses :: Maybe (DeclNum, List1 ([Declaration], [Clause]))

  Function clauses associated to the function signature.

type DeclNum = Int Source #

Numbering declarations in an `interleaved mutual` block.

isInterleavedFun :: InterleavedDecl -> Maybe () Source #

isInterleavedData :: InterleavedDecl -> Maybe () Source #

interleavedDecl :: Name -> InterleavedDecl -> [(DeclNum, NiceDeclaration)] Source #

data KindOfBlock Source #

Several declarations expect only type signatures as sub-declarations. These are:

Constructors

PostulateBlock

    postulate

PrimitiveBlock | `primitive`. Ensured by parser.
InstanceBlock | `instance`. Actually, here all kinds of sub-declarations are allowed a priori.
FieldBlock | `field`. Ensured by parser.
DataBlock | `data ... where`. Here we got a bad error message for Agda-2.5 (Issue 1698).
ConstructorBlock | `constructor`, in `interleaved mutual`.

#### Instances

Instances details

Data KindOfBlock Source # |

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> KindOfBlock -> c KindOfBlock Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c KindOfBlock Source #

toConstr :: KindOfBlock -> Constr Source #

dataTypeOf :: KindOfBlock -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c KindOfBlock) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KindOfBlock) Source #

gmapT :: (forall b. Data b => b -> b) -> KindOfBlock -> KindOfBlock Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KindOfBlock -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> KindOfBlock -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> KindOfBlock -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> KindOfBlock -> m KindOfBlock Source #

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

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

Methods

compare :: KindOfBlock -> KindOfBlock -> Ordering Source #

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

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

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

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

max :: KindOfBlock -> KindOfBlock -> KindOfBlock Source #

min :: KindOfBlock -> KindOfBlock -> KindOfBlock Source #

declName :: NiceDeclaration -> String Source #

data InMutual Source #

Constructors

InMutual | we are nicifying a mutual block
NotInMutual | we are nicifying decls not in a mutual block

#### Instances

Instances details

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

data DataRecOrFun Source #

The kind of the forward declaration.

Constructors

DataName | Name of a data type

Fields

- _kindPosCheck :: PositivityCheck
- _kindUniCheck :: UniverseCheck

RecName | Name of a record type

Fields

- _kindPosCheck :: PositivityCheck
- _kindUniCheck :: UniverseCheck

FunName TerminationCheck CoverageCheck | Name of a function.

#### Instances

Instances details

Pretty DataRecOrFun Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods pretty :: DataRecOrFun -> Doc Source # prettyPrec :: Int -> DataRecOrFun -> Doc Source # prettyList :: [DataRecOrFun] -> Doc Source #
Data DataRecOrFun Source # |

Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataRecOrFun -> c DataRecOrFun Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataRecOrFun Source #

toConstr :: DataRecOrFun -> Constr Source #

dataTypeOf :: DataRecOrFun -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataRecOrFun) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataRecOrFun) Source #

gmapT :: (forall b. Data b => b -> b) -> DataRecOrFun -> DataRecOrFun Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataRecOrFun -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> DataRecOrFun -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DataRecOrFun -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataRecOrFun -> m DataRecOrFun Source #

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

isFunName :: DataRecOrFun -> Bool Source #

sameKind :: DataRecOrFun -> DataRecOrFun -> Bool Source #

terminationCheck :: DataRecOrFun -> TerminationCheck Source #

coverageCheck :: DataRecOrFun -> CoverageCheck Source #

positivityCheck :: DataRecOrFun -> PositivityCheck Source #

mutualChecks :: DataRecOrFun -> MutualChecks Source #

universeCheck :: DataRecOrFun -> UniverseCheck Source #