Agda.Syntax.Abstract

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

Documentation

class SubstExpr a where

Minimal complete definition

Nothing

Methods

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

default substExpr :: (Functor t, SubstExpr b, t b ~ a) => [(Name, Expr)] -> a -> a

Instances

SubstExpr Name

Defined in Agda.Syntax.Abstract

Methods

substExpr :: [(Name0, Expr)] -> Name -> Name

SubstExpr ModuleName

Defined in Agda.Syntax.Abstract

Methods

substExpr :: [(Name, Expr)] -> ModuleName -> ModuleName

SubstExpr Expr

Defined in Agda.Syntax.Abstract

Methods

substExpr :: [(Name, Expr)] -> Expr -> Expr

SubstExpr a => SubstExpr [a]

Defined in Agda.Syntax.Abstract

Methods

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

SubstExpr a => SubstExpr (Maybe a)

Defined in Agda.Syntax.Abstract

Methods

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

SubstExpr a => SubstExpr (List1 a)

Defined in Agda.Syntax.Abstract

Methods

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

SubstExpr a => SubstExpr (Arg a)

Defined in Agda.Syntax.Abstract

Methods

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

SubstExpr a => SubstExpr (FieldAssignment' a)

Defined in Agda.Syntax.Abstract

Methods

substExpr :: [(Name, Expr)] -> FieldAssignment' a -> FieldAssignment' a

(SubstExpr a, SubstExpr b) => SubstExpr (Either a b)

Defined in Agda.Syntax.Abstract

Methods

substExpr :: [(Name, Expr)] -> Either a b -> Either a b

(SubstExpr a, SubstExpr b) => SubstExpr (a, b)

Defined in Agda.Syntax.Abstract

Methods

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

SubstExpr a => SubstExpr (Named name a)

Defined in Agda.Syntax.Abstract

Methods

substExpr :: [(Name, Expr)] -> Named name a -> Named name a

type PatternSynDefns = Map QName PatternSynDefn

type PatternSynDefn = ([Arg Name], Pattern' Void)

class NameToExpr a where

Turn a name into an expression.

Methods

nameToExpr :: a -> Expr

Instances

NameToExpr ResolvedName

Turn a ResolvedName into an expression.

Assumes name is not UnknownName.

Defined in Agda.Syntax.Abstract

Methods

nameToExpr :: ResolvedName -> Expr

NameToExpr AbstractName

Turn an AbstractName into an expression.

Defined in Agda.Syntax.Abstract

Methods

nameToExpr :: AbstractName -> Expr

class AnyAbstract a where

Are we in an abstract block?

In that case some definition is abstract.

Methods

anyAbstract :: a -> Bool

Instances

AnyAbstract Declaration

Defined in Agda.Syntax.Abstract

Methods

anyAbstract :: Declaration -> Bool

AnyAbstract a => AnyAbstract [a]

Defined in Agda.Syntax.Abstract

Methods

anyAbstract :: [a] -> Bool

type HoleContent = HoleContent' () BindName Pattern Expr

type Patterns = [NamedArg Pattern]

type Pattern = Pattern' Expr

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

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

data Pattern' e

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

Functor Pattern'

Defined in Agda.Syntax.Abstract

Methods

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

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

Foldable Pattern'

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'

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)

MapNamedArgPattern NAP

Defined in Agda.Syntax.Abstract.Pattern

Methods

mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP

ToConcrete Pattern

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Pattern

Methods

toConcrete :: Pattern -> AbsToCon (ConOfAbs Pattern)

bindToConcrete :: Pattern -> (ConOfAbs Pattern -> AbsToCon b) -> AbsToCon b

IsFlexiblePattern Pattern

Defined in Agda.TypeChecking.Rules.LHS

Methods

maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Pattern -> MaybeT m FlexibleVarKind

isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Pattern -> m Bool

Eq e => Eq (Pattern' e)

Defined in Agda.Syntax.Abstract

Methods

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

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

Data e => Data (Pattern' e)

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pattern' e -> c (Pattern' e)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Pattern' e)

toConstr :: Pattern' e -> Constr

dataTypeOf :: Pattern' e -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Pattern' e))

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (Pattern' e))

gmapT :: (forall b. Data b => b -> b) -> Pattern' e -> Pattern' e

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pattern' e -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pattern' e -> r

gmapQ :: (forall d. Data d => d -> u) -> Pattern' e -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Pattern' e -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pattern' e -> m (Pattern' e)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern' e -> m (Pattern' e)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern' e -> m (Pattern' e)

