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

pattern Def :: QName -> Expr
app :: Expr -> [NamedArg Expr] -> Expr
axiomName :: Declaration -> QName
clauseSpine :: Clause -> ClauseSpine
declarationSpine :: Declaration -> DeclarationSpine
extractPattern :: Binder' a -> Maybe (Pattern, a)
generalized :: Set QName -> Type -> Type
initCopyInfo :: ScopeCopyInfo
insertImplicitPatSynArgs :: HasRange a => (Hiding -> Range -> a) -> Range -> [WithHiding Name] -> [NamedArg a] -> Maybe ([(Name, a)], [WithHiding Name])
insertedBinder :: a -> Binder' a
insertedBinder_ :: Name -> Binder
lambdaLiftExpr :: [WithHiding Name] -> Expr -> Expr
mkBindName :: Name -> BindName
mkBinder :: a -> Binder' a
mkBinder_ :: Name -> Binder
mkDomainFree :: NamedArg Binder -> LamBinding
mkLet :: ExprInfo -> [LetBinding] -> Expr -> Expr
mkPi :: ExprInfo -> Telescope -> Type -> Type
mkTBind :: Range -> List1 (NamedArg Binder) -> Type -> TypedBinding
mkTLet :: Range -> [LetBinding] -> Maybe TypedBinding
noDataDefParams :: DataDefParams
noWhereDecls :: WhereDeclarations
rhsSpine :: RHS -> RHSSpine
whereDeclarationsSpine :: WhereDeclarations -> WhereDeclarationsSpine
class AnyAbstract a where
- anyAbstract :: a -> Bool
type Args = [NamedArg Expr]
type Assign = FieldAssignment' Expr
type Assigns = [Assign]
newtype BindName = BindName {
- unBind :: Name
}
type Binder = Binder' BindName
data Binder' a = Binder {
- binderPattern :: Maybe Pattern
- binderNameOrigin :: BinderNameOrigin
- binderName :: a
}
type Clause = Clause' LHS
data Clause' lhs = Clause {
- clauseLHS :: lhs
- clauseStrippedPats :: [ProblemEq]
- clauseRHS :: RHS
- clauseWhereDecls :: WhereDeclarations
- clauseCatchall :: Catchall
}
data ClauseSpine = ClauseS RHSSpine WhereDeclarationsSpine
type Constructor = TypeSignature
data DataDefParams = DataDefParams {
- dataDefGeneralizedParams :: Set Name
- dataDefParams :: [LamBinding]
}
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]
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
type DefInfo = DefInfo' Expr
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 RecInfo RecordAssigns
- | RecUpdate RecInfo Expr Assigns
- | ScopedExpr ScopeInfo Expr
- | Quote ExprInfo
- | QuoteTerm ExprInfo
- | Unquote ExprInfo
- | DontCare Expr
type Field = TypeSignature
data GeneralizeTelescope = GeneralizeTel {
- generalizeTelVars :: Map QName Name
- generalizeTel :: Telescope
}
type HoleContent = HoleContent' () BindName Pattern Expr
type ImportDirective = ImportDirective' QName ModuleName
type ImportedName = ImportedName' QName ModuleName
data LHS = LHS {
- lhsInfo :: LHSInfo
- lhsCore :: LHSCore
}
type LHSCore = LHSCore' Expr
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)]
  }
