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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Abstract

Contents

- Orphan instances

Description

The abstract syntax. This is what you get after desugaring and scope analysis of the concrete syntax. The type checker works on abstract syntax, producing internal syntax (Agda.Syntax.Internal).

Synopsis

- data Expr
  - = Var Name
  - | Def' QName Suffix
  - | Proj ProjOrigin AmbiguousQName
  - | Con AmbiguousQName
  - | PatternSyn AmbiguousQName
  - | Macro QName
  - | Lit ExprInfo Literal
  - | QuestionMark MetaInfo InteractionId
  - | Underscore MetaInfo
  - | Dot ExprInfo Expr
  - | App AppInfo Expr (NamedArg Expr)
  - | WithApp ExprInfo Expr (List1 Expr)
  - | Lam ExprInfo LamBinding Expr
  - | AbsurdLam ExprInfo Hiding
  - | ExtendedLam ExprInfo DefInfo Erased QName (List1 Clause)
  - | Pi ExprInfo Telescope1 Type
  - | Generalized (Set1 QName) Type
  - | Fun ExprInfo (Arg Type) Type
  - | Let ExprInfo (List1 LetBinding) Expr
  - | Rec KwRange ExprInfo RecordAssigns
  - | RecUpdate KwRange ExprInfo Expr Assigns
  - | ScopedExpr ScopeInfo Expr
  - | Quote ExprInfo
  - | QuoteTerm ExprInfo
  - | Unquote ExprInfo
  - | DontCare Expr
- type Constructor = TypeSignature
- type Type = Expr
- type Clause = Clause' LHS
- data Clause' lhs = Clause {
  - clauseLHS :: lhs
  - clauseStrippedPats :: [ProblemEq]
  - clauseRHS :: RHS
  - clauseWhereDecls :: WhereDeclarations
  - clauseCatchall :: Catchall
  }