Show e => Show (Pattern' e)

Defined in Agda.Syntax.Abstract

Methods

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

show :: Pattern' e -> String

showList :: [Pattern' e] -> ShowS

Generic (Pattern' e)

Defined in Agda.Syntax.Abstract

Associated Types

type Rep (Pattern' e) :: Type -> Type

Methods

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

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

NFData e => NFData (Pattern' e)

Defined in Agda.Syntax.Abstract

Methods

rnf :: Pattern' e -> ()

KillRange e => KillRange (Pattern' e)

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT (Pattern' e)

SetRange (Pattern' a)

Defined in Agda.Syntax.Abstract

Methods

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

HasRange (Pattern' e)

Defined in Agda.Syntax.Abstract

Methods

getRange :: Pattern' e -> Range

IsProjP (Pattern' e)

Defined in Agda.Syntax.Abstract

Methods

isProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName)

IsWithP (Pattern' e)

Check for with-pattern.

Defined in Agda.Syntax.Abstract.Pattern

Methods

isWithP :: Pattern' e -> Maybe (Pattern' e)

ExprLike a => ExprLike (Pattern' a)

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m (Pattern' a)

foldExpr :: FoldExprFn m (Pattern' a)

traverseExpr :: TraverseExprFn m (Pattern' a)

mapExpr :: (Expr -> Expr) -> Pattern' a -> Pattern' a

APatternLike (Pattern' a)

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (Pattern' a)

Methods

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

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)

EmbPrj a => EmbPrj (Pattern' a)

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Pattern' a -> S Int32

icod_ :: Pattern' a -> S Int32

value :: Int32 -> R (Pattern' a)

NamesIn (Pattern' a)

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Pattern' a -> m

ToConcrete (Maybe Pattern)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe Pattern)

Methods

toConcrete :: Maybe Pattern -> AbsToCon (ConOfAbs (Maybe Pattern))

bindToConcrete :: Maybe Pattern -> (ConOfAbs (Maybe Pattern) -> AbsToCon b) -> AbsToCon b

ExpandPatternSynonyms (Pattern' e)

Defined in Agda.TypeChecking.Patterns.Abstract

Methods

expandPatternSynonyms :: Pattern' e -> TCM (Pattern' e)

ToAbstract (Pattern' Expr)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Pattern' Expr)

Methods

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

ToAbstract (RewriteEqn' () BindName Pattern Expr)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (RewriteEqn' () BindName Pattern Expr)

Methods

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

type ConOfAbs Pattern

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs Pattern = Pattern

type Rep (Pattern' e)

Defined in Agda.Syntax.Abstract

type Rep (Pattern' e) = D1 ('MetaData "Pattern'" "Agda.Syntax.Abstract" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" '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 ADotT (Pattern' a)

Defined in Agda.Syntax.Abstract.Pattern

type ADotT (Pattern' a) = a

type ConOfAbs (Maybe Pattern)

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Maybe Pattern) = Maybe Pattern

type AbsOfCon (Pattern' Expr)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (Pattern' Expr) = Pattern' Expr

type AbsOfCon (RewriteEqn' () BindName Pattern Expr)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqn

type LHSCore = LHSCore' Expr

data LHSCore' e

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

Constructors

LHSHead

The head applied to ordinary patterns.

Fields

• lhsDefName :: QName

  Head f.

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

  Applied to patterns ps.

LHSProj

Projection.

Fields

• lhsDestructor :: AmbiguousQName

  Record projection identifier.

• lhsFocus :: NamedArg (LHSCore' e)

  Main argument of projection.

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

  Applied to patterns ps.

LHSWith

With patterns.

Fields

• lhsHead :: LHSCore' e

  E.g. the LHSHead.

• lhsWithPatterns :: [Arg (Pattern' e)]

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

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

  Applied to patterns ps.

Instances

Functor LHSCore'

Defined in Agda.Syntax.Abstract

Methods

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

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

Foldable LHSCore'

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'

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)

ToConcrete LHSCore

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHSCore

Methods

toConcrete :: LHSCore -> AbsToCon (ConOfAbs LHSCore)

bindToConcrete :: LHSCore -> (ConOfAbs LHSCore -> AbsToCon b) -> AbsToCon b

Eq e => Eq (LHSCore' e)

Defined in Agda.Syntax.Abstract

Methods

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

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

Data e => Data (LHSCore' e)

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LHSCore' e -> c (LHSCore' e)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (LHSCore' e)

toConstr :: LHSCore' e -> Constr

dataTypeOf :: LHSCore' e -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (LHSCore' e))

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (LHSCore' e))

gmapT :: (forall b. Data b => b -> b) -> LHSCore' e -> LHSCore' e

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHSCore' e -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHSCore' e -> r

gmapQ :: (forall d. Data d => d -> u) -> LHSCore' e -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> LHSCore' e -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHSCore' e -> m (LHSCore' e)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSCore' e -> m (LHSCore' e)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSCore' e -> m (LHSCore' e)

Show e => Show (LHSCore' e)

Defined in Agda.Syntax.Abstract

Methods

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

show :: LHSCore' e -> String

showList :: [LHSCore' e] -> ShowS

Generic (LHSCore' e)

Defined in Agda.Syntax.Abstract

Associated Types

type Rep (LHSCore' e) :: Type -> Type

Methods

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

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

NFData e => NFData (LHSCore' e)

Defined in Agda.Syntax.Abstract

Methods

rnf :: LHSCore' e -> ()

KillRange e => KillRange (LHSCore' e)

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT (LHSCore' e)

HasRange (LHSCore' e)

Defined in Agda.Syntax.Abstract

Methods

getRange :: LHSCore' e -> Range

ExprLike a => ExprLike (LHSCore' a)

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m (LHSCore' a)

foldExpr :: FoldExprFn m (LHSCore' a)

traverseExpr :: TraverseExprFn m (LHSCore' a)

mapExpr :: (Expr -> Expr) -> LHSCore' a -> LHSCore' a

ToAbstract (LHSCore' Expr)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (LHSCore' Expr)

Methods

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

type ConOfAbs LHSCore

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs LHSCore = Pattern

type Rep (LHSCore' e)

Defined in Agda.Syntax.Abstract

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

type AbsOfCon (LHSCore' Expr)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (LHSCore' Expr) = LHSCore' Expr

data LHS

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

Constructors

LHS

Fields

• lhsInfo :: LHSInfo

  Range.

• lhsCore :: LHSCore

  Copatterns.

Instances

Eq LHS

Ignore Range when comparing LHSs.

Defined in Agda.Syntax.Abstract

Methods

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

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

Data LHS

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LHS -> c LHS

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LHS

toConstr :: LHS -> Constr

dataTypeOf :: LHS -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LHS)

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

gmapT :: (forall b. Data b => b -> b) -> LHS -> LHS

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHS -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHS -> r

gmapQ :: (forall d. Data d => d -> u) -> LHS -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> LHS -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHS -> m LHS

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHS -> m LHS

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHS -> m LHS

Show LHS

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> LHS -> ShowS

show :: LHS -> String

showList :: [LHS] -> ShowS

Generic LHS

Defined in Agda.Syntax.Abstract

Associated Types

type Rep LHS :: Type -> Type

Methods

from :: LHS -> Rep LHS x

to :: Rep LHS x -> LHS

NFData LHS

Defined in Agda.Syntax.Abstract

Methods

rnf :: LHS -> ()

KillRange LHS

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT LHS

HasRange LHS

Defined in Agda.Syntax.Abstract

Methods

getRange :: LHS -> Range

DeclaredNames Clause

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => Clause -> m

ExprLike LHS

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m LHS

foldExpr :: FoldExprFn m LHS

traverseExpr :: TraverseExprFn m LHS

mapExpr :: (Expr -> Expr) -> LHS -> LHS

ToConcrete LHS

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHS

Methods

toConcrete :: LHS -> AbsToCon (ConOfAbs LHS)

bindToConcrete :: LHS -> (ConOfAbs LHS -> AbsToCon b) -> AbsToCon b

LHSToSpine LHS SpineLHS

LHS instance.

Defined in Agda.Syntax.Abstract.Pattern

Methods

lhsToSpine :: LHS -> SpineLHS

spineToLhs :: SpineLHS -> LHS

LHSToSpine Clause SpineClause

Clause instance.

Defined in Agda.Syntax.Abstract.Pattern

Methods

lhsToSpine :: Clause -> SpineClause

spineToLhs :: SpineClause -> Clause

type Rep LHS

Defined in Agda.Syntax.Abstract

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

type ConOfAbs LHS

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs LHS = LHS

data SpineLHS

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

Constructors

SpineLHS

Fields

• spLhsInfo :: LHSInfo

  Range.

• spLhsDefName :: QName

  Name of function we are defining.

• spLhsPats :: [NamedArg Pattern]

  Elimination by pattern, projections, with-patterns.

Instances

Eq SpineLHS

Defined in Agda.Syntax.Abstract

Methods

(==) :: SpineLHS -> SpineLHS -> Bool

(/=) :: SpineLHS -> SpineLHS -> Bool

Data SpineLHS

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SpineLHS -> c SpineLHS

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SpineLHS

toConstr :: SpineLHS -> Constr

dataTypeOf :: SpineLHS -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SpineLHS)

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

gmapT :: (forall b. Data b => b -> b) -> SpineLHS -> SpineLHS

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SpineLHS -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SpineLHS -> r

gmapQ :: (forall d. Data d => d -> u) -> SpineLHS -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SpineLHS -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SpineLHS -> m SpineLHS

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SpineLHS -> m SpineLHS

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SpineLHS -> m SpineLHS

Show SpineLHS

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> SpineLHS -> ShowS

show :: SpineLHS -> String

showList :: [SpineLHS] -> ShowS

Generic SpineLHS

Defined in Agda.Syntax.Abstract

Associated Types

type Rep SpineLHS :: Type -> Type

Methods

from :: SpineLHS -> Rep SpineLHS x

to :: Rep SpineLHS x -> SpineLHS

NFData SpineLHS

Defined in Agda.Syntax.Abstract

Methods

rnf :: SpineLHS -> ()

KillRange SpineLHS

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT SpineLHS

HasRange SpineLHS

Defined in Agda.Syntax.Abstract

Methods

getRange :: SpineLHS -> Range

ExprLike SpineLHS

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m SpineLHS

foldExpr :: FoldExprFn m SpineLHS

traverseExpr :: TraverseExprFn m SpineLHS

mapExpr :: (Expr -> Expr) -> SpineLHS -> SpineLHS

ToConcrete SpineLHS

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs SpineLHS

Methods

toConcrete :: SpineLHS -> AbsToCon (ConOfAbs SpineLHS)

bindToConcrete :: SpineLHS -> (ConOfAbs SpineLHS -> AbsToCon b) -> AbsToCon b

LHSToSpine LHS SpineLHS

LHS instance.

Defined in Agda.Syntax.Abstract.Pattern

Methods

lhsToSpine :: LHS -> SpineLHS

spineToLhs :: SpineLHS -> LHS

LHSToSpine Clause SpineClause

Clause instance.

Defined in Agda.Syntax.Abstract.Pattern

Methods

lhsToSpine :: Clause -> SpineClause

spineToLhs :: SpineClause -> Clause

type Rep SpineLHS

Defined in Agda.Syntax.Abstract

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

type ConOfAbs SpineLHS

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs SpineLHS = LHS

data RHS

Constructors

RHS

Fields

• rhsExpr :: Expr
• rhsConcrete :: Maybe Expr

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

AbsurdRHS

WithRHS QName [WithExpr] [Clause]

The QName is the name of the with function.

RewriteRHS

Fields

• rewriteExprs :: [RewriteEqn]

  The QNames are the names of the generated with functions, one for each Expr.

• rewriteStrippedPats :: [ProblemEq]

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

• rewriteRHS :: RHS

  The RHS should not be another RewriteRHS.

• rewriteWhereDecls :: WhereDeclarations

  The where clauses are attached to the RewriteRHS by

Instances

Eq RHS

Ignore rhsConcrete when comparing RHSs.

Defined in Agda.Syntax.Abstract

Methods

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

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

Data RHS

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RHS -> c RHS

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RHS

toConstr :: RHS -> Constr

dataTypeOf :: RHS -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RHS)

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

gmapT :: (forall b. Data b => b -> b) -> RHS -> RHS

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RHS -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RHS -> r

gmapQ :: (forall d. Data d => d -> u) -> RHS -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> RHS -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RHS -> m RHS

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RHS -> m RHS

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RHS -> m RHS

Show RHS

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> RHS -> ShowS

show :: RHS -> String

showList :: [RHS] -> ShowS

Generic RHS

Defined in Agda.Syntax.Abstract

Associated Types

type Rep RHS :: Type -> Type

Methods

from :: RHS -> Rep RHS x

to :: Rep RHS x -> RHS

NFData RHS

Defined in Agda.Syntax.Abstract

Methods

rnf :: RHS -> ()

KillRange RHS

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT RHS

HasRange RHS

Defined in Agda.Syntax.Abstract

Methods

getRange :: RHS -> Range

DeclaredNames RHS

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => RHS -> m

ExprLike RHS

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m RHS

foldExpr :: FoldExprFn m RHS

traverseExpr :: TraverseExprFn m RHS

mapExpr :: (Expr -> Expr) -> RHS -> RHS

ToConcrete RHS

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RHS

Methods

toConcrete :: RHS -> AbsToCon (ConOfAbs RHS)

bindToConcrete :: RHS -> (ConOfAbs RHS -> AbsToCon b) -> AbsToCon b

type Rep RHS

Defined in Agda.Syntax.Abstract

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

type ConOfAbs RHS

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs RHS = (RHS, [RewriteEqn], [WithExpr], [Declaration])

type WithExpr = WithExpr' Expr

type WithExpr' e = Named BindName (Arg e)

type RewriteEqn = RewriteEqn' QName BindName Pattern Expr

type SpineClause = Clause' SpineLHS

type Clause = Clause' LHS

data WhereDeclarations

Constructors

WhereDecls

Fields

• whereModule :: Maybe ModuleName
• whereDecls :: Maybe Declaration

  The declaration is a Section.

Instances

Eq WhereDeclarations

Defined in Agda.Syntax.Abstract

Methods

(==) :: WhereDeclarations -> WhereDeclarations -> Bool

(/=) :: WhereDeclarations -> WhereDeclarations -> Bool

Data WhereDeclarations

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> WhereDeclarations -> c WhereDeclarations

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c WhereDeclarations

toConstr :: WhereDeclarations -> Constr

dataTypeOf :: WhereDeclarations -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c WhereDeclarations)

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

gmapT :: (forall b. Data b => b -> b) -> WhereDeclarations -> WhereDeclarations

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WhereDeclarations -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WhereDeclarations -> r

gmapQ :: (forall d. Data d => d -> u) -> WhereDeclarations -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> WhereDeclarations -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> WhereDeclarations -> m WhereDeclarations

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WhereDeclarations -> m WhereDeclarations

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WhereDeclarations -> m WhereDeclarations

Show WhereDeclarations

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> WhereDeclarations -> ShowS

show :: WhereDeclarations -> String

showList :: [WhereDeclarations] -> ShowS

Generic WhereDeclarations

Defined in Agda.Syntax.Abstract

Associated Types

type Rep WhereDeclarations :: Type -> Type

Methods

from :: WhereDeclarations -> Rep WhereDeclarations x

to :: Rep WhereDeclarations x -> WhereDeclarations

NFData WhereDeclarations

Defined in Agda.Syntax.Abstract

Methods

rnf :: WhereDeclarations -> ()

Null WhereDeclarations

Defined in Agda.Syntax.Abstract

Methods

empty :: WhereDeclarations

null :: WhereDeclarations -> Bool

KillRange WhereDeclarations

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT WhereDeclarations

HasRange WhereDeclarations

Defined in Agda.Syntax.Abstract

Methods

getRange :: WhereDeclarations -> Range

DeclaredNames WhereDeclarations

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => WhereDeclarations -> m

ExprLike WhereDeclarations

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m WhereDeclarations

foldExpr :: FoldExprFn m WhereDeclarations

traverseExpr :: TraverseExprFn m WhereDeclarations

mapExpr :: (Expr -> Expr) -> WhereDeclarations -> WhereDeclarations

ToConcrete WhereDeclarations

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs WhereDeclarations

Methods

toConcrete :: WhereDeclarations -> AbsToCon (ConOfAbs WhereDeclarations)

bindToConcrete :: WhereDeclarations -> (ConOfAbs WhereDeclarations -> AbsToCon b) -> AbsToCon b

type Rep WhereDeclarations

Defined in Agda.Syntax.Abstract

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

type ConOfAbs WhereDeclarations

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs WhereDeclarations = WhereClause

data Clause' lhs

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

Constructors

Clause

Fields

• clauseLHS :: lhs
• clauseStrippedPats :: [ProblemEq]

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

• clauseRHS :: RHS
• clauseWhereDecls :: WhereDeclarations
• clauseCatchall :: Bool

Instances

Functor Clause'

Defined in Agda.Syntax.Abstract

Methods

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

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

Foldable Clause'

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'

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)

DeclaredNames Clause

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => Clause -> m

LHSToSpine Clause SpineClause

Clause instance.

Defined in Agda.Syntax.Abstract.Pattern

Methods

lhsToSpine :: Clause -> SpineClause

spineToLhs :: SpineClause -> Clause

Eq lhs => Eq (Clause' lhs)

Defined in Agda.Syntax.Abstract

Methods

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

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

Data lhs => Data (Clause' lhs)

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Clause' lhs -> c (Clause' lhs)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Clause' lhs)

toConstr :: Clause' lhs -> Constr

dataTypeOf :: Clause' lhs -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Clause' lhs -> Clause' lhs

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

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

gmapQ :: (forall d. Data d => d -> u) -> Clause' lhs -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Clause' lhs -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Clause' lhs -> m (Clause' lhs)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause' lhs -> m (Clause' lhs)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause' lhs -> m (Clause' lhs)

Show lhs => Show (Clause' lhs)

Defined in Agda.Syntax.Abstract

Methods

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

show :: Clause' lhs -> String

showList :: [Clause' lhs] -> ShowS

Generic (Clause' lhs)

Defined in Agda.Syntax.Abstract

Associated Types

type Rep (Clause' lhs) :: Type -> Type

Methods

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

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

NFData lhs => NFData (Clause' lhs)

Defined in Agda.Syntax.Abstract

Methods

rnf :: Clause' lhs -> ()

KillRange a => KillRange (Clause' a)

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT (Clause' a)

HasRange a => HasRange (Clause' a)

Defined in Agda.Syntax.Abstract

Methods

getRange :: Clause' a -> Range

ExprLike a => ExprLike (Clause' a)

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m (Clause' a)

foldExpr :: FoldExprFn m (Clause' a)

traverseExpr :: TraverseExprFn m (Clause' a)

mapExpr :: (Expr -> Expr) -> Clause' a -> Clause' a

(ToConcrete a, ConOfAbs a ~ LHS) => ToConcrete (Clause' a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Clause' a)

Methods

toConcrete :: Clause' a -> AbsToCon (ConOfAbs (Clause' a))

bindToConcrete :: Clause' a -> (ConOfAbs (Clause' a) -> AbsToCon b) -> AbsToCon b

type Rep (Clause' lhs)

Defined in Agda.Syntax.Abstract

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

type ConOfAbs (Clause' a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Clause' a) = [Declaration]

data ProblemEq

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

Constructors

ProblemEq

Fields

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

Instances

Eq ProblemEq

Defined in Agda.Syntax.Abstract

Methods

(==) :: ProblemEq -> ProblemEq -> Bool

(/=) :: ProblemEq -> ProblemEq -> Bool

Data ProblemEq

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProblemEq -> c ProblemEq

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProblemEq

toConstr :: ProblemEq -> Constr

dataTypeOf :: ProblemEq -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProblemEq)

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

gmapT :: (forall b. Data b => b -> b) -> ProblemEq -> ProblemEq

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProblemEq -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProblemEq -> r

gmapQ :: (forall d. Data d => d -> u) -> ProblemEq -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ProblemEq -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq

Show ProblemEq

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> ProblemEq -> ShowS

show :: ProblemEq -> String

showList :: [ProblemEq] -> ShowS

Generic ProblemEq

Defined in Agda.Syntax.Abstract

Associated Types

type Rep ProblemEq :: Type -> Type

Methods

from :: ProblemEq -> Rep ProblemEq x

to :: Rep ProblemEq x -> ProblemEq

NFData ProblemEq

Defined in Agda.Syntax.Abstract

Methods

rnf :: ProblemEq -> ()

KillRange ProblemEq

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT ProblemEq

Subst ProblemEq

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg ProblemEq

Methods

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

PrettyTCM ProblemEq

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: MonadPretty m => ProblemEq -> m Doc

type Rep ProblemEq

Defined in Agda.Syntax.Abstract

type Rep ProblemEq = D1 ('MetaData "ProblemEq" "Agda.Syntax.Abstract" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" '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)))))

type SubstArg ProblemEq

Defined in Agda.TypeChecking.Substitute

type SubstArg ProblemEq = Term

data DataDefParams

Constructors

DataDefParams

Fields

• dataDefGeneralizedParams :: Set Name

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

• dataDefParams :: [LamBinding]

Instances

Eq DataDefParams

Defined in Agda.Syntax.Abstract

Methods

(==) :: DataDefParams -> DataDefParams -> Bool

(/=) :: DataDefParams -> DataDefParams -> Bool

Data DataDefParams

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataDefParams -> c DataDefParams

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataDefParams

toConstr :: DataDefParams -> Constr

dataTypeOf :: DataDefParams -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataDefParams)

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

gmapT :: (forall b. Data b => b -> b) -> DataDefParams -> DataDefParams

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataDefParams -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataDefParams -> r

gmapQ :: (forall d. Data d => d -> u) -> DataDefParams -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> DataDefParams -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataDefParams -> m DataDefParams

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataDefParams -> m DataDefParams

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataDefParams -> m DataDefParams

Show DataDefParams

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> DataDefParams -> ShowS

show :: DataDefParams -> String

showList :: [DataDefParams] -> ShowS

Generic DataDefParams

Defined in Agda.Syntax.Abstract

Associated Types

type Rep DataDefParams :: Type -> Type

Methods

from :: DataDefParams -> Rep DataDefParams x

to :: Rep DataDefParams x -> DataDefParams

NFData DataDefParams

Defined in Agda.Syntax.Abstract

Methods

rnf :: DataDefParams -> ()

KillRange DataDefParams

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT DataDefParams

ExprLike DataDefParams

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m DataDefParams

foldExpr :: FoldExprFn m DataDefParams

traverseExpr :: TraverseExprFn m DataDefParams

mapExpr :: (Expr -> Expr) -> DataDefParams -> DataDefParams

type Rep DataDefParams

Defined in Agda.Syntax.Abstract

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

Constructors

GeneralizeTel

Fields

• generalizeTelVars :: Map QName Name

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

• generalizeTel :: Telescope

Instances

Eq GeneralizeTelescope

Defined in Agda.Syntax.Abstract

Methods

(==) :: GeneralizeTelescope -> GeneralizeTelescope -> Bool

(/=) :: GeneralizeTelescope -> GeneralizeTelescope -> Bool

Data GeneralizeTelescope

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GeneralizeTelescope -> c GeneralizeTelescope

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GeneralizeTelescope

toConstr :: GeneralizeTelescope -> Constr

dataTypeOf :: GeneralizeTelescope -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GeneralizeTelescope)

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

gmapT :: (forall b. Data b => b -> b) -> GeneralizeTelescope -> GeneralizeTelescope

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GeneralizeTelescope -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GeneralizeTelescope -> r

gmapQ :: (forall d. Data d => d -> u) -> GeneralizeTelescope -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> GeneralizeTelescope -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> GeneralizeTelescope -> m GeneralizeTelescope

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GeneralizeTelescope -> m GeneralizeTelescope

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GeneralizeTelescope -> m GeneralizeTelescope

Show GeneralizeTelescope

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> GeneralizeTelescope -> ShowS

show :: GeneralizeTelescope -> String

showList :: [GeneralizeTelescope] -> ShowS

Generic GeneralizeTelescope

Defined in Agda.Syntax.Abstract

Associated Types

type Rep GeneralizeTelescope :: Type -> Type

Methods

from :: GeneralizeTelescope -> Rep GeneralizeTelescope x

to :: Rep GeneralizeTelescope x -> GeneralizeTelescope

NFData GeneralizeTelescope

Defined in Agda.Syntax.Abstract

Methods

rnf :: GeneralizeTelescope -> ()

KillRange GeneralizeTelescope

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT GeneralizeTelescope

ExprLike GeneralizeTelescope

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m GeneralizeTelescope

foldExpr :: FoldExprFn m GeneralizeTelescope

traverseExpr :: TraverseExprFn m GeneralizeTelescope

mapExpr :: (Expr -> Expr) -> GeneralizeTelescope -> GeneralizeTelescope

type Rep GeneralizeTelescope

Defined in Agda.Syntax.Abstract

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

type Telescope = [TypedBinding]

type Telescope1 = List1 TypedBinding

data TypedBinding

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 TacticAttr (List1 (NamedArg Binder)) Expr

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

Eq TypedBinding

Defined in Agda.Syntax.Abstract

Methods

(==) :: TypedBinding -> TypedBinding -> Bool

(/=) :: TypedBinding -> TypedBinding -> Bool

Data TypedBinding

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypedBinding -> c TypedBinding

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypedBinding

toConstr :: TypedBinding -> Constr

dataTypeOf :: TypedBinding -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TypedBinding)

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

gmapT :: (forall b. Data b => b -> b) -> TypedBinding -> TypedBinding

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypedBinding -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypedBinding -> r

gmapQ :: (forall d. Data d => d -> u) -> TypedBinding -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> TypedBinding -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypedBinding -> m TypedBinding

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBinding -> m TypedBinding

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBinding -> m TypedBinding

Show TypedBinding

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> TypedBinding -> ShowS

show :: TypedBinding -> String

showList :: [TypedBinding] -> ShowS

Generic TypedBinding

Defined in Agda.Syntax.Abstract

Associated Types

type Rep TypedBinding :: Type -> Type

Methods

from :: TypedBinding -> Rep TypedBinding x

to :: Rep TypedBinding x -> TypedBinding

NFData TypedBinding

Defined in Agda.Syntax.Abstract

Methods

rnf :: TypedBinding -> ()

KillRange TypedBinding

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT TypedBinding

HasRange TypedBinding

Defined in Agda.Syntax.Abstract

Methods

getRange :: TypedBinding -> Range

LensHiding TypedBinding

Defined in Agda.Syntax.Abstract

Methods

getHiding :: TypedBinding -> Hiding

setHiding :: Hiding -> TypedBinding -> TypedBinding

mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding

ExprLike TypedBinding

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m TypedBinding

foldExpr :: FoldExprFn m TypedBinding

traverseExpr :: TraverseExprFn m TypedBinding

mapExpr :: (Expr -> Expr) -> TypedBinding -> TypedBinding

PrettyTCM TypedBinding

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => TypedBinding -> m Doc

ToConcrete TypedBinding

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs TypedBinding

Methods

toConcrete :: TypedBinding -> AbsToCon (ConOfAbs TypedBinding)

bindToConcrete :: TypedBinding -> (ConOfAbs TypedBinding -> AbsToCon b) -> AbsToCon b

type Rep TypedBinding

Defined in Agda.Syntax.Abstract

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

type ConOfAbs TypedBinding

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs TypedBinding = Maybe TypedBinding

data LamBinding

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

Eq LamBinding

Defined in Agda.Syntax.Abstract

Methods

(==) :: LamBinding -> LamBinding -> Bool

(/=) :: LamBinding -> LamBinding -> Bool

Data LamBinding

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LamBinding -> c LamBinding

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LamBinding

toConstr :: LamBinding -> Constr

dataTypeOf :: LamBinding -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LamBinding)

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

gmapT :: (forall b. Data b => b -> b) -> LamBinding -> LamBinding

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LamBinding -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LamBinding -> r

gmapQ :: (forall d. Data d => d -> u) -> LamBinding -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> LamBinding -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LamBinding -> m LamBinding

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LamBinding -> m LamBinding

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LamBinding -> m LamBinding

Show LamBinding

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> LamBinding -> ShowS

show :: LamBinding -> String

showList :: [LamBinding] -> ShowS

Generic LamBinding

Defined in Agda.Syntax.Abstract

Associated Types

type Rep LamBinding :: Type -> Type

Methods

from :: LamBinding -> Rep LamBinding x

to :: Rep LamBinding x -> LamBinding

NFData LamBinding

Defined in Agda.Syntax.Abstract

Methods

rnf :: LamBinding -> ()

KillRange LamBinding

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT LamBinding

HasRange LamBinding

Defined in Agda.Syntax.Abstract

Methods

getRange :: LamBinding -> Range

LensHiding LamBinding

Defined in Agda.Syntax.Abstract

Methods

getHiding :: LamBinding -> Hiding

setHiding :: Hiding -> LamBinding -> LamBinding

mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding

ExprLike LamBinding

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m LamBinding

foldExpr :: FoldExprFn m LamBinding

traverseExpr :: TraverseExprFn m LamBinding

mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding

ToConcrete LamBinding

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LamBinding

Methods

toConcrete :: LamBinding -> AbsToCon (ConOfAbs LamBinding)

bindToConcrete :: LamBinding -> (ConOfAbs LamBinding -> AbsToCon b) -> AbsToCon b

type Rep LamBinding

Defined in Agda.Syntax.Abstract

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

type ConOfAbs LamBinding

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs LamBinding = Maybe LamBinding

type Binder = Binder' BindName

data Binder' a

Constructors

Binder

Fields

• binderPattern :: Maybe Pattern
• binderName :: a

Instances

Functor Binder'

Defined in Agda.Syntax.Abstract

Methods

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

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

Foldable Binder'

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'

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)

Eq a => Eq (Binder' a)

Defined in Agda.Syntax.Abstract

Methods

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

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

Data a => Data (Binder' a)

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Binder' a -> c (Binder' a)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Binder' a)

toConstr :: Binder' a -> Constr

dataTypeOf :: Binder' a -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Binder' a))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Binder' a))

gmapT :: (forall b. Data b => b -> b) -> Binder' a -> Binder' a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Binder' a -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binder' a -> r

gmapQ :: (forall d. Data d => d -> u) -> Binder' a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Binder' a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Binder' a -> m (Binder' a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder' a -> m (Binder' a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder' a -> m (Binder' a)

Show a => Show (Binder' a)

Defined in Agda.Syntax.Abstract

Methods

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

show :: Binder' a -> String

showList :: [Binder' a] -> ShowS

Generic (Binder' a)

Defined in Agda.Syntax.Abstract

Associated Types

type Rep (Binder' a) :: Type -> Type

Methods

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

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

NFData a => NFData (Binder' a)

Defined in Agda.Syntax.Abstract

Methods

rnf :: Binder' a -> ()

KillRange a => KillRange (Binder' a)

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT (Binder' a)

HasRange a => HasRange (Binder' a)

Defined in Agda.Syntax.Abstract

Methods

getRange :: Binder' a -> Range

ToConcrete a => ToConcrete (Binder' a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Binder' a)

Methods

toConcrete :: Binder' a -> AbsToCon (ConOfAbs (Binder' a))

bindToConcrete :: Binder' a -> (ConOfAbs (Binder' a) -> AbsToCon b) -> AbsToCon b

type Rep (Binder' a)

Defined in Agda.Syntax.Abstract

type Rep (Binder' a) = D1 ('MetaData "Binder'" "Agda.Syntax.Abstract" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" '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)))

type ConOfAbs (Binder' a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Binder' a) = Binder' (ConOfAbs a)

type TacticAttr = Maybe Expr

type Field = TypeSignature

type Constructor = TypeSignature

type TypeSignature = Declaration

Only Axioms.

data LetBinding

Bindings that are valid in a let.

Constructors

LetBind LetInfo ArgInfo BindName Expr Expr

LetBind info rel name type defn

LetPatBind LetInfo Pattern Expr

Irrefutable pattern binding.

LetApply ModuleInfo 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. | LetGeneralize DefInfo ArgInfo Expr

Instances

Eq LetBinding

Defined in Agda.Syntax.Abstract

Methods

(==) :: LetBinding -> LetBinding -> Bool

(/=) :: LetBinding -> LetBinding -> Bool

Data LetBinding

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LetBinding -> c LetBinding

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LetBinding

toConstr :: LetBinding -> Constr

dataTypeOf :: LetBinding -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LetBinding)

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

gmapT :: (forall b. Data b => b -> b) -> LetBinding -> LetBinding

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LetBinding -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LetBinding -> r

gmapQ :: (forall d. Data d => d -> u) -> LetBinding -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> LetBinding -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LetBinding -> m LetBinding

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LetBinding -> m LetBinding

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LetBinding -> m LetBinding

Show LetBinding

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> LetBinding -> ShowS

show :: LetBinding -> String

showList :: [LetBinding] -> ShowS

Generic LetBinding

Defined in Agda.Syntax.Abstract

Associated Types

type Rep LetBinding :: Type -> Type

Methods

from :: LetBinding -> Rep LetBinding x

to :: Rep LetBinding x -> LetBinding

NFData LetBinding

Defined in Agda.Syntax.Abstract

Methods

rnf :: LetBinding -> ()

KillRange LetBinding

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT LetBinding

HasRange LetBinding

Defined in Agda.Syntax.Abstract

Methods

getRange :: LetBinding -> Range

ExprLike LetBinding

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m LetBinding

foldExpr :: FoldExprFn m LetBinding

traverseExpr :: TraverseExprFn m LetBinding

mapExpr :: (Expr -> Expr) -> LetBinding -> LetBinding

ToConcrete LetBinding

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LetBinding

Methods

toConcrete :: LetBinding -> AbsToCon (ConOfAbs LetBinding)

bindToConcrete :: LetBinding -> (ConOfAbs LetBinding -> AbsToCon b) -> AbsToCon b

type Rep LetBinding

Defined in Agda.Syntax.Abstract

type Rep LetBinding = D1 ('MetaData "LetBinding" "Agda.Syntax.Abstract" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" '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 Expr) :*: 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 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)))))

type ConOfAbs LetBinding

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs LetBinding = [Declaration]

data Pragma

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

DisplayPragma QName [NamedArg Pattern] Expr

Instances

Eq Pragma

Defined in Agda.Syntax.Abstract

Methods

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

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

Data Pragma

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pragma -> c Pragma

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Pragma

toConstr :: Pragma -> Constr

dataTypeOf :: Pragma -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Pragma)

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

gmapT :: (forall b. Data b => b -> b) -> Pragma -> Pragma

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pragma -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pragma -> r

gmapQ :: (forall d. Data d => d -> u) -> Pragma -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Pragma -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma

Show Pragma

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> Pragma -> ShowS

show :: Pragma -> String

showList :: [Pragma] -> ShowS

Generic Pragma

Defined in Agda.Syntax.Abstract

Associated Types

type Rep Pragma :: Type -> Type

Methods

from :: Pragma -> Rep Pragma x

to :: Rep Pragma x -> Pragma

NFData Pragma

Defined in Agda.Syntax.Abstract

Methods

rnf :: Pragma -> ()

DeclaredNames Pragma

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => Pragma -> m

ExprLike Pragma

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m Pragma

foldExpr :: FoldExprFn m Pragma

traverseExpr :: TraverseExprFn m Pragma

mapExpr :: (Expr -> Expr) -> Pragma -> Pragma

type Rep Pragma

Defined in Agda.Syntax.Abstract

type Rep Pragma = D1 ('MetaData "Pragma" "Agda.Syntax.Abstract" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" '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 "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 ModuleApplication

Constructors

SectionApp Telescope ModuleName [NamedArg Expr]

tel. M args: applies M to args and abstracts tel.

RecordModuleInstance ModuleName

M {{...}}

Instances

Eq ModuleApplication

Defined in Agda.Syntax.Abstract

Methods

(==) :: ModuleApplication -> ModuleApplication -> Bool

(/=) :: ModuleApplication -> ModuleApplication -> Bool

Data ModuleApplication

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModuleApplication -> c ModuleApplication

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModuleApplication

toConstr :: ModuleApplication -> Constr

dataTypeOf :: ModuleApplication -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModuleApplication)

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

gmapT :: (forall b. Data b => b -> b) -> ModuleApplication -> ModuleApplication

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModuleApplication -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModuleApplication -> r

gmapQ :: (forall d. Data d => d -> u) -> ModuleApplication -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ModuleApplication -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModuleApplication -> m ModuleApplication

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleApplication -> m ModuleApplication

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleApplication -> m ModuleApplication

Show ModuleApplication

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> ModuleApplication -> ShowS

show :: ModuleApplication -> String

showList :: [ModuleApplication] -> ShowS

Generic ModuleApplication

Defined in Agda.Syntax.Abstract

Associated Types

type Rep ModuleApplication :: Type -> Type

Methods

from :: ModuleApplication -> Rep ModuleApplication x

to :: Rep ModuleApplication x -> ModuleApplication

NFData ModuleApplication

Defined in Agda.Syntax.Abstract

Methods

rnf :: ModuleApplication -> ()

KillRange ModuleApplication

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT ModuleApplication

ExprLike ModuleApplication

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m ModuleApplication

foldExpr :: FoldExprFn m ModuleApplication

traverseExpr :: TraverseExprFn m ModuleApplication

mapExpr :: (Expr -> Expr) -> ModuleApplication -> ModuleApplication

ToConcrete ModuleApplication

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ModuleApplication

Methods

toConcrete :: ModuleApplication -> AbsToCon (ConOfAbs ModuleApplication)

bindToConcrete :: ModuleApplication -> (ConOfAbs ModuleApplication -> AbsToCon b) -> AbsToCon b

type Rep ModuleApplication

Defined in Agda.Syntax.Abstract

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

type ConOfAbs ModuleApplication

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs ModuleApplication = ModuleApplication

type ImportedName = ImportedName' QName ModuleName

type Renaming = Renaming' QName ModuleName

type ImportDirective = ImportDirective' QName ModuleName

type DefInfo = DefInfo' Expr

data Declaration

Constructors

Axiom KindOfName DefInfo ArgInfo (Maybe [Occurrence]) QName Expr

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 Expr

First argument is set of generalizable variables used in the type.

Field DefInfo QName (Arg Expr)

record field

Primitive DefInfo QName (Arg Expr)

primitive function

Mutual MutualInfo [Declaration]

a bunch of mutually recursive definitions

Section Range ModuleName GeneralizeTelescope [Declaration]

Apply ModuleInfo 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

only retained for highlighting purposes

FunDef DefInfo QName Delayed [Clause]

sequence of function clauses

DataSig DefInfo QName GeneralizeTelescope Expr

lone data signature

DataDef DefInfo QName UniverseCheck DataDefParams [Constructor]

RecSig DefInfo QName GeneralizeTelescope Expr

lone record signature

RecDef DefInfo QName UniverseCheck RecordDirectives DataDefParams Expr [Declaration]

The Expr gives the constructor type telescope, (x1 : A1)..(xn : An) -> Prop, 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

ScopedDecl ScopeInfo [Declaration]

scope annotation

Instances

Eq Declaration

Does not compare ScopeInfo fields.

Defined in Agda.Syntax.Abstract

Methods

(==) :: Declaration -> Declaration -> Bool

(/=) :: Declaration -> Declaration -> Bool

Data Declaration

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Declaration -> c Declaration

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Declaration

toConstr :: Declaration -> Constr

dataTypeOf :: Declaration -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Declaration)

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

gmapT :: (forall b. Data b => b -> b) -> Declaration -> Declaration

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Declaration -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Declaration -> r

gmapQ :: (forall d. Data d => d -> u) -> Declaration -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Declaration -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration

Show Declaration

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> Declaration -> ShowS

show :: Declaration -> String

showList :: [Declaration] -> ShowS

Generic Declaration

Defined in Agda.Syntax.Abstract

Associated Types

type Rep Declaration :: Type -> Type

Methods

from :: Declaration -> Rep Declaration x

to :: Rep Declaration x -> Declaration

NFData Declaration

Defined in Agda.Syntax.Abstract

Methods

rnf :: Declaration -> ()

KillRange Declaration

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT Declaration

HasRange Declaration

Defined in Agda.Syntax.Abstract

Methods

getRange :: Declaration -> Range

AnyAbstract Declaration

Defined in Agda.Syntax.Abstract

Methods

anyAbstract :: Declaration -> Bool

DeclaredNames Declaration

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => Declaration -> m

ExprLike Declaration

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m Declaration

foldExpr :: FoldExprFn m Declaration

traverseExpr :: TraverseExprFn m Declaration

mapExpr :: (Expr -> Expr) -> Declaration -> Declaration

ToConcrete Declaration

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Declaration

Methods

toConcrete :: Declaration -> AbsToCon (ConOfAbs Declaration)

bindToConcrete :: Declaration -> (ConOfAbs Declaration -> AbsToCon b) -> AbsToCon b

ShowHead Declaration

Defined in Agda.TypeChecking.Rules.Decl

Methods

showHead :: Declaration -> String

ToConcrete (Constr Constructor)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Constr Constructor)

Methods

toConcrete :: Constr Constructor -> AbsToCon (ConOfAbs (Constr Constructor))

bindToConcrete :: Constr Constructor -> (ConOfAbs (Constr Constructor) -> AbsToCon b) -> AbsToCon b

type Rep Declaration

Defined in Agda.Syntax.Abstract

type Rep Declaration = D1 ('MetaData "Declaration" "Agda.Syntax.Abstract" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" '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 Expr)))) :+: 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 Expr))))) :+: (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 Expr)))) :+: 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 Expr)))))) :+: ((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 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 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 Delayed) :*: 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 QName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralizeTelescope) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: (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 QName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralizeTelescope) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))))) :+: ((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 Expr) :*: 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 "ScopedDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])))))))

type ConOfAbs Declaration

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs Declaration = [Declaration]

type ConOfAbs (Constr Constructor)

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Constr Constructor) = Declaration

