Agda-2.6.4.2: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Abstract

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

Documentation

type Type = Expr Source #

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

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 [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 (Set 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 ExprInfo RecordAssigns

Record construction.

RecUpdate ExprInfo 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.

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

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

Underscore Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

ToConcrete Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Expr 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHSCore 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Pattern 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Reify Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Expr 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

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

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.6.4.2-inplace" '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 [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 (Set 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 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 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 #

to :: Rep Expr x -> Expr #

Show Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> Expr -> ShowS #

show :: Expr -> String #

showList :: [Expr] -> ShowS #

NFData Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: Expr -> () #

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 #

(/=) :: Expr -> Expr -> Bool #

ToConcrete (Maybe Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe Pattern) 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

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

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

ToAbstract (RewriteEqn' () BindName Pattern Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type ConOfAbs Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ReifiesTo Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type Rep Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep Expr = D1 ('MetaData "Expr" "Agda.Syntax.Abstract" "Agda-2.6.4.2-inplace" '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 [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 (Set 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 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 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 ConOfAbs (Maybe Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type AbsOfRef (Expr, Elim) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Expr, Elims) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Instances

Instances details
DeclaredNames Clause Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Foldable Clause' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

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

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

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

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

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

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

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

null :: Clause' a -> Bool #

length :: Clause' a -> Int #

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

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

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

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

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

Traversable Clause' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

traverse :: Applicative f => (a -> f b) -> Clause' a -> f (Clause' b) #

sequenceA :: Applicative f => Clause' (f a) -> f (Clause' a) #

mapM :: Monad m => (a -> m b) -> Clause' a -> m (Clause' b) #

sequence :: Monad m => Clause' (m a) -> m (Clause' a) #

Functor Clause' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

fmap :: (a -> b) -> Clause' a -> Clause' b #

(<$) :: a -> Clause' b -> Clause' a #

LHSToSpine Clause SpineClause Source #

Clause instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