- app :: Expr -> [NamedArg Expr] -> Expr
- data Declaration
  - = Axiom KindOfName DefInfo ArgInfo (Maybe PragmaPolarities) QName Type
  - | Generalize (Set QName) DefInfo ArgInfo QName Type
  - | Field DefInfo QName (Arg Type)
  - | Primitive DefInfo QName (Arg Type)
  - | Mutual MutualInfo [Declaration]
  - | Section Range Erased ModuleName GeneralizeTelescope [Declaration]
  - | Apply ModuleInfo Erased ModuleName ModuleApplication ScopeCopyInfo ImportDirective
  - | Import ModuleInfo ModuleName ImportDirective
  - | Pragma Range Pragma
  - | Open ModuleInfo ModuleName ImportDirective
  - | FunDef DefInfo QName [Clause]
  - | DataSig DefInfo Erased QName GeneralizeTelescope Type
  - | DataDef DefInfo QName UniverseCheck DataDefParams [Constructor]
  - | RecSig DefInfo Erased QName GeneralizeTelescope Type
  - | RecDef DefInfo QName UniverseCheck RecordDirectives DataDefParams Type [Declaration]
  - | PatternSynDef QName [WithHiding BindName] (Pattern' Void)
  - | UnquoteDecl MutualInfo [DefInfo] [QName] Expr
  - | UnquoteDef [DefInfo] [QName] Expr
  - | UnquoteData [DefInfo] QName UniverseCheck [DefInfo] [QName] Expr
  - | ScopedDecl ScopeInfo [Declaration]
  - | UnfoldingDecl Range [QName]
- type Pattern = Pattern' Expr
- data Pragma
  - = OptionsPragma [String]
  - | BuiltinPragma RString ResolvedName
  - | BuiltinNoDefPragma RString KindOfName QName
  - | RewritePragma Range [QName]
  - | CompilePragma (Ranged BackendName) QName String
  - | StaticPragma QName
  - | EtaPragma QName
  - | InjectivePragma QName
  - | InjectiveForInferencePragma QName
  - | InlinePragma Bool QName
  - | NotProjectionLikePragma QName
  - | OverlapPragma QName OverlapMode
  - | DisplayPragma QName [NamedArg Pattern] Expr
- data Pattern' e
  - = VarP BindName
  - | ConP ConPatInfo AmbiguousQName (NAPs e)
  - | ProjP PatInfo ProjOrigin AmbiguousQName
  - | DefP PatInfo AmbiguousQName (NAPs e)
  - | WildP PatInfo
  - | AsP PatInfo BindName (Pattern' e)
  - | DotP PatInfo e
  - | AbsurdP PatInfo
  - | LitP PatInfo Literal
  - | PatternSynP PatInfo AmbiguousQName (NAPs e)
  - | RecP KwRange ConPatInfo [FieldAssignment' (Pattern' e)]
  - | EqualP PatInfo (List1 (e, e))
  - | WithP PatInfo (Pattern' e)
- type Telescope = [TypedBinding]
- type Assign = FieldAssignment' Expr
- pattern Def :: QName -> Expr
- data LHS = LHS {
  - lhsInfo :: LHSInfo
  - lhsCore :: LHSCore
  }
- type TacticAttribute = TacticAttribute' Expr
- data Binder' a = Binder {
  - binderPattern :: Maybe Pattern
  - binderNameOrigin :: BinderNameOrigin
  - binderName :: a
  }
- type Binder = Binder' BindName
- mkBinder_ :: Name -> Binder
- mkBinder :: a -> Binder' a
- data LamBinding
  - = DomainFree TacticAttribute (NamedArg Binder)
  - | DomainFull TypedBinding
- data TypedBinding
  - = TBind Range TypedBindingInfo (List1 (NamedArg Binder)) Type
  - | TLet Range (List1 LetBinding)
- type Telescope1 = List1 TypedBinding
- mkLet :: ExprInfo -> [LetBinding] -> Expr -> Expr
- mkTLet :: Range -> [LetBinding] -> Maybe TypedBinding
- type RecordDirectives = RecordDirectives' RecordConName
- data ModuleApplication
  - = SectionApp Telescope ModuleName [NamedArg Expr]
  - | RecordModuleInstance ModuleName
- type TypeSignature = Declaration
- type ImportDirective = ImportDirective' QName ModuleName
- type ImportedName = ImportedName' QName ModuleName
- type Renaming = Renaming' QName ModuleName
- type RewriteEqn = RewriteEqn' QName BindName Pattern Expr
- type WithExpr = WithExpr' Expr
- type LHSCore = LHSCore' Expr
- data RHS
  - = RHS {
    - rhsExpr :: Expr
    - rhsConcrete :: Maybe Expr
    }
  - | AbsurdRHS
  - | WithRHS QName (List1 WithExpr) (List1 Clause)
  - | RewriteRHS {
    - rewriteExprs :: [RewriteEqn]
    - rewriteStrippedPats :: [ProblemEq]
    - rewriteRHS :: RHS
    - rewriteWhereDecls :: WhereDeclarations
    }
- type HoleContent = HoleContent' () BindName Pattern Expr
- data ScopeCopyInfo = ScopeCopyInfo {
  - renModules :: Ren ModuleName
  - renNames :: Ren QName
  }
- type Ren a = Map a (List1 a)
- type PatternSynDefn = ([WithHiding Name], Pattern' Void)
- type PatternSynDefns = Map QName PatternSynDefn
- data ProblemEq = ProblemEq {
  - problemInPat :: Pattern
  - problemInst :: Term
  - problemType :: Dom Type
  }
- data TypedBindingInfo = TypedBindingInfo {
  - tbTacticAttr :: TacticAttribute
  - tbFinite :: Bool
  }
- type Args = [NamedArg Expr]
- type Field = TypeSignature
- type NAPs e = [NamedArg (Pattern' e)]
- data LHSCore' e
  - = LHSHead {
    - lhsDefName :: QName
    - lhsPats :: [NamedArg (Pattern' e)]
    }
  - | LHSProj {
    - lhsDestructor :: AmbiguousQName
    - lhsFocus :: NamedArg (LHSCore' e)
    - lhsPats :: [NamedArg (Pattern' e)]
    }
  - | LHSWith {
    - lhsHead :: LHSCore' e
    - lhsWithPatterns :: List1 (Arg (Pattern' e))
    - lhsPats :: [NamedArg (Pattern' e)]
    }
- type DefInfo = DefInfo' Expr
- newtype BindName = BindName {
  - unBind :: Name
  }
- mkBindName :: Name -> BindName
- data LetBinding
  - = LetBind LetInfo ArgInfo BindName Type Expr
  - | LetAxiom LetInfo ArgInfo BindName Type
  - | LetPatBind LetInfo Pattern Expr
  - | LetApply ModuleInfo Erased ModuleName ModuleApplication ScopeCopyInfo ImportDirective
  - | LetOpen ModuleInfo ModuleName ImportDirective
- type RecordAssigns = [RecordAssign]
- type Assigns = [Assign]
- generalized :: Set QName -> Type -> Type
- type RecordAssign = Either Assign ModuleName
- initCopyInfo :: ScopeCopyInfo
- data RecordConName
  - = NamedRecCon {
    - recordConName :: !QName
    }
  - | FreshRecCon {
    - recordConName :: !QName
    }
- data GeneralizeTelescope = GeneralizeTel {
  - generalizeTelVars :: Map QName Name
  - generalizeTel :: Telescope
  }
- data DataDefParams = DataDefParams {
  - dataDefGeneralizedParams :: Set Name
  - dataDefParams :: [LamBinding]
  }
- insertedBinder :: a -> Binder' a
- insertedBinder_ :: Name -> Binder
- extractPattern :: Binder' a -> Maybe (Pattern, a)
- mkDomainFree :: NamedArg Binder -> LamBinding
- mkTBind :: Range -> List1 (NamedArg Binder) -> Type -> TypedBinding
- mkPi :: ExprInfo -> Telescope -> Type -> Type
- noDataDefParams :: DataDefParams
- data WhereDeclarations = WhereDecls {
  - whereModule :: Maybe ModuleName
  - whereAnywhere :: Bool
  - whereDecls :: Maybe Declaration
  }
- noWhereDecls :: WhereDeclarations
- type SpineClause = Clause' SpineLHS
- data SpineLHS = SpineLHS {
  - spLhsInfo :: LHSInfo
  - spLhsDefName :: QName
  - spLhsPats :: [NamedArg Pattern]
  }
- type WithExpr' e = Named BindName (Arg e)
- type NAPs1 e = List1 (NamedArg (Pattern' e))
- type Patterns = [NamedArg Pattern]
- axiomName :: Declaration -> QName
- class AnyAbstract a where
  - anyAbstract :: a -> Bool
- class NameToExpr a where
  - nameToExpr :: a -> Expr
- lambdaLiftExpr :: [WithHiding Name] -> Expr -> Expr
- class SubstExpr a where
  - substExpr :: [(Name, Expr)] -> a -> a
- insertImplicitPatSynArgs :: HasRange a => (Hiding -> Range -> a) -> Range -> [WithHiding Name] -> [NamedArg a] -> Maybe ([(Name, a)], [WithHiding Name])
- data DeclarationSpine
  - = AxiomS
  - | GeneralizeS
  - | FieldS
  - | PrimitiveS
  - | MutualS [DeclarationSpine]
  - | SectionS [DeclarationSpine]
  - | ApplyS
  - | ImportS
  - | PragmaS
  - | OpenS
  - | FunDefS [ClauseSpine]
  - | DataSigS
  - | DataDefS
  - | RecSigS
  - | RecDefS [DeclarationSpine]
  - | PatternSynDefS
  - | UnquoteDeclS
  - | UnquoteDefS
  - | UnquoteDataS
  - | ScopedDeclS [DeclarationSpine]
  - | UnfoldingDeclS
- data ClauseSpine = ClauseS RHSSpine WhereDeclarationsSpine
- data RHSSpine
  - = RHSS
  - | AbsurdRHSS
  - | WithRHSS (List1 ClauseSpine)
  - | RewriteRHSS RHSSpine WhereDeclarationsSpine
- data WhereDeclarationsSpine = WhereDeclsS (Maybe DeclarationSpine)
- declarationSpine :: Declaration -> DeclarationSpine
- clauseSpine :: Clause -> ClauseSpine
- rhsSpine :: RHS -> RHSSpine
- whereDeclarationsSpine :: WhereDeclarations -> WhereDeclarationsSpine
- module Agda.Syntax.Abstract.Name

# Documentation

data Expr Source #

Expressions after scope checking (operators parsed, names resolved).

Constructors

Var Name | Bound variable.
Def' QName Suffix | Constant: axiom, function, data or record type, with a possible suffix.
Proj ProjOrigin AmbiguousQName | Projection (overloaded).
Con AmbiguousQName | Constructor (overloaded).
PatternSyn AmbiguousQName | Pattern synonym.
Macro QName | Macro.
Lit ExprInfo Literal | Literal.
QuestionMark MetaInfo InteractionId | Meta variable for interaction. The `InteractionId` is usually identical with the `metaNumber` of `MetaInfo`. However, if you want to print an interaction meta as just `?` instead of `?n`, you should set the `metaNumber` to `Nothing` while keeping the `InteractionId`.
Underscore MetaInfo | Meta variable for hidden argument (must be inferred locally).
Dot ExprInfo Expr | `.e`, for postfix projection.
App AppInfo Expr (NamedArg Expr) | Ordinary (binary) application.
WithApp ExprInfo Expr (List1 Expr) | With application.
Lam ExprInfo LamBinding Expr | `λ bs → e`.
AbsurdLam ExprInfo Hiding | `λ()` or `λ{}`.
ExtendedLam ExprInfo DefInfo Erased QName (List1 Clause) |
Pi ExprInfo Telescope1 Type | Dependent function space `Γ → A`.
Generalized (Set1 QName) Type | Like a Pi, but the ordering is not known
Fun ExprInfo (Arg Type) Type | Non-dependent function space.
Let ExprInfo (List1 LetBinding) Expr | `let bs in e`.
Rec KwRange ExprInfo RecordAssigns | Record construction. The `KwRange` is for the `record` kewyword.
RecUpdate KwRange ExprInfo Expr Assigns | Record update. The `KwRange` is for the `record` kewyword.
ScopedExpr ScopeInfo Expr | Scope annotation.
Quote ExprInfo | Quote an identifier `QName`.
QuoteTerm ExprInfo | Quote a term.
Unquote ExprInfo | The splicing construct: unquote ...
DontCare Expr | For printing `DontCare` from `Syntax.Internal`.

#### Instances

Instances details

SubstExpr Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Expr -> Expr Source #
IsProjP Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods isProjP :: Expr -> Maybe (ProjOrigin, AmbiguousQName) Source #
MapNamedArgPattern NAP Source # |
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #
ExprLike Expr Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m Expr Source # foldExpr :: FoldExprFn m Expr Source # traverseExpr :: TraverseExprFn m Expr Source # mapExpr :: (Expr -> Expr) -> Expr -> Expr Source #
Underscore Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods underscore :: Expr Source # isUnderscore :: Expr -> Bool Source #
HasRange Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Expr -> Range Source #
KillRange Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT Expr Source #
ToConcrete Expr Source # |

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Expr |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Expr = Expr

Methods

toConcrete :: MonadToConcrete m => Expr -> m (ConOfAbs Expr) Source #

bindToConcrete :: MonadToConcrete m => Expr -> (ConOfAbs Expr -> m b) -> m b Source #

ToConcrete LHSCore Source # |

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHSCore |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LHSCore = Pattern

Methods

toConcrete :: MonadToConcrete m => LHSCore -> m (ConOfAbs LHSCore) Source #

bindToConcrete :: MonadToConcrete m => LHSCore -> (ConOfAbs LHSCore -> m b) -> m b Source #

ToConcrete Pattern Source # |

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Pattern |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Pattern = Pattern

Methods

toConcrete :: MonadToConcrete m => Pattern -> m (ConOfAbs Pattern) Source #

bindToConcrete :: MonadToConcrete m => Pattern -> (ConOfAbs Pattern -> m b) -> m b Source #

Reify Expr Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

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

Methods

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

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

PrettyTCM Expr Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Expr -> m Doc Source #
PrettyTCM Pattern Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Pattern -> m Doc Source #
IsFlexiblePattern Pattern Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Pattern -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Pattern -> m Bool Source #
EmbPrj Pattern Source # | Hackish serialization for patterns that deletes dot patterns. So that we can serialize the `WithClauseProjectionFixityMismatch` without having to define serialization of expressions.
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Pattern -> S Word32 Source # icod_ :: Pattern -> S Word32 Source # value :: Word32 -> R Pattern Source #
NFData Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Expr -> () Source #
Generic Expr Source # |

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep Expr |

Instance details

Defined in Agda.Syntax.Abstract

type Rep Expr = D1 ('MetaData "Expr" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((((C1 ('MetaCons "Var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: (C1 ('MetaCons "Def'" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Suffix)) :+: C1 ('MetaCons "Proj" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProjOrigin) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)))) :+: (C1 ('MetaCons "Con" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)) :+: (C1 ('MetaCons "PatternSyn" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)) :+: C1 ('MetaCons "Macro" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))))) :+: ((C1 ('MetaCons "Lit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: (C1 ('MetaCons "QuestionMark" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InteractionId)) :+: C1 ('MetaCons "Underscore" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaInfo)))) :+: ((C1 ('MetaCons "Dot" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "App" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AppInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg Expr))))) :+: (C1 ('MetaCons "WithApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 Expr)))) :+: C1 ('MetaCons "Lam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LamBinding) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))))) :+: (((C1 ('MetaCons "AbsurdLam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Hiding)) :+: (C1 ('MetaCons "ExtendedLam" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 Clause))))) :+: C1 ('MetaCons "Pi" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope1) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))))) :+: (C1 ('MetaCons "Generalized" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set1 QName)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: (C1 ('MetaCons "Fun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) :+: C1 ('MetaCons "Let" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 LetBinding)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))))) :+: ((C1 ('MetaCons "Rec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RecordAssigns))) :+: (C1 ('MetaCons "RecUpdate" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Assigns))) :+: C1 ('MetaCons "ScopedExpr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: ((C1 ('MetaCons "Quote" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo)) :+: C1 ('MetaCons "QuoteTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo))) :+: (C1 ('MetaCons "Unquote" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo)) :+: C1 ('MetaCons "DontCare" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))))))

Methods

from :: Expr -> Rep Expr x Source #

to :: Rep Expr x -> Expr Source #

Show Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Expr -> ShowS Source # show :: Expr -> String Source # showList :: [Expr] -> ShowS Source #
Eq Expr Source # | Does not compare `ScopeInfo` fields. Does not distinguish between prefix and postfix projections.
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Expr -> Expr -> Bool Source # (/=) :: Expr -> Expr -> Bool Source #
PatternToExpr Pattern Expr Source # |
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods patToExpr :: Pattern -> Reader Hiding Expr Source #
PrettyTCM (Arg Expr) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Arg Expr -> m Doc Source #
PrettyTCM (NamedArg Expr) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedArg Expr -> m Doc Source #
ToAbstract (Expr, Elim) Source # |

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elim) |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elim) = Expr

Methods

toAbstract :: MonadReflectedToAbstract m => (Expr, Elim) -> m (AbsOfRef (Expr, Elim)) Source #

ToAbstract (Expr, Elims) Source # |

Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elims) |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elims) = Expr

Methods

toAbstract :: MonadReflectedToAbstract m => (Expr, Elims) -> m (AbsOfRef (Expr, Elims)) Source #

ToAbstract (RewriteEqn' () BindName Pattern Expr) Source # |

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (RewriteEqn' () BindName Pattern Expr) |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqn

Methods

toAbstract :: RewriteEqn' () BindName Pattern Expr -> ScopeM (AbsOfCon (RewriteEqn' () BindName Pattern Expr)) Source #

type ConOfAbs Expr Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Expr = Expr
type ConOfAbs LHSCore Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LHSCore = Pattern
type ConOfAbs Pattern Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Pattern = Pattern
type ReifiesTo Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Expr = Expr
type Rep Expr Source # |

Instance details

Defined in Agda.Syntax.Abstract

type Rep Expr = D1 ('MetaData "Expr" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((((C1 ('MetaCons "Var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: (C1 ('MetaCons "Def'" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Suffix)) :+: C1 ('MetaCons "Proj" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProjOrigin) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)))) :+: (C1 ('MetaCons "Con" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)) :+: (C1 ('MetaCons "PatternSyn" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)) :+: C1 ('MetaCons "Macro" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))))) :+: ((C1 ('MetaCons "Lit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: (C1 ('MetaCons "QuestionMark" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InteractionId)) :+: C1 ('MetaCons "Underscore" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaInfo)))) :+: ((C1 ('MetaCons "Dot" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "App" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AppInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg Expr))))) :+: (C1 ('MetaCons "WithApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 Expr)))) :+: C1 ('MetaCons "Lam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LamBinding) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))))) :+: (((C1 ('MetaCons "AbsurdLam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Hiding)) :+: (C1 ('MetaCons "ExtendedLam" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 Clause))))) :+: C1 ('MetaCons "Pi" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope1) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))))) :+: (C1 ('MetaCons "Generalized" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set1 QName)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: (C1 ('MetaCons "Fun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) :+: C1 ('MetaCons "Let" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 LetBinding)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))))) :+: ((C1 ('MetaCons "Rec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RecordAssigns))) :+: (C1 ('MetaCons "RecUpdate" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Assigns))) :+: C1 ('MetaCons "ScopedExpr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: ((C1 ('MetaCons "Quote" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo)) :+: C1 ('MetaCons "QuoteTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo))) :+: (C1 ('MetaCons "Unquote" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo)) :+: C1 ('MetaCons "DontCare" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))))))

type AbsOfRef (Expr, Elim) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elim) = Expr
type AbsOfRef (Expr, Elims) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elims) = Expr
type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqn

type Constructor = TypeSignature Source #

type Type = Expr Source #

Types are just expressions. Use this type synonym for hinting that an expression should be a type.

type Clause = Clause' LHS Source #

data Clause' lhs Source #

We could throw away `where` clauses at this point and translate them to `let`. It's not obvious how to remember that the `let` was really a `where` clause though, so for the time being we keep it here.

Constructors

Clause |

Fields

- clauseLHS :: lhs
- clauseStrippedPats :: [ProblemEq]

  Only in with-clauses where we inherit some already checked patterns from the parent. These live in the context of the parent clause left-hand side.

- clauseRHS :: RHS
- clauseWhereDecls :: WhereDeclarations
- clauseCatchall :: Catchall

#### Instances

Instances details

DeclaredNames Clause Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => Clause -> m Source #
Functor Clause' Source # |
Instance details Defined in Agda.Syntax.Abstract Methods fmap :: (a -> b) -> Clause' a -> Clause' b Source # (<$) :: a -> Clause' b -> Clause' a Source #
Foldable Clause' Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

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

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

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

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

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

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

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

null :: Clause' a -> Bool Source #

length :: Clause' a -> Int Source #

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

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

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

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

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

Traversable Clause' Source # |
Instance details Defined in Agda.Syntax.Abstract Methods traverse :: Applicative f => (a -> f b) -> Clause' a -> f (Clause' b) Source # sequenceA :: Applicative f => Clause' (f a) -> f (Clause' a) Source # mapM :: Monad m => (a -> m b) -> Clause' a -> m (Clause' b) Source # sequence :: Monad m => Clause' (m a) -> m (Clause' a) Source #
LHSToSpine Clause SpineClause Source # | Clause instance.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: Clause -> SpineClause Source # spineToLhs :: SpineClause -> Clause Source #
ExprLike a => ExprLike (Clause' a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (Clause' a) Source # foldExpr :: FoldExprFn m (Clause' a) Source # traverseExpr :: TraverseExprFn m (Clause' a) Source # mapExpr :: (Expr -> Expr) -> Clause' a -> Clause' a Source #
HasRange a => HasRange (Clause' a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Clause' a -> Range Source #
KillRange a => KillRange (Clause' a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (Clause' a) Source #
(ToConcrete a, ConOfAbs a ~ LHS) => ToConcrete (Clause' a) Source # |

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Clause' a) |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Clause' a) = List1 Declaration

Methods

toConcrete :: MonadToConcrete m => Clause' a -> m (ConOfAbs (Clause' a)) Source #

bindToConcrete :: MonadToConcrete m => Clause' a -> (ConOfAbs (Clause' a) -> m b) -> m b Source #