type RecordDirectives = RecordDirectives' QName

data ScopeCopyInfo

Constructors

ScopeCopyInfo

Fields

• renModules :: Ren ModuleName
• renNames :: Ren QName

Instances

Eq ScopeCopyInfo

Defined in Agda.Syntax.Abstract

Methods

(==) :: ScopeCopyInfo -> ScopeCopyInfo -> Bool

(/=) :: ScopeCopyInfo -> ScopeCopyInfo -> Bool

Data ScopeCopyInfo

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ScopeCopyInfo -> c ScopeCopyInfo

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ScopeCopyInfo

toConstr :: ScopeCopyInfo -> Constr

dataTypeOf :: ScopeCopyInfo -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ScopeCopyInfo)

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

gmapT :: (forall b. Data b => b -> b) -> ScopeCopyInfo -> ScopeCopyInfo

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ScopeCopyInfo -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ScopeCopyInfo -> r

gmapQ :: (forall d. Data d => d -> u) -> ScopeCopyInfo -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ScopeCopyInfo -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ScopeCopyInfo -> m ScopeCopyInfo

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ScopeCopyInfo -> m ScopeCopyInfo

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ScopeCopyInfo -> m ScopeCopyInfo

Show ScopeCopyInfo

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> ScopeCopyInfo -> ShowS