ExprLike a => ExprLike (Clause' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

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

(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

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.6.4.2-inplace" '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 Bool)))))

Methods

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

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

Show lhs => Show (Clause' lhs) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> Clause' lhs -> ShowS #

show :: Clause' lhs -> String #

showList :: [Clause' lhs] -> ShowS #

NFData lhs => NFData (Clause' lhs) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: Clause' lhs -> () #

Eq lhs => Eq (Clause' lhs) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

(==) :: Clause' lhs -> Clause' lhs -> Bool #

(/=) :: Clause' lhs -> Clause' lhs -> Bool #

type ConOfAbs (Clause' a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep (Clause' lhs) Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep (Clause' lhs) = D1 ('MetaData "Clause'" "Agda.Syntax.Abstract" "Agda-2.6.4.2-inplace" '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 Bool)))))

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 RString 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 
InlinePragma Bool QName 
NotProjectionLikePragma QName 
DisplayPragma QName [NamedArg Pattern] Expr 

Instances

Instances details
DeclaredNames Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

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.6.4.2-inplace" '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 RString) :*: (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 "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 "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 #

to :: Rep Pragma x -> Pragma #

Show Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: Pragma -> () #

Eq Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

(==) :: Pragma -> Pragma -> Bool #

(/=) :: Pragma -> Pragma -> Bool #

type Rep Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep Pragma = D1 ('MetaData "Pragma" "Agda.Syntax.Abstract" "Agda-2.6.4.2-inplace" '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 RString) :*: (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 "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 "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 Declaration Source #

Constructors

Axiom KindOfName DefInfo ArgInfo (Maybe [Occurrence]) 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

First argument is 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 [Arg 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

DeclaredNames Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

HasRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete Declaration Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Declaration 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ShowHead Declaration Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Decl

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.6.4.2-inplace" '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 [Occurrence])) :*: (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 [Arg 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])))))))
Show Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: Declaration -> () #

Eq Declaration Source #

Does not compare ScopeInfo fields.

Instance details

Defined in Agda.Syntax.Abstract

ToConcrete (Constr Constructor) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs Declaration Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep Declaration = D1 ('MetaData "Declaration" "Agda.Syntax.Abstract" "Agda-2.6.4.2-inplace" '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 [Occurrence])) :*: (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 [Arg 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

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 PatInfo [FieldAssignment' (Pattern' e)] 
EqualP PatInfo [(e, e)] 
WithP PatInfo (Pattern' e)

| p, for with-patterns.

AnnP PatInfo e (Pattern' e)

Pattern with type annotation

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

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

Foldable Pattern' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

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

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

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

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

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

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

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

null :: Pattern' a -> Bool #

length :: Pattern' a -> Int #

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

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

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

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

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

Traversable Pattern' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

traverse :: Applicative f => (a -> f b) -> Pattern' a -> f (Pattern' b) #

sequenceA :: Applicative f => Pattern' (f a) -> f (Pattern' a) #

mapM :: Monad m => (a -> m b) -> Pattern' a -> m (Pattern' b) #

sequence :: Monad m => Pattern' (m a) -> m (Pattern' a) #

Functor Pattern' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

fmap :: (a -> b) -> Pattern' a -> Pattern' b #

(<$) :: a -> Pattern' b -> Pattern' a #

IsProjP (Pattern' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

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

SetRange (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

setRange :: Range -> Pattern' a -> Pattern' a Source #

ToConcrete (Maybe Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe Pattern) 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

ExpandPatternSynonyms (Pattern' e) Source # 
Instance details

Defined in Agda.TypeChecking.Patterns.Abstract

EmbPrj a => EmbPrj (Pattern' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

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.6.4.2-inplace" '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 PatInfo) :*: 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 [(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))) :+: C1 ('MetaCons "AnnP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 e) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' e))))))))

Methods

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

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

Show e => Show (Pattern' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> Pattern' e -> ShowS #

show :: Pattern' e -> String #

showList :: [Pattern' e] -> ShowS #

NFData e => NFData (Pattern' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: Pattern' e -> () #

Eq e => Eq (Pattern' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

(==) :: Pattern' e -> Pattern' e -> Bool #

(/=) :: Pattern' e -> Pattern' e -> Bool #

ToAbstract (RewriteEqn' () BindName Pattern Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type ConOfAbs Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ADotT (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

type ADotT (Pattern' a) = a
type ConOfAbs (Maybe Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type AbsOfCon (Pattern' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type Rep (Pattern' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep (Pattern' e) = D1 ('MetaData "Pattern'" "Agda.Syntax.Abstract" "Agda-2.6.4.2-inplace" '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 PatInfo) :*: 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 [(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))) :+: C1 ('MetaCons "AnnP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 e) :*: 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 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 LHSProjs.

Constructors

LHS 

Fields

Instances

Instances details
DeclaredNames Clause Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

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

ToConcrete LHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHS 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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.6.4.2-inplace" '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 #

to :: Rep LHS x -> LHS #

Show LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> LHS -> ShowS #

show :: LHS -> String #

showList :: [LHS] -> ShowS #

NFData LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: LHS -> () #

Eq LHS Source #

Ignore Range when comparing LHSs.

Instance details

Defined in Agda.Syntax.Abstract

Methods

(==) :: LHS -> LHS -> Bool #

(/=) :: LHS -> LHS -> Bool #

LHSToSpine Clause SpineClause Source #

Clause instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

LHSToSpine LHS SpineLHS Source #

LHS instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

type ConOfAbs LHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep LHS = D1 ('MetaData "LHS" "Agda.Syntax.Abstract" "Agda-2.6.4.2-inplace" 'False) (C1 ('MetaCons "LHS" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSInfo) :*: S1 ('MetaSel ('Just "lhsCore") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSCore)))

data Binder' a Source #

Constructors

Binder 

Instances

Instances details
Foldable Binder' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

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

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

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

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

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

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

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

null :: Binder' a -> Bool #

length :: Binder' a -> Int #

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

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

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

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

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

Traversable Binder' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

traverse :: Applicative f => (a -> f b) -> Binder' a -> f (Binder' b) #

sequenceA :: Applicative f => Binder' (f a) -> f (Binder' a) #

mapM :: Monad m => (a -> m b) -> Binder' a -> m (Binder' b) #

sequence :: Monad m => Binder' (m a) -> m (Binder' a) #

Functor Binder' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

fmap :: (a -> b) -> Binder' a -> Binder' b #

(<$) :: a -> Binder' b -> Binder' a #

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

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

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.6.4.2-inplace" 'False) (C1 ('MetaCons "Binder" 'PrefixI 'True) (S1 ('MetaSel ('Just "binderPattern") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Pattern)) :*: S1 ('MetaSel ('Just "binderName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

Methods

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

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

Show a => Show (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> Binder' a -> ShowS #

show :: Binder' a -> String #

showList :: [Binder' a] -> ShowS #

NFData a => NFData (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: Binder' a -> () #

Eq a => Eq (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

(==) :: Binder' a -> Binder' a -> Bool #

(/=) :: Binder' a -> Binder' a -> Bool #

type ConOfAbs (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

data LamBinding Source #

A lambda binding is either domain free or typed.

Constructors

DomainFree TacticAttr (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

LensHiding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LamBinding 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Generic LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Show LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: LamBinding -> () #

Eq LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

type ConOfAbs LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

LensHiding TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

PrettyTCM TypedBinding Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Generic TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Show TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: TypedBinding -> () #

Eq TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

type ConOfAbs TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

KillRange ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Generic ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

Show ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: ModuleApplication -> () #

Eq ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

type ConOfAbs ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

data RHS Source #

Constructors

RHS 

Fields

AbsurdRHS 
WithRHS QName [WithExpr] (List1 Clause)

The QName is the name of the with function.

RewriteRHS 

Fields

Instances

Instances details
DeclaredNames RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

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

ToConcrete RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RHS 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Generic RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

from :: RHS -> Rep RHS x #

to :: Rep RHS x -> RHS #

Show RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> RHS -> ShowS #

show :: RHS -> String #

showList :: [RHS] -> ShowS #

NFData RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: RHS -> () #

Eq RHS Source #

Ignore rhsConcrete when comparing RHSs.

Instance details

Defined in Agda.Syntax.Abstract

Methods

(==) :: RHS -> RHS -> Bool #

(/=) :: RHS -> RHS -> Bool #

type ConOfAbs RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

data ScopeCopyInfo Source #

Instances

Instances details
Pretty ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

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.6.4.2-inplace" '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))))
Show ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: ScopeCopyInfo -> () #

Eq ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep ScopeCopyInfo = D1 ('MetaData "ScopeCopyInfo" "Agda.Syntax.Abstract" "Agda-2.6.4.2-inplace" '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).

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.

Instances

Instances details
KillRange ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

PrettyTCM ProblemEq Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Subst ProblemEq Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg ProblemEq 
Instance details

Defined in Agda.TypeChecking.Substitute

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.6.4.2-inplace" '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)))))
Show ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: ProblemEq -> () #

Eq ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

type SubstArg ProblemEq Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type Rep ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep ProblemEq = D1 ('MetaData "ProblemEq" "Agda.Syntax.Abstract" "Agda-2.6.4.2-inplace" '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 :: TacticAttr

    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

KillRange TypedBindingInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

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.6.4.2-inplace" 'False) (C1 ('MetaCons "TypedBindingInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "tbTacticAttr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TacticAttr) :*: S1 ('MetaSel ('Just "tbFinite") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))
Show TypedBindingInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData TypedBindingInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: TypedBindingInfo -> () #

Eq TypedBindingInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep TypedBindingInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

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

LHSProj

Projection.

Fields

LHSWith

With patterns.

Fields

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

Foldable LHSCore' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

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

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

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

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

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

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

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

null :: LHSCore' a -> Bool #

length :: LHSCore' a -> Int #

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

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

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

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

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

Traversable LHSCore' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

traverse :: Applicative f => (a -> f b) -> LHSCore' a -> f (LHSCore' b) #

sequenceA :: Applicative f => LHSCore' (f a) -> f (LHSCore' a) #

mapM :: Monad m => (a -> m b) -> LHSCore' a -> m (LHSCore' b) #

sequence :: Monad m => LHSCore' (m a) -> m (LHSCore' a) #

Functor LHSCore' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

fmap :: (a -> b) -> LHSCore' a -> LHSCore' b #

(<$) :: a -> LHSCore' b -> LHSCore' a #

ExprLike a => ExprLike (LHSCore' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

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

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

Generic (LHSCore' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

Show e => Show (LHSCore' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> LHSCore' e -> ShowS #

show :: LHSCore' e -> String #

showList :: [LHSCore' e] -> ShowS #

NFData e => NFData (LHSCore' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: LHSCore' e -> () #

Eq e => Eq (LHSCore' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

(==) :: LHSCore' e -> LHSCore' e -> Bool #

(/=) :: LHSCore' e -> LHSCore' e -> Bool #

type ConOfAbs LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type AbsOfCon (LHSCore' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type Rep (LHSCore' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

type NAPs e = [NamedArg (Pattern' e)] 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

Instances

Instances details
ExprLike BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

HasRange BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

SetRange BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete BindName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs BindName 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

EmbPrj BindName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Show BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: BindName -> () #

Eq BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

Ord BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete (Maybe BindName) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe BindName) 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

(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

ToAbstract (RewriteEqn' () BindName Pattern Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type ConOfAbs BindName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Maybe BindName) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (RewriteEqn' qn BindName p a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data LetBinding Source #

Bindings that are valid in a let.

Constructors

LetBind LetInfo ArgInfo BindName Type Expr
LetBind info rel name type defn
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

LetDeclaredVariable BindName

Only used for highlighting. Refers to the first occurrence of x in let x : A; x = e.

Instances

Instances details
ExprLike LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

HasRange LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete LetBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LetBinding 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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.6.4.2-inplace" '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 "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))) :+: C1 ('MetaCons "LetDeclaredVariable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName)))))
Show LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: LetBinding -> () #

Eq LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

type ConOfAbs LetBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep LetBinding = D1 ('MetaData "LetBinding" "Agda.Syntax.Abstract" "Agda-2.6.4.2-inplace" '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 "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))) :+: C1 ('MetaCons "LetDeclaredVariable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName)))))

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

Smart constructor for Generalized.

data GeneralizeTelescope Source #

Constructors

GeneralizeTel 

Fields

Instances

Instances details
ExprLike GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

KillRange GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

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.6.4.2-inplace" '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)))
Show GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: GeneralizeTelescope -> () #

Eq GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep GeneralizeTelescope = D1 ('MetaData "GeneralizeTelescope" "Agda.Syntax.Abstract" "Agda-2.6.4.2-inplace" '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

Instances

Instances details
ExprLike DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

KillRange DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

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.6.4.2-inplace" '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])))
Show DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: DataDefParams -> () #

Eq DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep DataDefParams = D1 ('MetaData "DataDefParams" "Agda.Syntax.Abstract" "Agda-2.6.4.2-inplace" '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])))

data WhereDeclarations Source #

Constructors

WhereDecls 

Fields

Instances

Instances details
DeclaredNames WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

HasRange WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Null WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

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.6.4.2-inplace" '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)))))
Show WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: WhereDeclarations -> () #

Eq WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

type ConOfAbs WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep WhereDeclarations = D1 ('MetaData "WhereDeclarations" "Agda.Syntax.Abstract" "Agda-2.6.4.2-inplace" '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)))))

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

Instances

Instances details
ExprLike SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

HasRange SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs SpineLHS 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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.6.4.2-inplace" '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 #

to :: Rep SpineLHS x -> SpineLHS #

Show SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: SpineLHS -> () #

Eq SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

LHSToSpine Clause SpineClause Source #

Clause instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

LHSToSpine LHS SpineLHS Source #

LHS instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

type ConOfAbs SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep SpineLHS = D1 ('MetaData "SpineLHS" "Agda.Syntax.Abstract" "Agda-2.6.4.2-inplace" '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]))))

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

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

NameToExpr ResolvedName Source #

Turn a ResolvedName into an expression.

Assumes name is not UnknownName.

Instance details

Defined in Agda.Syntax.Abstract

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

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

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 :: HasRange a => (Range -> a) -> Range -> [Arg Name] -> [NamedArg a] -> Maybe ([(Name, a)], [Arg Name]) Source #

data ClauseSpine Source #

Clause spines.

Instances

Instances details
Show ClauseSpine Source # 
Instance details

Defined in Agda.Syntax.Abstract

data RHSSpine Source #

Right-hand side spines.

Instances

Instances details
Show RHSSpine Source # 
Instance details

Defined in Agda.Syntax.Abstract

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.

Orphan instances

KillRange Suffix Source # 
Instance details