NFData lhs => NFData (Clause' lhs) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Clause' lhs -> () Source #
Generic (Clause' lhs) Source # |

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep (Clause' lhs) |

Instance details

Defined in Agda.Syntax.Abstract

type Rep (Clause' lhs) = D1 ('MetaData "Clause'" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Clause" 'PrefixI 'True) ((S1 ('MetaSel ('Just "clauseLHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 lhs) :*: S1 ('MetaSel ('Just "clauseStrippedPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ProblemEq])) :*: (S1 ('MetaSel ('Just "clauseRHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RHS) :*: (S1 ('MetaSel ('Just "clauseWhereDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhereDeclarations) :*: S1 ('MetaSel ('Just "clauseCatchall") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Catchall)))))

Methods

from :: Clause' lhs -> Rep (Clause' lhs) x Source #

to :: Rep (Clause' lhs) x -> Clause' lhs Source #

Show lhs => Show (Clause' lhs) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Clause' lhs -> ShowS Source # show :: Clause' lhs -> String Source # showList :: [Clause' lhs] -> ShowS Source #
Eq lhs => Eq (Clause' lhs) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Clause' lhs -> Clause' lhs -> Bool Source # (/=) :: Clause' lhs -> Clause' lhs -> Bool Source #
type ConOfAbs (Clause' a) Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Clause' a) = List1 Declaration
type Rep (Clause' lhs) Source # |

Instance details

Defined in Agda.Syntax.Abstract

type Rep (Clause' lhs) = D1 ('MetaData "Clause'" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Clause" 'PrefixI 'True) ((S1 ('MetaSel ('Just "clauseLHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 lhs) :*: S1 ('MetaSel ('Just "clauseStrippedPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ProblemEq])) :*: (S1 ('MetaSel ('Just "clauseRHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RHS) :*: (S1 ('MetaSel ('Just "clauseWhereDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhereDeclarations) :*: S1 ('MetaSel ('Just "clauseCatchall") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Catchall)))))

app :: Expr -> [NamedArg Expr] -> Expr Source #

data Declaration Source #

Constructors

Axiom KindOfName DefInfo ArgInfo (Maybe PragmaPolarities) QName Type | Type signature (can be irrelevant, but not hidden). The fourth argument contains an optional assignment of polarities to arguments.
Generalize (Set QName) DefInfo ArgInfo QName Type | The first argument is the (possibly empty) set of generalizable variables used in the type.
Field DefInfo QName (Arg Type) | record field
Primitive DefInfo QName (Arg Type) | primitive function
Mutual MutualInfo [Declaration] | a bunch of mutually recursive definitions
Section Range Erased ModuleName GeneralizeTelescope [Declaration] |
Apply ModuleInfo Erased ModuleName ModuleApplication ScopeCopyInfo ImportDirective | The `ImportDirective` is for highlighting purposes.
Import ModuleInfo ModuleName ImportDirective | The `ImportDirective` is for highlighting purposes.
Pragma Range Pragma |
Open ModuleInfo ModuleName ImportDirective |
FunDef DefInfo QName [Clause] | sequence of function clauses
DataSig DefInfo Erased QName GeneralizeTelescope Type | lone data signature
DataDef DefInfo QName UniverseCheck DataDefParams [Constructor] |
RecSig DefInfo Erased QName GeneralizeTelescope Type | lone record signature
RecDef DefInfo QName UniverseCheck RecordDirectives DataDefParams Type [Declaration] | The `Type` gives the constructor type telescope, `(x1 : A1)..(xn : An) -> Dummy`, and the optional name is the constructor's name. The optional `Range` is for the `pattern` attribute.
PatternSynDef QName [WithHiding BindName] (Pattern' Void) | Only for highlighting purposes
UnquoteDecl MutualInfo [DefInfo] [QName] Expr |
UnquoteDef [DefInfo] [QName] Expr |
UnquoteData [DefInfo] QName UniverseCheck [DefInfo] [QName] Expr |
ScopedDecl ScopeInfo [Declaration] | scope annotation
UnfoldingDecl Range [QName] | Only for highlighting the unfolded names

#### Instances

Instances details

AnyAbstract Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract Methods anyAbstract :: Declaration -> Bool Source #
DeclaredNames Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => Declaration -> m Source #
ExprLike Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m Declaration Source # foldExpr :: FoldExprFn m Declaration Source # traverseExpr :: TraverseExprFn m Declaration Source # mapExpr :: (Expr -> Expr) -> Declaration -> Declaration Source #
HasRange Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Declaration -> Range Source #
KillRange Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT Declaration Source #
ToConcrete Declaration Source # |

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Declaration |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Declaration = [Declaration]

Methods

toConcrete :: MonadToConcrete m => Declaration -> m (ConOfAbs Declaration) Source #

bindToConcrete :: MonadToConcrete m => Declaration -> (ConOfAbs Declaration -> m b) -> m b Source #

ShowHead Declaration Source # |
Instance details Defined in Agda.TypeChecking.Rules.Decl Methods showHead :: Declaration -> String Source #
NFData Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Declaration -> () Source #
Generic Declaration Source # |

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep Declaration |

Instance details

Defined in Agda.Syntax.Abstract

type Rep Declaration = D1 ('MetaData "Declaration" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((((C1 ('MetaCons "Axiom" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe PragmaPolarities)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))) :+: C1 ('MetaCons "Generalize" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set QName)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))))) :+: (C1 ('MetaCons "Field" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Type)))) :+: (C1 ('MetaCons "Primitive" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Type)))) :+: C1 ('MetaCons "Mutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MutualInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration]))))) :+: ((C1 ('MetaCons "Section" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralizeTelescope) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])))) :+: C1 ('MetaCons "Apply" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleApplication) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeCopyInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))))) :+: (C1 ('MetaCons "Import" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))) :+: (C1 ('MetaCons "Pragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pragma)) :+: C1 ('MetaCons "Open" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))))))) :+: (((C1 ('MetaCons "FunDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause]))) :+: C1 ('MetaCons "DataSig" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralizeTelescope) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))))) :+: (C1 ('MetaCons "DataDef" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataDefParams) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Constructor])))) :+: (C1 ('MetaCons "RecSig" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralizeTelescope) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))) :+: C1 ('MetaCons "RecDef" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RecordDirectives) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataDefParams)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration]))))))) :+: ((C1 ('MetaCons "PatternSynDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [WithHiding BindName]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' Void)))) :+: (C1 ('MetaCons "UnquoteDecl" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MutualInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefInfo])) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: C1 ('MetaCons "UnquoteDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefInfo]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))) :+: (C1 ('MetaCons "UnquoteData" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefInfo]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefInfo]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: (C1 ('MetaCons "ScopedDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])) :+: C1 ('MetaCons "UnfoldingDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName])))))))

Methods

from :: Declaration -> Rep Declaration x Source #

to :: Rep Declaration x -> Declaration Source #

Show Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Declaration -> ShowS Source # show :: Declaration -> String Source # showList :: [Declaration] -> ShowS Source #
Eq Declaration Source # | Does not compare `ScopeInfo` fields.
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Declaration -> Declaration -> Bool Source # (/=) :: Declaration -> Declaration -> Bool Source #
ToConcrete (Constr Constructor) Source # |

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Constr Constructor) |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Constr Constructor) = Declaration

Methods

toConcrete :: MonadToConcrete m => Constr Constructor -> m (ConOfAbs (Constr Constructor)) Source #

bindToConcrete :: MonadToConcrete m => Constr Constructor -> (ConOfAbs (Constr Constructor) -> m b) -> m b Source #

type ConOfAbs Declaration Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Declaration = [Declaration]
type Rep Declaration Source # |

Instance details

Defined in Agda.Syntax.Abstract

type Rep Declaration = D1 ('MetaData "Declaration" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((((C1 ('MetaCons "Axiom" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe PragmaPolarities)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))) :+: C1 ('MetaCons "Generalize" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set QName)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))))) :+: (C1 ('MetaCons "Field" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Type)))) :+: (C1 ('MetaCons "Primitive" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Type)))) :+: C1 ('MetaCons "Mutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MutualInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration]))))) :+: ((C1 ('MetaCons "Section" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralizeTelescope) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])))) :+: C1 ('MetaCons "Apply" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleApplication) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeCopyInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))))) :+: (C1 ('MetaCons "Import" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))) :+: (C1 ('MetaCons "Pragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pragma)) :+: C1 ('MetaCons "Open" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))))))) :+: (((C1 ('MetaCons "FunDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause]))) :+: C1 ('MetaCons "DataSig" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralizeTelescope) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))))) :+: (C1 ('MetaCons "DataDef" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataDefParams) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Constructor])))) :+: (C1 ('MetaCons "RecSig" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralizeTelescope) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))) :+: C1 ('MetaCons "RecDef" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RecordDirectives) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataDefParams)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration]))))))) :+: ((C1 ('MetaCons "PatternSynDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [WithHiding BindName]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' Void)))) :+: (C1 ('MetaCons "UnquoteDecl" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MutualInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefInfo])) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: C1 ('MetaCons "UnquoteDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefInfo]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))) :+: (C1 ('MetaCons "UnquoteData" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefInfo]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefInfo]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: (C1 ('MetaCons "ScopedDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])) :+: C1 ('MetaCons "UnfoldingDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName])))))))

type ConOfAbs (Constr Constructor) Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Constr Constructor) = Declaration

type Pattern = Pattern' Expr Source #

data Pragma Source #

Constructors

OptionsPragma [String] |
BuiltinPragma RString ResolvedName | `ResolvedName` is not `UnknownName`. Name can be ambiguous e.g. for built-in constructors.
BuiltinNoDefPragma RString KindOfName QName | Builtins that do not come with a definition, but declare a name for an Agda concept.
RewritePragma Range [QName] | Range is range of REWRITE keyword.
CompilePragma (Ranged BackendName) QName String |
StaticPragma QName |
EtaPragma QName | For coinductive records, use pragma instead of regular `eta-equality` definition (as it is might make Agda loop).
InjectivePragma QName |
InjectiveForInferencePragma QName |
InlinePragma Bool QName |
NotProjectionLikePragma QName | Mark the definition as not being projection-like
OverlapPragma QName OverlapMode | If the definition is an instance, set its overlap mode.
DisplayPragma QName [NamedArg Pattern] Expr |

#### Instances

Instances details

DeclaredNames Pragma Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => Pragma -> m Source #
ExprLike Pragma Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m Pragma Source # foldExpr :: FoldExprFn m Pragma Source # traverseExpr :: TraverseExprFn m Pragma Source # mapExpr :: (Expr -> Expr) -> Pragma -> Pragma Source #
NFData Pragma Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Pragma -> () Source #
Generic Pragma Source # |

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep Pragma |

Instance details

Defined in Agda.Syntax.Abstract

type Rep Pragma = D1 ('MetaData "Pragma" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (((C1 ('MetaCons "OptionsPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])) :+: (C1 ('MetaCons "BuiltinPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RString) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ResolvedName)) :+: C1 ('MetaCons "BuiltinNoDefPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RString) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))))) :+: (C1 ('MetaCons "RewritePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName])) :+: (C1 ('MetaCons "CompilePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Ranged BackendName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) :+: C1 ('MetaCons "StaticPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))))) :+: ((C1 ('MetaCons "EtaPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: (C1 ('MetaCons "InjectivePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "InjectiveForInferencePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)))) :+: ((C1 ('MetaCons "InlinePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "NotProjectionLikePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))) :+: (C1 ('MetaCons "OverlapPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OverlapMode)) :+: C1 ('MetaCons "DisplayPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg Pattern]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))))))

Methods

from :: Pragma -> Rep Pragma x Source #

to :: Rep Pragma x -> Pragma Source #

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

Instance details

Defined in Agda.Syntax.Abstract

type Rep Pragma = D1 ('MetaData "Pragma" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (((C1 ('MetaCons "OptionsPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])) :+: (C1 ('MetaCons "BuiltinPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RString) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ResolvedName)) :+: C1 ('MetaCons "BuiltinNoDefPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RString) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))))) :+: (C1 ('MetaCons "RewritePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName])) :+: (C1 ('MetaCons "CompilePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Ranged BackendName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) :+: C1 ('MetaCons "StaticPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))))) :+: ((C1 ('MetaCons "EtaPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: (C1 ('MetaCons "InjectivePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "InjectiveForInferencePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)))) :+: ((C1 ('MetaCons "InlinePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "NotProjectionLikePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))) :+: (C1 ('MetaCons "OverlapPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OverlapMode)) :+: C1 ('MetaCons "DisplayPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg Pattern]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))))))

data Pattern' e Source #

Parameterised over the type of dot patterns.

Constructors

VarP BindName |
ConP ConPatInfo AmbiguousQName (NAPs e) |
ProjP PatInfo ProjOrigin AmbiguousQName | Destructor pattern `d`.
DefP PatInfo AmbiguousQName (NAPs e) | Defined pattern: function definition `f ps`. It is also abused to convert destructor patterns into concrete syntax thus, we put AmbiguousQName here as well.
WildP PatInfo | Underscore pattern entered by user. Or generated at type checking for implicit arguments.
AsP PatInfo BindName (Pattern' e) |
DotP PatInfo e | Dot pattern `.e`
AbsurdP PatInfo |
LitP PatInfo Literal |
PatternSynP PatInfo AmbiguousQName (NAPs e) |
RecP KwRange ConPatInfo [FieldAssignment' (Pattern' e)] |
EqualP PatInfo (List1 (e, e)) |
WithP PatInfo (Pattern' e) | `| p`, for with-patterns.

#### Instances

Instances details

MapNamedArgPattern NAP Source # |
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #
ToConcrete Pattern Source # |

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Pattern |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Pattern = Pattern

Methods

toConcrete :: MonadToConcrete m => Pattern -> m (ConOfAbs Pattern) Source #

bindToConcrete :: MonadToConcrete m => Pattern -> (ConOfAbs Pattern -> m b) -> m b Source #

PrettyTCM Pattern Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Pattern -> m Doc Source #
IsFlexiblePattern Pattern Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Pattern -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Pattern -> m Bool Source #
EmbPrj Pattern Source # | Hackish serialization for patterns that deletes dot patterns. So that we can serialize the `WithClauseProjectionFixityMismatch` without having to define serialization of expressions.
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Pattern -> S Word32 Source # icod_ :: Pattern -> S Word32 Source # value :: Word32 -> R Pattern Source #
Functor Pattern' Source # |
Instance details Defined in Agda.Syntax.Abstract Methods fmap :: (a -> b) -> Pattern' a -> Pattern' b Source # (<$) :: a -> Pattern' b -> Pattern' a Source #
Foldable Pattern' Source # |

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

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

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

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

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

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

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

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

null :: Pattern' a -> Bool Source #

length :: Pattern' a -> Int Source #

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

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

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

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

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

Traversable Pattern' Source # |
Instance details Defined in Agda.Syntax.Abstract Methods traverse :: Applicative f => (a -> f b) -> Pattern' a -> f (Pattern' b) Source # sequenceA :: Applicative f => Pattern' (f a) -> f (Pattern' a) Source # mapM :: Monad m => (a -> m b) -> Pattern' a -> m (Pattern' b) Source # sequence :: Monad m => Pattern' (m a) -> m (Pattern' a) Source #
PatternToExpr Pattern Expr Source # |
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods patToExpr :: Pattern -> Reader Hiding Expr Source #
IsProjP (Pattern' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods isProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName) Source #
APatternLike (Pattern' a) Source # |

Instance details

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (Pattern' a) |
Instance details Defined in Agda.Syntax.Abstract.Pattern type ADotT (Pattern' a) = a

Methods

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

traverseAPatternM :: Monad m => (Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))) -> (Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))) -> Pattern' a -> m (Pattern' a) Source #