show :: ScopeCopyInfo -> String

showList :: [ScopeCopyInfo] -> ShowS

Generic ScopeCopyInfo

Defined in Agda.Syntax.Abstract

Associated Types

type Rep ScopeCopyInfo :: Type -> Type

Methods

from :: ScopeCopyInfo -> Rep ScopeCopyInfo x

to :: Rep ScopeCopyInfo x -> ScopeCopyInfo

NFData ScopeCopyInfo

Defined in Agda.Syntax.Abstract

Methods

rnf :: ScopeCopyInfo -> ()

Pretty ScopeCopyInfo

Defined in Agda.Syntax.Abstract

Methods

pretty :: ScopeCopyInfo -> Doc

prettyPrec :: Int -> ScopeCopyInfo -> Doc

prettyList :: [ScopeCopyInfo] -> Doc

KillRange ScopeCopyInfo

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT ScopeCopyInfo

type Rep ScopeCopyInfo

Defined in Agda.Syntax.Abstract

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

Renaming (generic).

type RecordAssigns = [RecordAssign]

type RecordAssign = Either Assign ModuleName

type Assigns = [Assign]

type Assign = FieldAssignment' Expr

Record field assignment f = e.

data Expr

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 Expr

Dependent function space Γ → A.

Generalized (Set QName) Expr

