Agda-2.6.2.1: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Abstract

Description

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

Synopsis

Documentation

class SubstExpr a where Source #

Minimal complete definition

Nothing

Methods

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

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

Instances

Instances details
SubstExpr Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

SubstExpr ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract

SubstExpr Name Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

SubstExpr a => SubstExpr (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

SubstExpr a => SubstExpr (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

SubstExpr a => SubstExpr (List1 a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

SubstExpr a => SubstExpr (Maybe a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

SubstExpr a => SubstExpr [a] Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

SubstExpr a => SubstExpr (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

(SubstExpr a, SubstExpr b) => SubstExpr (Either a b) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

(SubstExpr a, SubstExpr b) => SubstExpr (a, b) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

class NameToExpr a where Source #

Turn a name into an expression.

Methods

nameToExpr :: a -> Expr Source #

Instances

Instances details
NameToExpr AbstractName Source #

Turn an AbstractName into an expression.

Instance details

Defined in Agda.Syntax.Abstract

NameToExpr ResolvedName Source #

Turn a ResolvedName into an expression.

Assumes name is not UnknownName.

Instance details

Defined in Agda.Syntax.Abstract

class AnyAbstract a where Source #

Are we in an abstract block?

In that case some definition is abstract.

Methods

anyAbstract :: a -> Bool Source #

Instances

Instances details
AnyAbstract Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

AnyAbstract a => AnyAbstract [a] Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

anyAbstract :: [a] -> Bool Source #

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

data Pattern' e Source #

Parameterised over the type of dot patterns.

Constructors

VarP BindName 
ConP ConPatInfo AmbiguousQName (NAPs e) 
ProjP PatInfo ProjOrigin AmbiguousQName

Destructor pattern d.

DefP PatInfo AmbiguousQName (NAPs e)

Defined pattern: function definition f ps. It is also abused to convert destructor patterns into concrete syntax thus, we put AmbiguousQName here as well.

WildP PatInfo

Underscore pattern entered by user. Or generated at type checking for implicit arguments.

AsP PatInfo BindName (Pattern' e) 
DotP PatInfo e

Dot pattern .e

AbsurdP PatInfo 
LitP PatInfo Literal 
PatternSynP PatInfo AmbiguousQName (NAPs e) 
RecP PatInfo [FieldAssignment' (Pattern' e)] 
EqualP PatInfo [(e, e)] 
WithP PatInfo (Pattern' e)

| p, for with-patterns.

AnnP PatInfo e (Pattern' e)

Pattern with type annotation

Instances

Instances details
MapNamedArgPattern NAP Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #

ToConcrete Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Pattern Source #

IsFlexiblePattern Pattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS

Foldable Pattern' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

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

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

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

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

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

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

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

null :: Pattern' a -> Bool #

length :: Pattern' a -> Int #

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

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

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

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

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

Traversable Pattern' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

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

Functor Pattern' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

IsProjP (Pattern' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

APatternLike (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (Pattern' a) Source #

Methods

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

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

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

Defined in Agda.Syntax.Abstract.Views

IsWithP (Pattern' e) Source #

Check for with-pattern.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

NamesIn (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

HasRange (Pattern' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: Pattern' e -> Range Source #

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

Defined in Agda.Syntax.Abstract

SetRange (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

ToConcrete (Maybe Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe Pattern) Source #

ToAbstract (Pattern' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Pattern' Expr) Source #

ExpandPatternSynonyms (Pattern' e) Source # 
Instance details

Defined in Agda.TypeChecking.Patterns.Abstract

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

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

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

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

Generic (Pattern' e) Source # 
Instance details

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 #

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

Defined in Agda.Syntax.Abstract

Methods

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

show :: Pattern' e -> String #

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

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

Defined in Agda.Syntax.Abstract

Methods

rnf :: Pattern' e -> () #

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

Defined in Agda.Syntax.Abstract

Methods

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

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

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

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

type ConOfAbs Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ADotT (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

type AbsOfCon (Pattern' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type Rep (Pattern' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data LHSCore' e Source #

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

Constructors

LHSHead

The head applied to ordinary patterns.

Fields

LHSProj

Projection.

Fields

LHSWith

With patterns.

Fields

Instances

Instances details
ToConcrete LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHSCore Source #

Foldable LHSCore' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

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

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

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

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

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

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

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

null :: LHSCore' a -> Bool #

length :: LHSCore' a -> Int #

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

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

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

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

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

Traversable LHSCore' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

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

Functor LHSCore' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

Defined in Agda.Syntax.Abstract.Views

HasRange (LHSCore' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: LHSCore' e -> Range Source #

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

Defined in Agda.Syntax.Abstract

ToAbstract (LHSCore' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (LHSCore' Expr) Source #

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

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

Generic (LHSCore' e) Source # 
Instance details

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 #

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

Defined in Agda.Syntax.Abstract

Methods

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

show :: LHSCore' e -> String #

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

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

Defined in Agda.Syntax.Abstract

Methods

rnf :: LHSCore' e -> () #

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

Defined in Agda.Syntax.Abstract

Methods

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

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

type ConOfAbs LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type AbsOfCon (LHSCore' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type Rep (LHSCore' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

data LHS Source #

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

Constructors

LHS 

Fields

Instances

Instances details
DeclaredNames Clause Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

HasRange LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: LHS -> Range Source #

KillRange LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete LHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHS Source #

Data LHS Source # 
Instance details

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 #

Generic LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep LHS :: Type -> Type #

Methods

from :: LHS -> Rep LHS x #

to :: Rep LHS x -> LHS #

Show LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> LHS -> ShowS #

show :: LHS -> String #

showList :: [LHS] -> ShowS #

NFData LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: LHS -> () #

Eq LHS Source #

Ignore Range' when comparing LHSs.

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

LHSToSpine Clause SpineClause Source #

Clause instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

LHSToSpine LHS SpineLHS Source #

LHS instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

type ConOfAbs LHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

data SpineLHS Source #

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

Constructors

SpineLHS 

Fields

Instances

Instances details
ExprLike SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

HasRange SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs SpineLHS Source #

Data SpineLHS Source # 
Instance details

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 #

Generic SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep SpineLHS :: Type -> Type #

Methods

from :: SpineLHS -> Rep SpineLHS x #

to :: Rep SpineLHS x -> SpineLHS #

Show SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: SpineLHS -> () #

Eq SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

LHSToSpine Clause SpineClause Source #

Clause instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

LHSToSpine LHS SpineLHS Source #

LHS instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

type ConOfAbs SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

data RHS Source #

Constructors

RHS 

Fields

AbsurdRHS 
WithRHS QName [WithExpr] [Clause]

The QName is the name of the with function.

RewriteRHS 

Fields

Instances

Instances details
DeclaredNames RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

HasRange RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: RHS -> Range Source #

KillRange RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RHS Source #

Data RHS Source # 
Instance details

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 #

Generic RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep RHS :: Type -> Type #

Methods

from :: RHS -> Rep RHS x #

to :: Rep RHS x -> RHS #

Show RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> RHS -> ShowS #

show :: RHS -> String #

showList :: [RHS] -> ShowS #

NFData RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: RHS -> () #

Eq RHS Source #

Ignore rhsConcrete when comparing RHSs.

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

type ConOfAbs RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

data WhereDeclarations Source #

Constructors

WhereDecls 

Fields

Instances

Instances details
DeclaredNames WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

HasRange WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs WhereDeclarations Source #

Null WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

Data WhereDeclarations Source # 
Instance details

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 #

Generic WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep WhereDeclarations :: Type -> Type #

Show WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: WhereDeclarations -> () #

Eq WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

type ConOfAbs WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

data Clause' lhs Source #

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

Constructors

Clause 

Fields

Instances

Instances details
DeclaredNames Clause Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Foldable Clause' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

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

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

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

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

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

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

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

null :: Clause' a -> Bool #

length :: Clause' a -> Int #

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

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

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

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

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

Traversable Clause' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

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

Functor Clause' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

LHSToSpine Clause SpineClause Source #

Clause instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

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

Defined in Agda.Syntax.Abstract.Views

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

Defined in Agda.Syntax.Abstract

Methods

getRange :: Clause' a -> Range Source #

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

Defined in Agda.Syntax.Abstract

(ToConcrete a, ConOfAbs a ~ LHS) => ToConcrete (Clause' a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Clause' a) Source #

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

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

Generic (Clause' lhs) Source # 
Instance details

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 #

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

Defined in Agda.Syntax.Abstract

Methods

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

show :: Clause' lhs -> String #

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

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

Defined in Agda.Syntax.Abstract

Methods

rnf :: Clause' lhs -> () #

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

Defined in Agda.Syntax.Abstract

Methods

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

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

type ConOfAbs (Clause' a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep (Clause' lhs) Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

data ProblemEq Source #

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

Instances

Instances details
KillRange ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

PrettyTCM ProblemEq Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Subst ProblemEq Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg ProblemEq Source #

Data ProblemEq Source # 
Instance details

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 #

Generic ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep ProblemEq :: Type -> Type #

Show ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: ProblemEq -> () #

Eq ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

type SubstArg ProblemEq Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type Rep ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

data DataDefParams Source #

Constructors

DataDefParams 

Fields

Instances

Instances details
ExprLike DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

KillRange DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

Data DataDefParams Source # 
Instance details

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 #

Generic DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep DataDefParams :: Type -> Type #

Show DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: DataDefParams -> () #

Eq DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

data GeneralizeTelescope Source #

Constructors

GeneralizeTel 

Fields

Instances

Instances details
ExprLike GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

KillRange GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

Data GeneralizeTelescope Source # 
Instance details

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 #

Generic GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep GeneralizeTelescope :: Type -> Type #

Show GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: GeneralizeTelescope -> () #

Eq GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

data TypedBinding Source #

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

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

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

Constructors

TBind Range 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

Instances details
ExprLike TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

LensHiding TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs TypedBinding Source #

PrettyTCM TypedBinding Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Data TypedBinding Source # 
Instance details

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 #

Generic TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep TypedBinding :: Type -> Type #

Show TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: TypedBinding -> () #

Eq TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

type ConOfAbs TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

data LamBinding Source #

A lambda binding is either domain free or typed.

Constructors

DomainFree TacticAttr (NamedArg Binder)

. x or {x} or .x or {x = y} or x@p or (p)

DomainFull TypedBinding

. (xs:e) or {xs:e} or (let Ds)

Instances

Instances details
ExprLike LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

LensHiding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LamBinding Source #

Data LamBinding Source # 
Instance details

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 #

Generic LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep LamBinding :: Type -> Type #

Show LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: LamBinding -> () #

Eq LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

type ConOfAbs LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

data Binder' a Source #

Constructors

Binder 

Instances

Instances details
Foldable Binder' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

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

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

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

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

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

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

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

null :: Binder' a -> Bool #

length :: Binder' a -> Int #

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

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

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

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

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

Traversable Binder' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

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

Functor Binder' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

Defined in Agda.Syntax.Abstract

Methods

getRange :: Binder' a -> Range Source #

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

Defined in Agda.Syntax.Abstract

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Binder' a) Source #

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

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

Generic (Binder' a) Source # 
Instance details

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 #

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

Defined in Agda.Syntax.Abstract

Methods

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

show :: Binder' a -> String #

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

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

Defined in Agda.Syntax.Abstract

Methods

rnf :: Binder' a -> () #

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

Defined in Agda.Syntax.Abstract

Methods

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

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

type ConOfAbs (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

data LetBinding Source #

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

Instances details
ExprLike LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

HasRange LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete LetBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LetBinding Source #

Data LetBinding Source # 
Instance details

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 #

Generic LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep LetBinding :: Type -> Type #

Show LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: LetBinding -> () #

Eq LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

type ConOfAbs LetBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

data Pragma Source #

Constructors

OptionsPragma [String] 
BuiltinPragma RString ResolvedName

ResolvedName is not UnknownName. Name can be ambiguous e.g. for built-in constructors.

BuiltinNoDefPragma RString KindOfName QName

Builtins that do not come with a definition, but declare a name for an Agda concept.

RewritePragma Range [QName]

Range is range of REWRITE keyword.

CompilePragma RString QName String 
StaticPragma QName 
EtaPragma QName

For coinductive records, use pragma instead of regular eta-equality definition (as it is might make Agda loop).

InjectivePragma QName 
InlinePragma Bool QName 
DisplayPragma QName [NamedArg Pattern] Expr 

Instances

Instances details
DeclaredNames Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Data Pragma Source # 
Instance details

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 #

Generic Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep Pragma :: Type -> Type #

Methods

from :: Pragma -> Rep Pragma x #

to :: Rep Pragma x -> Pragma #

Show Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: Pragma -> () #

Eq Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

type Rep Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep Pragma = D1 ('MetaData "Pragma" "Agda.Syntax.Abstract" "Agda-2.6.2.1-inplace" 'False) (((C1 ('MetaCons "OptionsPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])) :+: C1 ('MetaCons "BuiltinPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RString) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ResolvedName))) :+: (C1 ('MetaCons "BuiltinNoDefPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RString) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))) :+: (C1 ('MetaCons "RewritePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName])) :+: C1 ('MetaCons "CompilePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RString) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))))) :+: ((C1 ('MetaCons "StaticPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "EtaPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))) :+: (C1 ('MetaCons "InjectivePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: (C1 ('MetaCons "InlinePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "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 Source #

Constructors

SectionApp Telescope ModuleName [NamedArg Expr]

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

RecordModuleInstance ModuleName
M {{...}}

Instances

Instances details
ExprLike ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

KillRange ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ModuleApplication Source #

Data ModuleApplication Source # 
Instance details

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 #

Generic ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep ModuleApplication :: Type -> Type #

Show ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: ModuleApplication -> () #

Eq ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

type ConOfAbs ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

data Declaration Source #

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

Instances details
AnyAbstract Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

DeclaredNames Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

HasRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete Declaration Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Declaration Source #

ShowHead Declaration Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Decl

Data Declaration Source # 
Instance details

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 #

Generic Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep Declaration :: Type -> Type #

Show Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: Declaration -> () #

Eq Declaration Source #

Does not compare ScopeInfo fields.

Instance details

Defined in Agda.Syntax.Abstract

ToConcrete (Constr Constructor) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Constr Constructor) Source #

type ConOfAbs Declaration Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep Declaration = D1 ('MetaData "Declaration" "Agda.Syntax.Abstract" "Agda-2.6.2.1-inplace" 'False) ((((C1 ('MetaCons "Axiom" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe [Occurrence])) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 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 (Constr Constructor) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

data ScopeCopyInfo Source #

Instances

Instances details
KillRange ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

Pretty ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

Data ScopeCopyInfo Source # 
Instance details

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 #

Generic ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep ScopeCopyInfo :: Type -> Type #

Show ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: ScopeCopyInfo -> () #

Eq ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

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

Renaming (generic).

type Assign = FieldAssignment' Expr Source #

Record field assignment f = e.

data Expr Source #

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

Constructors

Var Name

Bound variable.

Def' QName Suffix

Constant: axiom, function, data or record type, with a possible suffix.

Proj ProjOrigin AmbiguousQName

Projection (overloaded).

Con AmbiguousQName

Constructor (overloaded).

PatternSyn AmbiguousQName

Pattern synonym.

Macro QName

Macro.

Lit ExprInfo Literal

Literal.

QuestionMark MetaInfo InteractionId

Meta variable for interaction. The InteractionId is usually identical with the metaNumber of MetaInfo. However, if you want to print an interaction meta as just ? instead of ?n, you should set the metaNumber to Nothing while keeping the InteractionId.

Underscore MetaInfo

Meta variable for hidden argument (must be inferred locally).

Dot ExprInfo Expr

.e, for postfix projection.

App AppInfo Expr (NamedArg Expr)

Ordinary (binary) application.

WithApp ExprInfo Expr [Expr]

With application.

Lam ExprInfo LamBinding Expr

λ bs → e.

AbsurdLam ExprInfo Hiding

λ() or λ{}.

ExtendedLam ExprInfo DefInfo Erased QName (List1 Clause) 
Pi ExprInfo Telescope1 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

Instances details
SubstExpr Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

IsProjP Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

MapNamedArgPattern NAP Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #

ExprLike Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Underscore Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: Expr -> Range Source #

KillRange Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Expr Source #

ToConcrete LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHSCore Source #

ToConcrete Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Pattern Source #

Reify Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Expr Source #

PrettyTCM Expr Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

IsFlexiblePattern Pattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS

Data Expr Source # 
Instance details

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 #

Generic Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep Expr :: Type -> Type #

Methods

from :: Expr -> Rep Expr x #

to :: Rep Expr x -> Expr #

Show Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> Expr -> ShowS #

show :: Expr -> String #

showList :: [Expr] -> ShowS #

NFData Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: Expr -> () #

Eq Expr Source #

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

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

ToConcrete (Maybe Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe Pattern) Source #

PrettyTCM (Arg Expr) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (NamedArg Expr) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

ToAbstract (Expr, Elim) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elim) Source #

ToAbstract (Expr, Elims) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elims) Source #

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

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

type ConOfAbs Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ReifiesTo Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type Rep Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep Expr = D1 ('MetaData "Expr" "Agda.Syntax.Abstract" "Agda-2.6.2.1-inplace" 'False) ((((C1 ('MetaCons "Var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: (C1 ('MetaCons "Def'" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Suffix)) :+: C1 ('MetaCons "Proj" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProjOrigin) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)))) :+: (C1 ('MetaCons "Con" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)) :+: (C1 ('MetaCons "PatternSyn" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)) :+: C1 ('MetaCons "Macro" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))))) :+: ((C1 ('MetaCons "Lit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: (C1 ('MetaCons "QuestionMark" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InteractionId)) :+: C1 ('MetaCons "Underscore" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaInfo)))) :+: ((C1 ('MetaCons "Dot" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "App" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AppInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg Expr))))) :+: (C1 ('MetaCons "WithApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Expr]))) :+: C1 ('MetaCons "Lam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LamBinding) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))))) :+: (((C1 ('MetaCons "AbsurdLam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Hiding)) :+: (C1 ('MetaCons "ExtendedLam" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 Clause))))) :+: C1 ('MetaCons "Pi" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope1) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 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 (Maybe Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type AbsOfRef (Expr, Elim) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Expr, Elims) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

newtype BindName Source #

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

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

Constructors

BindName 

Fields

Instances

Instances details
ExprLike BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

HasRange BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

SetRange BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete BindName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs BindName Source #

EmbPrj BindName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Data BindName Source # 
Instance details

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 #

Show BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

NFData BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: BindName -> () #

Eq BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

Ord BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete (Maybe BindName) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe BindName) Source #

(ToConcrete p, ToConcrete a) => ToConcrete (RewriteEqn' qn BindName p a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

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

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

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

type ConOfAbs BindName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Maybe BindName) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

pattern Def :: QName -> Expr Source #

Pattern synonym for regular Def

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

Smart constructor for Generalized

axiomName :: Declaration -> QName Source #

The name defined by the given axiom.

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

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

Orphan instances

KillRange Suffix Source # 
Instance details