ExprLike a => ExprLike (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (Pattern' a) Source # foldExpr :: FoldExprFn m (Pattern' a) Source # traverseExpr :: TraverseExprFn m (Pattern' a) Source # mapExpr :: (Expr -> Expr) -> Pattern' a -> Pattern' a Source #
IsWithP (Pattern' e) Source # | Check for with-pattern.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods isWithP :: Pattern' e -> Maybe (Pattern' e) Source #
NamesIn (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Pattern' a -> m Source #
HasRange (Pattern' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Pattern' e -> Range Source #
KillRange e => KillRange (Pattern' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (Pattern' e) Source #
SetRange (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods setRange :: Range -> Pattern' a -> Pattern' a Source #
ToAbstract (Pattern' Expr) Source # |

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Pattern' Expr) |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (Pattern' Expr) = Pattern' Expr

Methods

toAbstract :: Pattern' Expr -> ScopeM (AbsOfCon (Pattern' Expr)) Source #

ExpandPatternSynonyms (Pattern' e) Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Abstract Methods expandPatternSynonyms :: Pattern' e -> TCM (Pattern' e) Source #
EmbPrj a => EmbPrj (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Pattern' a -> S Word32 Source # icod_ :: Pattern' a -> S Word32 Source # value :: Word32 -> R (Pattern' a) Source #
NFData e => NFData (Pattern' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Pattern' e -> () Source #
Generic (Pattern' e) Source # |

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep (Pattern' e) |

Instance details

Defined in Agda.Syntax.Abstract

type Rep (Pattern' e) = D1 ('MetaData "Pattern'" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (((C1 ('MetaCons "VarP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName)) :+: (C1 ('MetaCons "ConP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConPatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NAPs e)))) :+: C1 ('MetaCons "ProjP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProjOrigin) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName))))) :+: (C1 ('MetaCons "DefP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NAPs e)))) :+: (C1 ('MetaCons "WildP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo)) :+: C1 ('MetaCons "AsP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' e))))))) :+: ((C1 ('MetaCons "DotP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 e)) :+: (C1 ('MetaCons "AbsurdP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo)) :+: C1 ('MetaCons "LitP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)))) :+: ((C1 ('MetaCons "PatternSynP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NAPs e)))) :+: C1 ('MetaCons "RecP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConPatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FieldAssignment' (Pattern' e)])))) :+: (C1 ('MetaCons "EqualP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (e, e)))) :+: C1 ('MetaCons "WithP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' e)))))))

Methods

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

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

Show e => Show (Pattern' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Pattern' e -> ShowS Source # show :: Pattern' e -> String Source # showList :: [Pattern' e] -> ShowS Source #
Eq e => Eq (Pattern' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Pattern' e -> Pattern' e -> Bool Source # (/=) :: Pattern' e -> Pattern' e -> Bool Source #
ToAbstract (RewriteEqn' () BindName Pattern Expr) Source # |

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (RewriteEqn' () BindName Pattern Expr) |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqn

Methods

toAbstract :: RewriteEqn' () BindName Pattern Expr -> ScopeM (AbsOfCon (RewriteEqn' () BindName Pattern Expr)) Source #

type ConOfAbs Pattern Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Pattern = Pattern
type ADotT (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Pattern type ADotT (Pattern' a) = a
type AbsOfCon (Pattern' Expr) Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (Pattern' Expr) = Pattern' Expr
type Rep (Pattern' e) Source # |

Instance details

Defined in Agda.Syntax.Abstract

type Rep (Pattern' e) = D1 ('MetaData "Pattern'" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (((C1 ('MetaCons "VarP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName)) :+: (C1 ('MetaCons "ConP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConPatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NAPs e)))) :+: C1 ('MetaCons "ProjP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProjOrigin) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName))))) :+: (C1 ('MetaCons "DefP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NAPs e)))) :+: (C1 ('MetaCons "WildP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo)) :+: C1 ('MetaCons "AsP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' e))))))) :+: ((C1 ('MetaCons "DotP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 e)) :+: (C1 ('MetaCons "AbsurdP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo)) :+: C1 ('MetaCons "LitP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)))) :+: ((C1 ('MetaCons "PatternSynP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NAPs e)))) :+: C1 ('MetaCons "RecP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConPatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FieldAssignment' (Pattern' e)])))) :+: (C1 ('MetaCons "EqualP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (e, e)))) :+: C1 ('MetaCons "WithP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' e)))))))

type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqn

type Telescope = [TypedBinding] Source #

type Assign = FieldAssignment' Expr Source #

Record field assignment `f = e`.

pattern Def :: QName -> Expr Source #

Pattern synonym for regular `Def`.

data LHS Source #

The lhs of a clause in focused (projection-application) view (outside-in). Projection patters are represented as `LHSProj`s.

Constructors

LHS |

Fields

- lhsInfo :: LHSInfo

  Range.

- lhsCore :: LHSCore

  Copatterns.

#### Instances

Instances details

DeclaredNames Clause Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => Clause -> m Source #
ExprLike LHS Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m LHS Source # foldExpr :: FoldExprFn m LHS Source # traverseExpr :: TraverseExprFn m LHS Source # mapExpr :: (Expr -> Expr) -> LHS -> LHS Source #
HasRange LHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LHS -> Range Source #
KillRange LHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT LHS Source #
ToConcrete LHS Source # |

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHS |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LHS = LHS

Methods

toConcrete :: MonadToConcrete m => LHS -> m (ConOfAbs LHS) Source #

bindToConcrete :: MonadToConcrete m => LHS -> (ConOfAbs LHS -> m b) -> m b Source #

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

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep LHS |
Instance details Defined in Agda.Syntax.Abstract type Rep LHS = D1 ('MetaData "LHS" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "LHS" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSInfo) :*: S1 ('MetaSel ('Just "lhsCore") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSCore)))

Methods

from :: LHS -> Rep LHS x Source #

to :: Rep LHS x -> LHS Source #

Show LHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> LHS -> ShowS Source # show :: LHS -> String Source # showList :: [LHS] -> ShowS Source #
Eq LHS Source # | Ignore `Range` when comparing `LHS`s.
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: LHS -> LHS -> Bool Source # (/=) :: LHS -> LHS -> Bool Source #
LHSToSpine Clause SpineClause Source # | Clause instance.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: Clause -> SpineClause Source # spineToLhs :: SpineClause -> Clause Source #
LHSToSpine LHS SpineLHS Source # | LHS instance.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: LHS -> SpineLHS Source # spineToLhs :: SpineLHS -> LHS Source #
type ConOfAbs LHS Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LHS = LHS
type Rep LHS Source # |
Instance details Defined in Agda.Syntax.Abstract type Rep LHS = D1 ('MetaData "LHS" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "LHS" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSInfo) :*: S1 ('MetaSel ('Just "lhsCore") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSCore)))

type TacticAttribute = TacticAttribute' Expr Source #

data Binder' a Source #

Constructors

Binder |

Fields

- binderPattern :: Maybe Pattern
- binderNameOrigin :: BinderNameOrigin
- binderName :: a

#### Instances

Instances details

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

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

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

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

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

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

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

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

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

null :: Binder' a -> Bool Source #

length :: Binder' a -> Int Source #

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

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

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

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

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

Traversable Binder' Source # |
Instance details Defined in Agda.Syntax.Abstract Methods traverse :: Applicative f => (a -> f b) -> Binder' a -> f (Binder' b) Source # sequenceA :: Applicative f => Binder' (f a) -> f (Binder' a) Source # mapM :: Monad m => (a -> m b) -> Binder' a -> m (Binder' b) Source # sequence :: Monad m => Binder' (m a) -> m (Binder' a) Source #
HasRange a => HasRange (Binder' a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Binder' a -> Range Source #
KillRange a => KillRange (Binder' a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (Binder' a) Source #
ToConcrete a => ToConcrete (Binder' a) Source # |

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Binder' a) |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Binder' a) = Binder' (ConOfAbs a)

Methods

toConcrete :: MonadToConcrete m => Binder' a -> m (ConOfAbs (Binder' a)) Source #

bindToConcrete :: MonadToConcrete m => Binder' a -> (ConOfAbs (Binder' a) -> m b) -> m b Source #

NFData a => NFData (Binder' a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Binder' a -> () Source #
Generic (Binder' a) Source # |

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep (Binder' a) |

Instance details

Defined in Agda.Syntax.Abstract

type Rep (Binder' a) = D1 ('MetaData "Binder'" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Binder" 'PrefixI 'True) (S1 ('MetaSel ('Just "binderPattern") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Pattern)) :*: (S1 ('MetaSel ('Just "binderNameOrigin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BinderNameOrigin) :*: S1 ('MetaSel ('Just "binderName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))))

Methods

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

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

Show a => Show (Binder' a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Binder' a -> ShowS Source # show :: Binder' a -> String Source # showList :: [Binder' a] -> ShowS Source #
Eq a => Eq (Binder' a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Binder' a -> Binder' a -> Bool Source # (/=) :: Binder' a -> Binder' a -> Bool Source #
type ConOfAbs (Binder' a) Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Binder' a) = Binder' (ConOfAbs a)
type Rep (Binder' a) Source # |

Instance details

Defined in Agda.Syntax.Abstract

type Rep (Binder' a) = D1 ('MetaData "Binder'" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Binder" 'PrefixI 'True) (S1 ('MetaSel ('Just "binderPattern") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Pattern)) :*: (S1 ('MetaSel ('Just "binderNameOrigin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BinderNameOrigin) :*: S1 ('MetaSel ('Just "binderName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))))

type Binder = Binder' BindName Source #

mkBinder_ :: Name -> Binder Source #

mkBinder :: a -> Binder' a Source #

data LamBinding Source #

A lambda binding is either domain free or typed.

Constructors

DomainFree TacticAttribute (NamedArg Binder) | . `x` or `{x}` or `.x` or `{x = y}` or `x@p` or `(p)`
DomainFull TypedBinding | . `(xs:e)` or `{xs:e}` or `(let Ds)`

#### Instances

Instances details

ExprLike LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m LamBinding Source # foldExpr :: FoldExprFn m LamBinding Source # traverseExpr :: TraverseExprFn m LamBinding Source # mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding Source #
LensHiding LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source #
HasRange LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LamBinding -> Range Source #
KillRange LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT LamBinding Source #
ToConcrete LamBinding Source # |

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LamBinding |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LamBinding = Maybe LamBinding

Methods

toConcrete :: MonadToConcrete m => LamBinding -> m (ConOfAbs LamBinding) Source #

bindToConcrete :: MonadToConcrete m => LamBinding -> (ConOfAbs LamBinding -> m b) -> m b Source #

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

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep LamBinding |

Instance details

Defined in Agda.Syntax.Abstract

type Rep LamBinding = D1 ('MetaData "LamBinding" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "DomainFree" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TacticAttribute) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg Binder))) :+: C1 ('MetaCons "DomainFull" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypedBinding)))

Methods

from :: LamBinding -> Rep LamBinding x Source #

to :: Rep LamBinding x -> LamBinding Source #

Show LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> LamBinding -> ShowS Source # show :: LamBinding -> String Source # showList :: [LamBinding] -> ShowS Source #
Eq LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: LamBinding -> LamBinding -> Bool Source # (/=) :: LamBinding -> LamBinding -> Bool Source #
type ConOfAbs LamBinding Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LamBinding = Maybe LamBinding
type Rep LamBinding Source # |

Instance details

Defined in Agda.Syntax.Abstract

type Rep LamBinding = D1 ('MetaData "LamBinding" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "DomainFree" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TacticAttribute) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg Binder))) :+: C1 ('MetaCons "DomainFull" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypedBinding)))

data TypedBinding Source #

A typed binding. Appears in dependent function spaces, typed lambdas, and telescopes. It might be tempting to simplify this to only bind a single name at a time, and translate, say, `(x y : A)` to `(x : A)(y : A)` before type-checking. However, this would be slightly problematic:

1. We would have to typecheck the type `A` several times.
2. If `A` contains a meta variable or hole, it would be duplicated by such a translation.

While 1. is only slightly inefficient, 2. would be an outright bug. Duplicating `A` could not be done naively, we would have to make sure that the metas of the copy are aliases of the metas of the original.

Constructors

TBind Range TypedBindingInfo (List1 (NamedArg Binder)) Type | As in telescope `(x y z : A)` or type `(x y z : A) -> B`.
TLet Range (List1 LetBinding) | E.g. `(let x = e)` or `(let open M)`.

#### Instances

Instances details

ExprLike TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m TypedBinding Source # foldExpr :: FoldExprFn m TypedBinding Source # traverseExpr :: TraverseExprFn m TypedBinding Source # mapExpr :: (Expr -> Expr) -> TypedBinding -> TypedBinding Source #
LensHiding TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getHiding :: TypedBinding -> Hiding Source # setHiding :: Hiding -> TypedBinding -> TypedBinding Source # mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding Source #
HasRange TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: TypedBinding -> Range Source #
KillRange TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT TypedBinding Source #
ToConcrete TypedBinding Source # |

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs TypedBinding |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs TypedBinding = Maybe TypedBinding

Methods

toConcrete :: MonadToConcrete m => TypedBinding -> m (ConOfAbs TypedBinding) Source #

bindToConcrete :: MonadToConcrete m => TypedBinding -> (ConOfAbs TypedBinding -> m b) -> m b Source #

PrettyTCM TypedBinding Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => TypedBinding -> m Doc Source #
NFData TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: TypedBinding -> () Source #
Generic TypedBinding Source # |

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep TypedBinding |

Instance details

Defined in Agda.Syntax.Abstract

type Rep TypedBinding = D1 ('MetaData "TypedBinding" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "TBind" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypedBindingInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (NamedArg Binder))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) :+: C1 ('MetaCons "TLet" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 LetBinding))))

Methods

from :: TypedBinding -> Rep TypedBinding x Source #

to :: Rep TypedBinding x -> TypedBinding Source #

Show TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> TypedBinding -> ShowS Source # show :: TypedBinding -> String Source # showList :: [TypedBinding] -> ShowS Source #
Eq TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: TypedBinding -> TypedBinding -> Bool Source # (/=) :: TypedBinding -> TypedBinding -> Bool Source #
type ConOfAbs TypedBinding Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs TypedBinding = Maybe TypedBinding
type Rep TypedBinding Source # |

Instance details

Defined in Agda.Syntax.Abstract

type Rep TypedBinding = D1 ('MetaData "TypedBinding" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "TBind" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypedBindingInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (NamedArg Binder))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) :+: C1 ('MetaCons "TLet" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 LetBinding))))

type Telescope1 = List1 TypedBinding Source #

mkLet :: ExprInfo -> [LetBinding] -> Expr -> Expr Source #

mkTLet :: Range -> [LetBinding] -> Maybe TypedBinding Source #

type RecordDirectives = RecordDirectives' RecordConName Source #

data ModuleApplication Source #

Constructors

SectionApp Telescope ModuleName [NamedArg Expr] | `tel. M args`: applies `M` to `args` and abstracts `tel`.

RecordModuleInstance ModuleName

    M {{...}}

#### Instances

Instances details

ExprLike ModuleApplication Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m ModuleApplication Source # foldExpr :: FoldExprFn m ModuleApplication Source # traverseExpr :: TraverseExprFn m ModuleApplication Source # mapExpr :: (Expr -> Expr) -> ModuleApplication -> ModuleApplication Source #
KillRange ModuleApplication Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT ModuleApplication Source #
ToConcrete ModuleApplication Source # |

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ModuleApplication |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs ModuleApplication = ModuleApplication

Methods

toConcrete :: MonadToConcrete m => ModuleApplication -> m (ConOfAbs ModuleApplication) Source #

bindToConcrete :: MonadToConcrete m => ModuleApplication -> (ConOfAbs ModuleApplication -> m b) -> m b Source #

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

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep ModuleApplication |

Instance details

Defined in Agda.Syntax.Abstract

type Rep ModuleApplication = D1 ('MetaData "ModuleApplication" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "SectionApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg Expr]))) :+: C1 ('MetaCons "RecordModuleInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName)))

Methods

from :: ModuleApplication -> Rep ModuleApplication x Source #

to :: Rep ModuleApplication x -> ModuleApplication Source #

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

Instance details

Defined in Agda.Syntax.Abstract

type Rep ModuleApplication = D1 ('MetaData "ModuleApplication" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "SectionApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg Expr]))) :+: C1 ('MetaCons "RecordModuleInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName)))

type TypeSignature = Declaration Source #

Only `Axiom`s.

type ImportDirective = ImportDirective' QName ModuleName Source #

type ImportedName = ImportedName' QName ModuleName Source #

type Renaming = Renaming' QName ModuleName Source #

type RewriteEqn = RewriteEqn' QName BindName Pattern Expr Source #

type WithExpr = WithExpr' Expr Source #

type LHSCore = LHSCore' Expr Source #

data RHS Source #

Constructors

RHS |

Fields

- rhsExpr :: Expr
- rhsConcrete :: Maybe Expr

  We store the original concrete expression in case we have to reproduce it during interactive case splitting. `Nothing` for internally generated rhss.

AbsurdRHS |
WithRHS QName (List1 WithExpr) (List1 Clause) | The `QName` is the name of the with function.
RewriteRHS |

Fields

- rewriteExprs :: [RewriteEqn]

  The `QName`s are the names of the generated with functions, one for each `Expr`.

- rewriteStrippedPats :: [ProblemEq]

  The patterns stripped by with-desugaring. These are only present if this rewrite follows a with.

- rewriteRHS :: RHS

  The RHS should not be another `RewriteRHS`.

- rewriteWhereDecls :: WhereDeclarations

  The where clauses are attached to the `RewriteRHS` by

#### Instances

Instances details

DeclaredNames RHS Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => RHS -> m Source #
ExprLike RHS Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m RHS Source # foldExpr :: FoldExprFn m RHS Source # traverseExpr :: TraverseExprFn m RHS Source # mapExpr :: (Expr -> Expr) -> RHS -> RHS Source #
HasRange RHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: RHS -> Range Source #
KillRange RHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT RHS Source #
ToConcrete RHS Source # |

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RHS |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs RHS = (RHS, [RewriteEqn], [WithExpr], [Declaration])

Methods

toConcrete :: MonadToConcrete m => RHS -> m (ConOfAbs RHS) Source #

bindToConcrete :: MonadToConcrete m => RHS -> (ConOfAbs RHS -> m b) -> m b Source #

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

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep RHS |

Instance details

Defined in Agda.Syntax.Abstract

type Rep RHS = D1 ('MetaData "RHS" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((C1 ('MetaCons "RHS" 'PrefixI 'True) (S1 ('MetaSel ('Just "rhsExpr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Just "rhsConcrete") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Expr))) :+: C1 ('MetaCons "AbsurdRHS" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "WithRHS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 WithExpr)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 Clause)))) :+: C1 ('MetaCons "RewriteRHS" 'PrefixI 'True) ((S1 ('MetaSel ('Just "rewriteExprs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [RewriteEqn]) :*: S1 ('MetaSel ('Just "rewriteStrippedPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ProblemEq])) :*: (S1 ('MetaSel ('Just "rewriteRHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RHS) :*: S1 ('MetaSel ('Just "rewriteWhereDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhereDeclarations)))))

Methods

from :: RHS -> Rep RHS x Source #

to :: Rep RHS x -> RHS Source #

Show RHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> RHS -> ShowS Source # show :: RHS -> String Source # showList :: [RHS] -> ShowS Source #
Eq RHS Source # | Ignore `rhsConcrete` when comparing `RHS`s.
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: RHS -> RHS -> Bool Source # (/=) :: RHS -> RHS -> Bool Source #
type ConOfAbs RHS Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs RHS = (RHS, [RewriteEqn], [WithExpr], [Declaration])
type Rep RHS Source # |

Instance details

Defined in Agda.Syntax.Abstract

type Rep RHS = D1 ('MetaData "RHS" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((C1 ('MetaCons "RHS" 'PrefixI 'True) (S1 ('MetaSel ('Just "rhsExpr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Just "rhsConcrete") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Expr))) :+: C1 ('MetaCons "AbsurdRHS" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "WithRHS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 WithExpr)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 Clause)))) :+: C1 ('MetaCons "RewriteRHS" 'PrefixI 'True) ((S1 ('MetaSel ('Just "rewriteExprs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [RewriteEqn]) :*: S1 ('MetaSel ('Just "rewriteStrippedPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ProblemEq])) :*: (S1 ('MetaSel ('Just "rewriteRHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RHS) :*: S1 ('MetaSel ('Just "rewriteWhereDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhereDeclarations)))))

type HoleContent = HoleContent' () BindName Pattern Expr Source #

data ScopeCopyInfo Source #

Constructors

ScopeCopyInfo |

Fields

- renModules :: Ren ModuleName
- renNames :: Ren QName

#### Instances

Instances details

Pretty ScopeCopyInfo Source # |
Instance details Defined in Agda.Syntax.Abstract Methods pretty :: ScopeCopyInfo -> Doc Source # prettyPrec :: Int -> ScopeCopyInfo -> Doc Source # prettyList :: [ScopeCopyInfo] -> Doc Source #
KillRange ScopeCopyInfo Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT ScopeCopyInfo Source #
NFData ScopeCopyInfo Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: ScopeCopyInfo -> () Source #
Generic ScopeCopyInfo Source # |

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep ScopeCopyInfo |

Instance details

Defined in Agda.Syntax.Abstract

type Rep ScopeCopyInfo = D1 ('MetaData "ScopeCopyInfo" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "ScopeCopyInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "renModules") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Ren ModuleName)) :*: S1 ('MetaSel ('Just "renNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Ren QName))))

Methods

from :: ScopeCopyInfo -> Rep ScopeCopyInfo x Source #

to :: Rep ScopeCopyInfo x -> ScopeCopyInfo Source #

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

Instance details

Defined in Agda.Syntax.Abstract

type Rep ScopeCopyInfo = D1 ('MetaData "ScopeCopyInfo" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "ScopeCopyInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "renModules") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Ren ModuleName)) :*: S1 ('MetaSel ('Just "renNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Ren QName))))

type Ren a = Map a (List1 a) Source #

Renaming (generic).

type PatternSynDefn = ([WithHiding Name], Pattern' Void) Source #

type PatternSynDefns = Map QName PatternSynDefn Source #

data ProblemEq Source #

A user pattern together with an internal term that it should be equal to after splitting is complete. Special cases: * User pattern is a variable but internal term isn't: this will be turned into an as pattern. * User pattern is a dot pattern: this pattern won't trigger any splitting but will be checked for equality after all splitting is complete and as patterns have been bound. * User pattern is an absurd pattern: emptiness of the type will be checked after splitting is complete. * User pattern is an annotated wildcard: type annotation will be checked after splitting is complete.

Constructors

ProblemEq |

Fields

- problemInPat :: Pattern
- problemInst :: Term
- problemType :: Dom Type

#### Instances

Instances details

KillRange ProblemEq Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT ProblemEq Source #
PrettyTCM ProblemEq Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => ProblemEq -> m Doc Source #
Subst ProblemEq Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

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

Methods

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

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

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep ProblemEq |

Instance details

Defined in Agda.Syntax.Abstract

type Rep ProblemEq = D1 ('MetaData "ProblemEq" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "ProblemEq" 'PrefixI 'True) (S1 ('MetaSel ('Just "problemInPat") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern) :*: (S1 ('MetaSel ('Just "problemInst") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :*: S1 ('MetaSel ('Just "problemType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Dom Type)))))

Methods

from :: ProblemEq -> Rep ProblemEq x Source #

to :: Rep ProblemEq x -> ProblemEq Source #

Show ProblemEq Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> ProblemEq -> ShowS Source # show :: ProblemEq -> String Source # showList :: [ProblemEq] -> ShowS Source #
Eq ProblemEq Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: ProblemEq -> ProblemEq -> Bool Source # (/=) :: ProblemEq -> ProblemEq -> Bool Source #
type SubstArg ProblemEq Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg ProblemEq = Term
type Rep ProblemEq Source # |

Instance details

Defined in Agda.Syntax.Abstract

type Rep ProblemEq = D1 ('MetaData "ProblemEq" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "ProblemEq" 'PrefixI 'True) (S1 ('MetaSel ('Just "problemInPat") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern) :*: (S1 ('MetaSel ('Just "problemInst") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :*: S1 ('MetaSel ('Just "problemType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Dom Type)))))

data TypedBindingInfo Source #

Extra information that is attached to a typed binding, that plays a role during type checking but strictly speaking is not part of the `name : type`" relation which a makes up a binding.

Constructors

TypedBindingInfo |

Fields

- tbTacticAttr :: TacticAttribute

  Does this binding have a tactic annotation?

- tbFinite :: Bool

  Does this binding correspond to a Partial binder, rather than to a Pi binder? Must be present here to be reflected into abstract syntax later (and to be printed to the user later).

#### Instances

Instances details

ExprLike TypedBindingInfo Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m TypedBindingInfo Source # foldExpr :: FoldExprFn m TypedBindingInfo Source # traverseExpr :: TraverseExprFn m TypedBindingInfo Source # mapExpr :: (Expr -> Expr) -> TypedBindingInfo -> TypedBindingInfo Source #
KillRange TypedBindingInfo Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT TypedBindingInfo Source #
Null TypedBindingInfo Source # |
Instance details Defined in Agda.Syntax.Abstract Methods empty :: TypedBindingInfo Source # null :: TypedBindingInfo -> Bool Source #
NFData TypedBindingInfo Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: TypedBindingInfo -> () Source #
Generic TypedBindingInfo Source # |

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep TypedBindingInfo |

Instance details

Defined in Agda.Syntax.Abstract

type Rep TypedBindingInfo = D1 ('MetaData "TypedBindingInfo" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "TypedBindingInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "tbTacticAttr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TacticAttribute) :*: S1 ('MetaSel ('Just "tbFinite") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))

Methods

from :: TypedBindingInfo -> Rep TypedBindingInfo x Source #

to :: Rep TypedBindingInfo x -> TypedBindingInfo Source #

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

Instance details

Defined in Agda.Syntax.Abstract

type Rep TypedBindingInfo = D1 ('MetaData "TypedBindingInfo" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "TypedBindingInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "tbTacticAttr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TacticAttribute) :*: S1 ('MetaSel ('Just "tbFinite") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))

type Args = [NamedArg Expr] Source #

type Field = TypeSignature Source #

type NAPs e = [NamedArg (Pattern' e)] Source #

data LHSCore' e Source #

The lhs in projection-application and with-pattern view. Parameterised over the type `e` of dot patterns.

Constructors

LHSHead | The head applied to ordinary patterns.

Fields

- lhsDefName :: QName

  Head `f`.

- lhsPats :: [NamedArg (Pattern' e)]

  Applied to patterns `ps`.

LHSProj | Projection.

Fields

- lhsDestructor :: AmbiguousQName

  Record projection identifier.

- lhsFocus :: NamedArg (LHSCore' e)

  Main argument of projection.

- lhsPats :: [NamedArg (Pattern' e)]

  Applied to patterns `ps`.

LHSWith | With patterns.

Fields

- lhsHead :: LHSCore' e

  E.g. the `LHSHead`.

- lhsWithPatterns :: List1 (Arg (Pattern' e))

  Applied to with patterns `| p1 | ... | pn`. These patterns are not prefixed with `WithP`!

- lhsPats :: [NamedArg (Pattern' e)]

  Applied to patterns `ps`.

#### Instances

Instances details

ToConcrete LHSCore Source # |

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHSCore |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LHSCore = Pattern

Methods

toConcrete :: MonadToConcrete m => LHSCore -> m (ConOfAbs LHSCore) Source #

bindToConcrete :: MonadToConcrete m => LHSCore -> (ConOfAbs LHSCore -> m b) -> m b Source #

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

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

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

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

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

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

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

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

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

null :: LHSCore' a -> Bool Source #

length :: LHSCore' a -> Int Source #

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

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

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

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

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

Traversable LHSCore' Source # |
Instance details Defined in Agda.Syntax.Abstract Methods traverse :: Applicative f => (a -> f b) -> LHSCore' a -> f (LHSCore' b) Source # sequenceA :: Applicative f => LHSCore' (f a) -> f (LHSCore' a) Source # mapM :: Monad m => (a -> m b) -> LHSCore' a -> m (LHSCore' b) Source # sequence :: Monad m => LHSCore' (m a) -> m (LHSCore' a) Source #
ExprLike a => ExprLike (LHSCore' a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (LHSCore' a) Source # foldExpr :: FoldExprFn m (LHSCore' a) Source # traverseExpr :: TraverseExprFn m (LHSCore' a) Source # mapExpr :: (Expr -> Expr) -> LHSCore' a -> LHSCore' a Source #
HasRange (LHSCore' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LHSCore' e -> Range Source #
KillRange e => KillRange (LHSCore' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (LHSCore' e) Source #
ToAbstract (LHSCore' Expr) Source # |

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (LHSCore' Expr) |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (LHSCore' Expr) = LHSCore' Expr

Methods

toAbstract :: LHSCore' Expr -> ScopeM (AbsOfCon (LHSCore' Expr)) Source #

NFData e => NFData (LHSCore' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: LHSCore' e -> () Source #
Generic (LHSCore' e) Source # |

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep (LHSCore' e) |

Instance details

Defined in Agda.Syntax.Abstract

type Rep (LHSCore' e) = D1 ('MetaData "LHSCore'" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "LHSHead" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsDefName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "lhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' e)])) :+: (C1 ('MetaCons "LHSProj" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsDestructor") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :*: (S1 ('MetaSel ('Just "lhsFocus") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg (LHSCore' e))) :*: S1 ('MetaSel ('Just "lhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' e)]))) :+: C1 ('MetaCons "LHSWith" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsHead") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (LHSCore' e)) :*: (S1 ('MetaSel ('Just "lhsWithPatterns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (Arg (Pattern' e)))) :*: S1 ('MetaSel ('Just "lhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' e)])))))

Methods

from :: LHSCore' e -> Rep (LHSCore' e) x Source #

to :: Rep (LHSCore' e) x -> LHSCore' e Source #

Show e => Show (LHSCore' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> LHSCore' e -> ShowS Source # show :: LHSCore' e -> String Source # showList :: [LHSCore' e] -> ShowS Source #
Eq e => Eq (LHSCore' e) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: LHSCore' e -> LHSCore' e -> Bool Source # (/=) :: LHSCore' e -> LHSCore' e -> Bool Source #
type ConOfAbs LHSCore Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LHSCore = Pattern
type AbsOfCon (LHSCore' Expr) Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (LHSCore' Expr) = LHSCore' Expr
type Rep (LHSCore' e) Source # |

Instance details

Defined in Agda.Syntax.Abstract

type Rep (LHSCore' e) = D1 ('MetaData "LHSCore'" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "LHSHead" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsDefName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "lhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' e)])) :+: (C1 ('MetaCons "LHSProj" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsDestructor") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :*: (S1 ('MetaSel ('Just "lhsFocus") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg (LHSCore' e))) :*: S1 ('MetaSel ('Just "lhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' e)]))) :+: C1 ('MetaCons "LHSWith" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsHead") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (LHSCore' e)) :*: (S1 ('MetaSel ('Just "lhsWithPatterns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (Arg (Pattern' e)))) :*: S1 ('MetaSel ('Just "lhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' e)])))))

type DefInfo = DefInfo' Expr Source #

newtype BindName Source #

A name in a binding position: we also compare the nameConcrete when comparing the binders for equality.

With `--caching` on we compare abstract syntax to determine if we can reuse previous typechecking results: during that comparison two names can have the same nameId but be semantically different, e.g. in `{_ : A} -> ..` vs. `{r : A} -> ..`.

Constructors

BindName |

Fields

- unBind :: Name

#### Instances

Instances details

ExprLike BindName Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m BindName Source # foldExpr :: FoldExprFn m BindName Source # traverseExpr :: TraverseExprFn m BindName Source # mapExpr :: (Expr -> Expr) -> BindName -> BindName Source #
HasRange BindName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: BindName -> Range Source #
KillRange BindName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT BindName Source #
SetRange BindName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods setRange :: Range -> BindName -> BindName Source #
ToConcrete BindName Source # |

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs BindName |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs BindName = BoundName

Methods

toConcrete :: MonadToConcrete m => BindName -> m (ConOfAbs BindName) Source #

bindToConcrete :: MonadToConcrete m => BindName -> (ConOfAbs BindName -> m b) -> m b Source #

EmbPrj BindName Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: BindName -> S Word32 Source # icod_ :: BindName -> S Word32 Source # value :: Word32 -> R BindName Source #
NFData BindName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: BindName -> () Source #
Show BindName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> BindName -> ShowS Source # show :: BindName -> String Source # showList :: [BindName] -> ShowS Source #
Eq BindName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: BindName -> BindName -> Bool Source # (/=) :: BindName -> BindName -> Bool Source #
Ord BindName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods compare :: BindName -> BindName -> Ordering Source # (<) :: BindName -> BindName -> Bool Source # (<=) :: BindName -> BindName -> Bool Source # (>) :: BindName -> BindName -> Bool Source # (>=) :: BindName -> BindName -> Bool Source # max :: BindName -> BindName -> BindName Source # min :: BindName -> BindName -> BindName Source #
(ToConcrete p, ToConcrete a) => ToConcrete (RewriteEqn' qn BindName p a) Source # |

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (RewriteEqn' qn BindName p a) |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (RewriteEqn' qn BindName p a) = RewriteEqn' () Name (ConOfAbs p) (ConOfAbs a)

Methods

toConcrete :: MonadToConcrete m => RewriteEqn' qn BindName p a -> m (ConOfAbs (RewriteEqn' qn BindName p a)) Source #

bindToConcrete :: MonadToConcrete m => RewriteEqn' qn BindName p a -> (ConOfAbs (RewriteEqn' qn BindName p a) -> m b) -> m b Source #

ToAbstract (RewriteEqn' () BindName Pattern Expr) Source # |

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (RewriteEqn' () BindName Pattern Expr) |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqn

Methods

toAbstract :: RewriteEqn' () BindName Pattern Expr -> ScopeM (AbsOfCon (RewriteEqn' () BindName Pattern Expr)) Source #

type ConOfAbs BindName Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs BindName = BoundName
type ConOfAbs (RewriteEqn' qn BindName p a) Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (RewriteEqn' qn BindName p a) = RewriteEqn' () Name (ConOfAbs p) (ConOfAbs a)
type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqn

mkBindName :: Name -> BindName Source #

data LetBinding Source #

Bindings that are valid in a `let`.

Constructors

LetBind LetInfo ArgInfo BindName Type Expr

    LetBind info rel name type defn

LetAxiom LetInfo ArgInfo BindName Type | Function declarations in a let with no matching body.
LetPatBind LetInfo Pattern Expr | Irrefutable pattern binding.
LetApply ModuleInfo Erased ModuleName ModuleApplication ScopeCopyInfo ImportDirective | `LetApply mi newM (oldM args) renamings dir`. The `ImportDirective` is for highlighting purposes.
LetOpen ModuleInfo ModuleName ImportDirective | only for highlighting and abstractToConcrete

#### Instances

Instances details

ExprLike LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m LetBinding Source # foldExpr :: FoldExprFn m LetBinding Source # traverseExpr :: TraverseExprFn m LetBinding Source # mapExpr :: (Expr -> Expr) -> LetBinding -> LetBinding Source #
HasRange LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LetBinding -> Range Source #
KillRange LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT LetBinding Source #
ToConcrete LetBinding Source # |

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LetBinding |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LetBinding = [Declaration]

Methods

toConcrete :: MonadToConcrete m => LetBinding -> m (ConOfAbs LetBinding) Source #

bindToConcrete :: MonadToConcrete m => LetBinding -> (ConOfAbs LetBinding -> m b) -> m b Source #

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

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep LetBinding |

Instance details

Defined in Agda.Syntax.Abstract

type Rep LetBinding = D1 ('MetaData "LetBinding" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((C1 ('MetaCons "LetBind" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LetInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: C1 ('MetaCons "LetAxiom" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LetInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))) :+: (C1 ('MetaCons "LetPatBind" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LetInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: (C1 ('MetaCons "LetApply" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleApplication) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeCopyInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective)))) :+: C1 ('MetaCons "LetOpen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))))))

Methods

from :: LetBinding -> Rep LetBinding x Source #

to :: Rep LetBinding x -> LetBinding Source #

Show LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> LetBinding -> ShowS Source # show :: LetBinding -> String Source # showList :: [LetBinding] -> ShowS Source #
Eq LetBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: LetBinding -> LetBinding -> Bool Source # (/=) :: LetBinding -> LetBinding -> Bool Source #
type ConOfAbs LetBinding Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LetBinding = [Declaration]
type Rep LetBinding Source # |

Instance details

Defined in Agda.Syntax.Abstract

type Rep LetBinding = D1 ('MetaData "LetBinding" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((C1 ('MetaCons "LetBind" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LetInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: C1 ('MetaCons "LetAxiom" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LetInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))) :+: (C1 ('MetaCons "LetPatBind" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LetInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: (C1 ('MetaCons "LetApply" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleApplication) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeCopyInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective)))) :+: C1 ('MetaCons "LetOpen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))))))

type RecordAssigns = [RecordAssign] Source #

type Assigns = [Assign] Source #

generalized :: Set QName -> Type -> Type Source #

Smart constructor for `Generalized`.

type RecordAssign = Either Assign ModuleName Source #

initCopyInfo :: ScopeCopyInfo Source #

data RecordConName Source #

How did we get our hands on the `QName` for the constructor of this record?

Constructors

NamedRecCon | The user wrote it.

Fields

- recordConName :: !QName

FreshRecCon | We made it up.

Fields

- recordConName :: !QName

#### Instances

Instances details

DeclaredNames RecordDirectives Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => RecordDirectives -> m Source #
KillRange RecordConName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT RecordConName Source #
ToConcrete RecordDirectives Source # |

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RecordDirectives |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs RecordDirectives = [RecordDirective]

Methods

toConcrete :: MonadToConcrete m => RecordDirectives -> m (ConOfAbs RecordDirectives) Source #

bindToConcrete :: MonadToConcrete m => RecordDirectives -> (ConOfAbs RecordDirectives -> m b) -> m b Source #

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

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep RecordConName |

Instance details

Defined in Agda.Syntax.Abstract

type Rep RecordConName = D1 ('MetaData "RecordConName" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "NamedRecCon" 'PrefixI 'True) (S1 ('MetaSel ('Just "recordConName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 QName)) :+: C1 ('MetaCons "FreshRecCon" 'PrefixI 'True) (S1 ('MetaSel ('Just "recordConName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 QName)))

Methods

from :: RecordConName -> Rep RecordConName x Source #

to :: Rep RecordConName x -> RecordConName Source #

Show RecordConName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> RecordConName -> ShowS Source # show :: RecordConName -> String Source # showList :: [RecordConName] -> ShowS Source #
Eq RecordConName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: RecordConName -> RecordConName -> Bool Source # (/=) :: RecordConName -> RecordConName -> Bool Source #
type ConOfAbs RecordDirectives Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs RecordDirectives = [RecordDirective]
type Rep RecordConName Source # |

Instance details

Defined in Agda.Syntax.Abstract

type Rep RecordConName = D1 ('MetaData "RecordConName" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "NamedRecCon" 'PrefixI 'True) (S1 ('MetaSel ('Just "recordConName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 QName)) :+: C1 ('MetaCons "FreshRecCon" 'PrefixI 'True) (S1 ('MetaSel ('Just "recordConName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 QName)))

data GeneralizeTelescope Source #

Constructors

GeneralizeTel |

Fields

- generalizeTelVars :: Map QName Name

  Maps generalize variables to the corresponding bound variable (to be introduced by the generalisation).

- generalizeTel :: Telescope

#### Instances

Instances details

ExprLike GeneralizeTelescope Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m GeneralizeTelescope Source # foldExpr :: FoldExprFn m GeneralizeTelescope Source # traverseExpr :: TraverseExprFn m GeneralizeTelescope Source # mapExpr :: (Expr -> Expr) -> GeneralizeTelescope -> GeneralizeTelescope Source #
KillRange GeneralizeTelescope Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT GeneralizeTelescope Source #
NFData GeneralizeTelescope Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: GeneralizeTelescope -> () Source #
Generic GeneralizeTelescope Source # |

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep GeneralizeTelescope |

Instance details

Defined in Agda.Syntax.Abstract

type Rep GeneralizeTelescope = D1 ('MetaData "GeneralizeTelescope" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "GeneralizeTel" 'PrefixI 'True) (S1 ('MetaSel ('Just "generalizeTelVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map QName Name)) :*: S1 ('MetaSel ('Just "generalizeTel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope)))

Methods

from :: GeneralizeTelescope -> Rep GeneralizeTelescope x Source #

to :: Rep GeneralizeTelescope x -> GeneralizeTelescope Source #

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

Instance details

Defined in Agda.Syntax.Abstract

type Rep GeneralizeTelescope = D1 ('MetaData "GeneralizeTelescope" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "GeneralizeTel" 'PrefixI 'True) (S1 ('MetaSel ('Just "generalizeTelVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map QName Name)) :*: S1 ('MetaSel ('Just "generalizeTel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope)))

data DataDefParams Source #

Constructors

DataDefParams |

Fields

- dataDefGeneralizedParams :: Set Name

  We don't yet know the position of generalized parameters from the data sig, so we keep these in a set on the side.

- dataDefParams :: [LamBinding]

#### Instances

Instances details

ExprLike DataDefParams Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m DataDefParams Source # foldExpr :: FoldExprFn m DataDefParams Source # traverseExpr :: TraverseExprFn m DataDefParams Source # mapExpr :: (Expr -> Expr) -> DataDefParams -> DataDefParams Source #
KillRange DataDefParams Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT DataDefParams Source #
NFData DataDefParams Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: DataDefParams -> () Source #
Generic DataDefParams Source # |

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep DataDefParams |

Instance details

Defined in Agda.Syntax.Abstract

type Rep DataDefParams = D1 ('MetaData "DataDefParams" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "DataDefParams" 'PrefixI 'True) (S1 ('MetaSel ('Just "dataDefGeneralizedParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Name)) :*: S1 ('MetaSel ('Just "dataDefParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LamBinding])))

Methods

from :: DataDefParams -> Rep DataDefParams x Source #

to :: Rep DataDefParams x -> DataDefParams Source #

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

Instance details

Defined in Agda.Syntax.Abstract

type Rep DataDefParams = D1 ('MetaData "DataDefParams" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "DataDefParams" 'PrefixI 'True) (S1 ('MetaSel ('Just "dataDefGeneralizedParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Name)) :*: S1 ('MetaSel ('Just "dataDefParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LamBinding])))

insertedBinder :: a -> Binder' a Source #

insertedBinder_ :: Name -> Binder Source #

extractPattern :: Binder' a -> Maybe (Pattern, a) Source #

mkDomainFree :: NamedArg Binder -> LamBinding Source #

mkTBind :: Range -> List1 (NamedArg Binder) -> Type -> TypedBinding Source #

mkPi :: ExprInfo -> Telescope -> Type -> Type Source #

noDataDefParams :: DataDefParams Source #

data WhereDeclarations Source #

Constructors

WhereDecls |

Fields

- whereModule :: Maybe ModuleName
- whereAnywhere :: Bool

  is it an ordinary unnamed `where`?

- whereDecls :: Maybe Declaration

  The declaration is a `Section`.

#### Instances

Instances details

DeclaredNames WhereDeclarations Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => WhereDeclarations -> m Source #
ExprLike WhereDeclarations Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m WhereDeclarations Source # foldExpr :: FoldExprFn m WhereDeclarations Source # traverseExpr :: TraverseExprFn m WhereDeclarations Source # mapExpr :: (Expr -> Expr) -> WhereDeclarations -> WhereDeclarations Source #
HasRange WhereDeclarations Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: WhereDeclarations -> Range Source #
KillRange WhereDeclarations Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT WhereDeclarations Source #
ToConcrete WhereDeclarations Source # |

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs WhereDeclarations |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs WhereDeclarations = WhereClause

Methods

toConcrete :: MonadToConcrete m => WhereDeclarations -> m (ConOfAbs WhereDeclarations) Source #

bindToConcrete :: MonadToConcrete m => WhereDeclarations -> (ConOfAbs WhereDeclarations -> m b) -> m b Source #

Null WhereDeclarations Source # |
Instance details Defined in Agda.Syntax.Abstract Methods empty :: WhereDeclarations Source # null :: WhereDeclarations -> Bool Source #
NFData WhereDeclarations Source # |
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: WhereDeclarations -> () Source #
Generic WhereDeclarations Source # |

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep WhereDeclarations |

Instance details

Defined in Agda.Syntax.Abstract

type Rep WhereDeclarations = D1 ('MetaData "WhereDeclarations" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "WhereDecls" 'PrefixI 'True) (S1 ('MetaSel ('Just "whereModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModuleName)) :*: (S1 ('MetaSel ('Just "whereAnywhere") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "whereDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Declaration)))))

Methods

from :: WhereDeclarations -> Rep WhereDeclarations x Source #

to :: Rep WhereDeclarations x -> WhereDeclarations Source #

Show WhereDeclarations Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> WhereDeclarations -> ShowS Source # show :: WhereDeclarations -> String Source # showList :: [WhereDeclarations] -> ShowS Source #
Eq WhereDeclarations Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: WhereDeclarations -> WhereDeclarations -> Bool Source # (/=) :: WhereDeclarations -> WhereDeclarations -> Bool Source #
type ConOfAbs WhereDeclarations Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs WhereDeclarations = WhereClause
type Rep WhereDeclarations Source # |

Instance details

Defined in Agda.Syntax.Abstract

type Rep WhereDeclarations = D1 ('MetaData "WhereDeclarations" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "WhereDecls" 'PrefixI 'True) (S1 ('MetaSel ('Just "whereModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModuleName)) :*: (S1 ('MetaSel ('Just "whereAnywhere") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "whereDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Declaration)))))

noWhereDecls :: WhereDeclarations Source #

type SpineClause = Clause' SpineLHS Source #

data SpineLHS Source #

The lhs of a clause in spine view (inside-out). Projection patterns are contained in `spLhsPats`, represented as `ProjP d`.

Constructors

SpineLHS |

Fields

- spLhsInfo :: LHSInfo

  Range.

- spLhsDefName :: QName

  Name of function we are defining.

- spLhsPats :: [NamedArg Pattern]

  Elimination by pattern, projections, with-patterns.

#### Instances

Instances details

ExprLike SpineLHS Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m SpineLHS Source # foldExpr :: FoldExprFn m SpineLHS Source # traverseExpr :: TraverseExprFn m SpineLHS Source # mapExpr :: (Expr -> Expr) -> SpineLHS -> SpineLHS Source #
HasRange SpineLHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: SpineLHS -> Range Source #
KillRange SpineLHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT SpineLHS Source #
ToConcrete SpineLHS Source # |

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs SpineLHS |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs SpineLHS = LHS

Methods

toConcrete :: MonadToConcrete m => SpineLHS -> m (ConOfAbs SpineLHS) Source #

bindToConcrete :: MonadToConcrete m => SpineLHS -> (ConOfAbs SpineLHS -> m b) -> m b Source #

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

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep SpineLHS |

Instance details

Defined in Agda.Syntax.Abstract

type Rep SpineLHS = D1 ('MetaData "SpineLHS" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "SpineLHS" 'PrefixI 'True) (S1 ('MetaSel ('Just "spLhsInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSInfo) :*: (S1 ('MetaSel ('Just "spLhsDefName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "spLhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg Pattern]))))

Methods

from :: SpineLHS -> Rep SpineLHS x Source #

to :: Rep SpineLHS x -> SpineLHS Source #

Show SpineLHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> SpineLHS -> ShowS Source # show :: SpineLHS -> String Source # showList :: [SpineLHS] -> ShowS Source #
Eq SpineLHS Source # |
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: SpineLHS -> SpineLHS -> Bool Source # (/=) :: SpineLHS -> SpineLHS -> Bool Source #
LHSToSpine Clause SpineClause Source # | Clause instance.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: Clause -> SpineClause Source # spineToLhs :: SpineClause -> Clause Source #
LHSToSpine LHS SpineLHS Source # | LHS instance.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: LHS -> SpineLHS Source # spineToLhs :: SpineLHS -> LHS Source #
type ConOfAbs SpineLHS Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs SpineLHS = LHS
type Rep SpineLHS Source # |

Instance details

Defined in Agda.Syntax.Abstract

type Rep SpineLHS = D1 ('MetaData "SpineLHS" "Agda.Syntax.Abstract" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "SpineLHS" 'PrefixI 'True) (S1 ('MetaSel ('Just "spLhsInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSInfo) :*: (S1 ('MetaSel ('Just "spLhsDefName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "spLhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg Pattern]))))

type WithExpr' e = Named BindName (Arg e) Source #

type NAPs1 e = List1 (NamedArg (Pattern' e)) Source #

type Patterns = [NamedArg Pattern] Source #

axiomName :: Declaration -> QName Source #

The name defined by the given axiom.

Precondition: The declaration has to be a (scoped) `Axiom`.

class AnyAbstract a where Source #

Are we in an abstract block?

In that case some definition is abstract.

Methods

anyAbstract :: a -> Bool Source #

#### Instances

Instances details

AnyAbstract Declaration Source # |
Instance details Defined in Agda.Syntax.Abstract Methods anyAbstract :: Declaration -> Bool Source #
AnyAbstract a => AnyAbstract [a] Source # |
Instance details Defined in Agda.Syntax.Abstract Methods anyAbstract :: [a] -> Bool Source #

class NameToExpr a where Source #

Turn a name into an expression.

Methods

nameToExpr :: a -> Expr Source #

#### Instances

Instances details

NameToExpr AbstractName Source # | Turn an `AbstractName` into an expression.
Instance details Defined in Agda.Syntax.Abstract Methods nameToExpr :: AbstractName -> Expr Source #
NameToExpr ResolvedName Source # | Turn a `ResolvedName` into an expression. Assumes name is not `UnknownName`.
Instance details Defined in Agda.Syntax.Abstract Methods nameToExpr :: ResolvedName -> Expr Source #

lambdaLiftExpr :: [WithHiding Name] -> Expr -> Expr Source #

class SubstExpr a where Source #

Minimal complete definition

Nothing

Methods

substExpr :: [(Name, Expr)] -> a -> a Source #

default substExpr :: forall (t :: Type -> Type) b. (Functor t, SubstExpr b, t b ~ a) => [(Name, Expr)] -> a -> a Source #

#### Instances

Instances details

SubstExpr Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Expr -> Expr Source #
SubstExpr ModuleName Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> ModuleName -> ModuleName Source #
SubstExpr Name Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Name -> Name Source #
SubstExpr a => SubstExpr (Arg a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Arg a -> Arg a Source #
SubstExpr a => SubstExpr (FieldAssignment' a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> FieldAssignment' a -> FieldAssignment' a Source #
SubstExpr a => SubstExpr (List1 a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> List1 a -> List1 a Source #
SubstExpr a => SubstExpr (Maybe a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Maybe a -> Maybe a Source #
SubstExpr a => SubstExpr [a] Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> [a] -> [a] Source #
SubstExpr a => SubstExpr (Named name a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Named name a -> Named name a Source #
(SubstExpr a, SubstExpr b) => SubstExpr (Either a b) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Either a b -> Either a b Source #
(SubstExpr a, SubstExpr b) => SubstExpr (a, b) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> (a, b) -> (a, b) Source #

insertImplicitPatSynArgs Source #

Arguments

:: HasRange a |
=> (Hiding -> Range -> a) | Thing to insert (wildcard).
-> Range | Range of the whole pattern synonym expression/pattern.
-> [WithHiding Name] | The parameters of the pattern synonym (from its definition).
-> [NamedArg a] | The arguments it is used with.
-> Maybe ([(Name, a)], [WithHiding Name]) | Substitution and left-over parameters.

data DeclarationSpine Source #

Declaration spines. Used in debugging to make it easy to see where constructors such as `ScopedDecl` and `Mutual` are placed.

Constructors

AxiomS |
GeneralizeS |
FieldS |
PrimitiveS |
MutualS [DeclarationSpine] |
SectionS [DeclarationSpine] |
ApplyS |
ImportS |
PragmaS |
OpenS |
FunDefS [ClauseSpine] |
DataSigS |
DataDefS |
RecSigS |
RecDefS [DeclarationSpine] |
PatternSynDefS |
UnquoteDeclS |
UnquoteDefS |
UnquoteDataS |
ScopedDeclS [DeclarationSpine] |
UnfoldingDeclS |

#### Instances

Instances details

Show DeclarationSpine Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> DeclarationSpine -> ShowS Source # show :: DeclarationSpine -> String Source # showList :: [DeclarationSpine] -> ShowS Source #

data ClauseSpine Source #

Clause spines.

Constructors

ClauseS RHSSpine WhereDeclarationsSpine |

#### Instances

Instances details

Show ClauseSpine Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> ClauseSpine -> ShowS Source # show :: ClauseSpine -> String Source # showList :: [ClauseSpine] -> ShowS Source #

data RHSSpine Source #

Right-hand side spines.

Constructors

RHSS |
AbsurdRHSS |
WithRHSS (List1 ClauseSpine) |
RewriteRHSS RHSSpine WhereDeclarationsSpine |

#### Instances

Instances details

Show RHSSpine Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> RHSSpine -> ShowS Source # show :: RHSSpine -> String Source # showList :: [RHSSpine] -> ShowS Source #

data WhereDeclarationsSpine Source #

Spines corresponding to `WhereDeclarations` values.

Constructors

WhereDeclsS (Maybe DeclarationSpine) |

#### Instances

Instances details

Show WhereDeclarationsSpine Source # |
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> WhereDeclarationsSpine -> ShowS Source # show :: WhereDeclarationsSpine -> String Source # showList :: [WhereDeclarationsSpine] -> ShowS Source #

declarationSpine :: Declaration -> DeclarationSpine Source #

The declaration spine corresponding to a declaration.

clauseSpine :: Clause -> ClauseSpine Source #

The clause spine corresponding to a clause.

rhsSpine :: RHS -> RHSSpine Source #

The right-hand side spine corresponding to a right-hand side.

whereDeclarationsSpine :: WhereDeclarations -> WhereDeclarationsSpine Source #

The spine corresponding to a `WhereDeclarations` value.

module Agda.Syntax.Abstract.Name

# Orphan instances

KillRange Suffix Source # |
Instance details Methods killRange :: KillRangeT Suffix Source #