Like a Pi, but the ordering is not known

Fun ExprInfo (Arg Expr) Expr

Non-dependent function space.

Let ExprInfo (List1 LetBinding) Expr

let bs in e.

ETel Telescope

Only used when printing telescopes.

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

Eq Expr

Does not compare ScopeInfo fields. Does not distinguish between prefix and postfix projections.

Defined in Agda.Syntax.Abstract

Methods

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

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

Data Expr

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Expr -> c Expr

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Expr

toConstr :: Expr -> Constr

dataTypeOf :: Expr -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Expr)

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

gmapT :: (forall b. Data b => b -> b) -> Expr -> Expr

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r

gmapQ :: (forall d. Data d => d -> u) -> Expr -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Expr -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Expr -> m Expr

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr

Show Expr

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> Expr -> ShowS

show :: Expr -> String

showList :: [Expr] -> ShowS

Generic Expr

Defined in Agda.Syntax.Abstract

Associated Types

type Rep Expr :: Type -> Type

Methods

from :: Expr -> Rep Expr x

to :: Rep Expr x -> Expr

NFData Expr

Defined in Agda.Syntax.Abstract

Methods

rnf :: Expr -> ()

KillRange Expr

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT Expr

HasRange Expr

Defined in Agda.Syntax.Abstract