data LamBinding
- = DomainFree TacticAttribute (NamedArg Binder)
- | DomainFull TypedBinding
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
data ModuleApplication
- = SectionApp Telescope ModuleName [NamedArg Expr]
- | RecordModuleInstance ModuleName
type NAPs e = [NamedArg (Pattern' e)]
type NAPs1 e = List1 (NamedArg (Pattern' e))
class NameToExpr a where
- nameToExpr :: a -> Expr
type Pattern = 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 ConPatInfo [FieldAssignment' (Pattern' e)]
- | EqualP PatInfo (List1 (e, e))
- | WithP PatInfo (Pattern' e)
type PatternSynDefn = ([WithHiding Name], Pattern' Void)
type PatternSynDefns = Map QName PatternSynDefn
type Patterns = [NamedArg Pattern]
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 ProblemEq = ProblemEq {
- problemInPat :: Pattern
- problemInst :: Term
- problemType :: Dom Type
}
data RHS
- = RHS {
  - rhsExpr :: Expr
  - rhsConcrete :: Maybe Expr
  }
- | AbsurdRHS
- | WithRHS QName (List1 WithExpr) (List1 Clause)
- | RewriteRHS {
  - rewriteExprs :: [RewriteEqn]
  - rewriteStrippedPats :: [ProblemEq]
  - rewriteRHS :: RHS
  - rewriteWhereDecls :: WhereDeclarations
  }
data RHSSpine
- = RHSS
- | AbsurdRHSS
- | WithRHSS (List1 ClauseSpine)
- | RewriteRHSS RHSSpine WhereDeclarationsSpine
type RecordAssign = Either Assign ModuleName
type RecordAssigns = [RecordAssign]
data RecordConName
- = NamedRecCon {
  - recordConName :: !QName
  }
- | FreshRecCon {
  - recordConName :: !QName
  }
type RecordDirectives = RecordDirectives' RecordConName
type Ren a = Map a (List1 a)
type Renaming = Renaming' QName ModuleName
type RewriteEqn = RewriteEqn' QName BindName Pattern Expr
data ScopeCopyInfo = ScopeCopyInfo {
- renModules :: Ren ModuleName
- renNames :: Ren QName
}
type SpineClause = Clause' SpineLHS
data SpineLHS = SpineLHS {
- spLhsInfo :: LHSInfo
- spLhsDefName :: QName
- spLhsPats :: [NamedArg Pattern]
}
class SubstExpr a where
- substExpr :: [(Name, Expr)] -> a -> a
type TacticAttribute = TacticAttribute' Expr
type Telescope = [TypedBinding]
type Telescope1 = List1 TypedBinding
type Type = Expr
type TypeSignature = Declaration
data TypedBinding
- = TBind Range TypedBindingInfo (List1 (NamedArg Binder)) Type
- | TLet Range (List1 LetBinding)
data TypedBindingInfo = TypedBindingInfo {
- tbTacticAttr :: TacticAttribute
- tbFinite :: Bool
}
data WhereDeclarations = WhereDecls {
- whereModule :: Maybe ModuleName
- whereAnywhere :: Bool
- whereDecls :: Maybe Declaration
}
data WhereDeclarationsSpine = WhereDeclsS (Maybe DeclarationSpine)
type WithExpr = WithExpr' Expr
type WithExpr' e = Named BindName (Arg e)
module Agda.Syntax.Abstract.Name

Documentation

pattern Def :: QName -> Expr Source #

Pattern synonym for regular Def.

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

axiomName :: Declaration -> QName Source #

The name defined by the given axiom.

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

clauseSpine :: Clause -> ClauseSpine Source #

The clause spine corresponding to a clause.

declarationSpine :: Declaration -> DeclarationSpine Source #

The declaration spine corresponding to a declaration.

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

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

Smart constructor for Generalized.

initCopyInfo :: ScopeCopyInfo 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.

insertedBinder :: a -> Binder' a Source #

insertedBinder_ :: Name -> Binder Source #

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

mkBindName :: Name -> BindName Source #

mkBinder :: a -> Binder' a Source #

mkBinder_ :: Name -> Binder Source #

mkDomainFree :: NamedArg Binder -> LamBinding Source #

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

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

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

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

noDataDefParams :: DataDefParams Source #

noWhereDecls :: WhereDeclarations Source #

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.

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 #

type Args = [NamedArg Expr] Source #

type Assign = FieldAssignment' Expr Source #

Record field assignment f = e.

type Assigns = [Assign] 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

Binder
Fields binderPattern :: Maybe Pattern binderNameOrigin :: BinderNameOrigin binderName :: a

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

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

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]

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

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

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

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 RecInfo RecordAssigns	Record construction.
RecUpdate RecInfo Expr Assigns	Record update.
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`.

GeneralizeTel
Fields generalizeTelVars :: Map QName Name Maps generalize variables to the corresponding bound variable (to be introduced by the generalisation). generalizeTel :: Telescope

LHS
Fields lhsInfo :: LHSInfo Range. lhsCore :: LHSCore Copatterns.

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`.

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)`

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

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

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 #

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 ConPatInfo [FieldAssignment' (Pattern' e)]
EqualP PatInfo (List1 (e, e))
WithP PatInfo (Pattern' e)	`\| p`, for with-patterns.

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

ProblemEq
Fields problemInPat :: Pattern problemInst :: Term problemType :: Dom Type

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

RHSS
AbsurdRHSS
WithRHSS (List1 ClauseSpine)
RewriteRHSS RHSSpine WhereDeclarationsSpine

Documentation

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Orphan instances

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

NamedRecCon	The user wrote it.
Fields recordConName :: !QName
FreshRecCon	We made it up.
Fields recordConName :: !QName

ScopeCopyInfo
Fields renModules :: Ren ModuleName renNames :: Ren QName

SpineLHS
Fields spLhsInfo :: LHSInfo Range. spLhsDefName :: QName Name of function we are defining. spLhsPats :: [NamedArg Pattern] Elimination by pattern, projections, with-patterns.

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 #

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)`.

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).

WhereDecls
Fields whereModule :: Maybe ModuleName whereAnywhere :: Bool is it an ordinary unnamed `where`? whereDecls :: Maybe Declaration The declaration is a `Section`.

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

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