Methods

getRange :: Expr -> Range

Underscore Expr

Defined in Agda.Syntax.Abstract

Methods

underscore :: Expr

isUnderscore :: Expr -> Bool

IsProjP Expr

Defined in Agda.Syntax.Abstract

Methods

isProjP :: Expr -> Maybe (ProjOrigin, AmbiguousQName)

SubstExpr Expr

Defined in Agda.Syntax.Abstract

Methods

substExpr :: [(Name, Expr)] -> Expr -> Expr

ExprLike Expr

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m Expr

foldExpr :: FoldExprFn m Expr

traverseExpr :: TraverseExprFn m Expr

mapExpr :: (Expr -> Expr) -> Expr -> Expr

MapNamedArgPattern NAP

Defined in Agda.Syntax.Abstract.Pattern

Methods

mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP

PrettyTCM Expr

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Expr -> m Doc

ToConcrete Pattern

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Pattern

Methods

toConcrete :: Pattern -> AbsToCon (ConOfAbs Pattern)

bindToConcrete :: Pattern -> (ConOfAbs Pattern -> AbsToCon b) -> AbsToCon b

ToConcrete LHSCore

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHSCore

Methods

toConcrete :: LHSCore -> AbsToCon (ConOfAbs LHSCore)

bindToConcrete :: LHSCore -> (ConOfAbs LHSCore -> AbsToCon b) -> AbsToCon b

ToConcrete Expr

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Expr

Methods

toConcrete :: Expr -> AbsToCon (ConOfAbs Expr)

bindToConcrete :: Expr -> (ConOfAbs Expr -> AbsToCon b) -> AbsToCon b

Reify Expr

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Expr

Methods

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

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

IsFlexiblePattern Pattern

Defined in Agda.TypeChecking.Rules.LHS

Methods

maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Pattern -> MaybeT m FlexibleVarKind

isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Pattern -> m Bool

PrettyTCM (NamedArg Expr)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => NamedArg Expr -> m Doc

PrettyTCM (Arg Expr)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Arg Expr -> m Doc

ToConcrete (Maybe Pattern)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe Pattern)

Methods

toConcrete :: Maybe Pattern -> AbsToCon (ConOfAbs (Maybe Pattern))

bindToConcrete :: Maybe Pattern -> (ConOfAbs (Maybe Pattern) -> AbsToCon b) -> AbsToCon b

ToAbstract (Expr, Elims)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elims)

Methods

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

ToAbstract (Expr, Elim)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elim)

Methods

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

ToAbstract (RewriteEqn' () BindName Pattern Expr)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (RewriteEqn' () BindName Pattern Expr)

Methods

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

type Rep Expr

Defined in Agda.Syntax.Abstract

type Rep Expr = D1 ('MetaData "Expr" "Agda.Syntax.Abstract" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" '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 Expr))))) :+: ((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 Expr)) :+: 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 Expr)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: (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 "ETel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope))))) :+: ((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 Pattern

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs Pattern = Pattern

type ConOfAbs LHSCore

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs LHSCore = Pattern

type ConOfAbs Expr

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs Expr = Expr

type ReifiesTo Expr

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo Expr = Expr

type ConOfAbs (Maybe Pattern)

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Maybe Pattern) = Maybe Pattern

type AbsOfRef (Expr, Elims)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Expr, Elims) = Expr

type AbsOfRef (Expr, Elim)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Expr, Elim) = Expr

type AbsOfCon (RewriteEqn' () BindName Pattern Expr)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqn

type Args = [NamedArg Expr]

newtype BindName

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

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

Constructors

BindName

Fields

• unBind :: Name

Instances

Eq BindName

Defined in Agda.Syntax.Abstract

Methods

(==) :: BindName -> BindName -> Bool

(/=) :: BindName -> BindName -> Bool

Data BindName

Defined in Agda.Syntax.Abstract

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BindName -> c BindName

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BindName

toConstr :: BindName -> Constr

dataTypeOf :: BindName -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BindName)

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

gmapT :: (forall b. Data b => b -> b) -> BindName -> BindName

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BindName -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BindName -> r

gmapQ :: (forall d. Data d => d -> u) -> BindName -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> BindName -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BindName -> m BindName

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BindName -> m BindName

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BindName -> m BindName

Ord BindName

Defined in Agda.Syntax.Abstract

Methods

compare :: BindName -> BindName -> Ordering

(<) :: BindName -> BindName -> Bool

(<=) :: BindName -> BindName -> Bool

(>) :: BindName -> BindName -> Bool

(>=) :: BindName -> BindName -> Bool

max :: BindName -> BindName -> BindName

min :: BindName -> BindName -> BindName

Show BindName

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> BindName -> ShowS

show :: BindName -> String

showList :: [BindName] -> ShowS

NFData BindName

Defined in Agda.Syntax.Abstract

Methods

rnf :: BindName -> ()

KillRange BindName

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT BindName

SetRange BindName

Defined in Agda.Syntax.Abstract

Methods

setRange :: Range -> BindName -> BindName

HasRange BindName

Defined in Agda.Syntax.Abstract

Methods

getRange :: BindName -> Range

ExprLike BindName

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m BindName

foldExpr :: FoldExprFn m BindName

traverseExpr :: TraverseExprFn m BindName

mapExpr :: (Expr -> Expr) -> BindName -> BindName

EmbPrj BindName

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: BindName -> S Int32

icod_ :: BindName -> S Int32

value :: Int32 -> R BindName

ToConcrete BindName

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs BindName

Methods

toConcrete :: BindName -> AbsToCon (ConOfAbs BindName)

bindToConcrete :: BindName -> (ConOfAbs BindName -> AbsToCon b) -> AbsToCon b

ToConcrete (Maybe BindName)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe BindName)

Methods

toConcrete :: Maybe BindName -> AbsToCon (ConOfAbs (Maybe BindName))

bindToConcrete :: Maybe BindName -> (ConOfAbs (Maybe BindName) -> AbsToCon b) -> AbsToCon b

(ToConcrete p, ToConcrete a) => ToConcrete (RewriteEqn' qn BindName p a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (RewriteEqn' qn BindName p a)

Methods

toConcrete :: RewriteEqn' qn BindName p a -> AbsToCon (ConOfAbs (RewriteEqn' qn BindName p a))

bindToConcrete :: RewriteEqn' qn BindName p a -> (ConOfAbs (RewriteEqn' qn BindName p a) -> AbsToCon b) -> AbsToCon b

ToAbstract (RewriteEqn' () BindName Pattern Expr)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (RewriteEqn' () BindName Pattern Expr)

Methods

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

type ConOfAbs BindName

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs BindName = BoundName

type ConOfAbs (Maybe BindName)

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Maybe BindName) = Maybe Name

type ConOfAbs (RewriteEqn' qn BindName p a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (RewriteEqn' qn BindName p a) = RewriteEqn' () Name (ConOfAbs p) (ConOfAbs a)

type AbsOfCon (RewriteEqn' () BindName Pattern Expr)

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqn

pattern Def :: QName -> Expr

Pattern synonym for regular Def

mkBindName :: Name -> BindName

generalized :: Set QName -> Expr -> Expr

Smart constructor for Generalized

initCopyInfo :: ScopeCopyInfo

mkBinder :: a -> Binder' a

mkBinder_ :: Name -> Binder

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

mkDomainFree :: NamedArg Binder -> LamBinding

mkTBind :: Range -> List1 (NamedArg Binder) -> Expr -> TypedBinding

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

mkPi :: ExprInfo -> Telescope -> Expr -> Expr

noDataDefParams :: DataDefParams

noWhereDecls :: WhereDeclarations

axiomName :: Declaration -> QName

The name defined by the given axiom.

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

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

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

patternToExpr :: Pattern -> Expr

lambdaLiftExpr :: [Name] -> Expr -> Expr

insertImplicitPatSynArgs :: HasRange a => (Range -> a) -> Range -> [Arg Name] -> [NamedArg a] -> Maybe ([(Name, a)], [Arg Name])

module Agda.Syntax.Abstract.Name

Orphan instances

KillRange Suffix

Methods

killRange :: KillRangeT Suffix