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

Agda.Syntax.Abstract

Description

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

Synopsis

Documentation

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 Name Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

SubstExpr ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract

SubstExpr Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

Defined in Agda.Syntax.Abstract

Methods

substExpr :: [(Name, Expr)] -> [a] -> [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 (List1 a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

substExpr :: [(Name, Expr)] -> List1 a -> List1 a 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 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 #

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 #

class NameToExpr a where Source #

Turn a name into an expression.

Methods

nameToExpr :: a -> Expr Source #

Instances

Instances details
NameToExpr ResolvedName Source #

Turn a ResolvedName into an expression.

Assumes name is not UnknownName.

Instance details

Defined in Agda.Syntax.Abstract

NameToExpr AbstractName Source #

Turn an AbstractName into an expression.

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

Methods

anyAbstract :: Declaration -> Bool Source #

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
Functor Pattern' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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)

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

Methods

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

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

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

Defined in Agda.Syntax.Abstract

Methods

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

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

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)

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

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

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

Defined in Agda.Syntax.Abstract

Methods

rnf :: Pattern' e -> ()

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 #

HasRange (Pattern' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: Pattern' e -> Range Source #

IsProjP (Pattern' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

IsWithP (Pattern' e) Source #

Check for with-pattern.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

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

Defined in Agda.Syntax.Abstract.Views

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 #

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

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: Pattern' a -> S Int32 Source #

icod_ :: Pattern' a -> S Int32 Source #

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

NamesIn (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

ToConcrete (Maybe Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe Pattern) Source #

Methods

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

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

ExpandPatternSynonyms (Pattern' e) Source # 
Instance details

Defined in Agda.TypeChecking.Patterns.Abstract

ToAbstract (Pattern' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Pattern' Expr) 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 Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (((C1 ('MetaCons "VarP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName)) :+: (C1 ('MetaCons "ConP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConPatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NAPs e)))) :+: C1 ('MetaCons "ProjP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProjOrigin) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName))))) :+: ((C1 ('MetaCons "DefP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NAPs e)))) :+: C1 ('MetaCons "WildP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo))) :+: (C1 ('MetaCons "AsP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' e)))) :+: C1 ('MetaCons "DotP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 e))))) :+: ((C1 ('MetaCons "AbsurdP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo)) :+: (C1 ('MetaCons "LitP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: C1 ('MetaCons "PatternSynP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NAPs e)))))) :+: ((C1 ('MetaCons "RecP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FieldAssignment' (Pattern' e)])) :+: C1 ('MetaCons "EqualP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(e, e)]))) :+: (C1 ('MetaCons "WithP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' e))) :+: C1 ('MetaCons "AnnP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 e) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' e))))))))
type ADotT (Pattern' a) 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 ConOfAbs (Maybe Pattern) = Maybe Pattern
type AbsOfCon (Pattern' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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
Functor LHSCore' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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)

ToConcrete LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHSCore Source #

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

Defined in Agda.Syntax.Abstract

Methods

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

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

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)

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

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

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

Defined in Agda.Syntax.Abstract

Methods

rnf :: LHSCore' e -> ()

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

Defined in Agda.Syntax.Abstract

HasRange (LHSCore' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: LHSCore' e -> Range Source #

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

Defined in Agda.Syntax.Abstract.Views

ToAbstract (LHSCore' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (LHSCore' Expr) Source #

type ConOfAbs LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type Rep (LHSCore' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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
Eq LHS Source #

Ignore Range when comparing LHSs.

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

Show LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> LHS -> ShowS

show :: LHS -> String

showList :: [LHS] -> ShowS

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

NFData LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: LHS -> ()

KillRange LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: LHS -> Range Source #

DeclaredNames Clause Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ToConcrete LHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHS Source #

LHSToSpine LHS SpineLHS Source #

LHS instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

LHSToSpine Clause SpineClause Source #

Clause instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

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-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "LHS" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSInfo) :*: S1 ('MetaSel ('Just "lhsCore") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSCore)))
type ConOfAbs LHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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
Eq SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

Show SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> SpineLHS -> ShowS

show :: SpineLHS -> String

showList :: [SpineLHS] -> ShowS

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

NFData SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: SpineLHS -> ()

KillRange SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

ExprLike SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ToConcrete SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs SpineLHS Source #

LHSToSpine LHS SpineLHS Source #

LHS instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

LHSToSpine Clause SpineClause Source #

Clause instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

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-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "SpineLHS" 'PrefixI 'True) (S1 ('MetaSel ('Just "spLhsInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSInfo) :*: (S1 ('MetaSel ('Just "spLhsDefName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "spLhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg Pattern]))))
type ConOfAbs SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

data RHS Source #

Constructors

RHS 

Fields

  • rhsExpr :: Expr
     
  • rhsConcrete :: Maybe Expr

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

AbsurdRHS 
WithRHS QName [WithExpr] [Clause]

The QName is the name of the with function.

RewriteRHS 

Fields

Instances

Instances details
Eq RHS Source #

Ignore rhsConcrete when comparing RHSs.

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

Show RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> RHS -> ShowS

show :: RHS -> String

showList :: [RHS] -> ShowS

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

NFData RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: RHS -> ()

KillRange RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: RHS -> Range Source #

DeclaredNames RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ToConcrete RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RHS Source #

type Rep RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

data WhereDeclarations Source #

Constructors

WhereDecls 

Fields

Instances

Instances details
Eq 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

Show WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> WhereDeclarations -> ShowS

show :: WhereDeclarations -> String

showList :: [WhereDeclarations] -> ShowS

Generic WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep WhereDeclarations :: Type -> Type

NFData WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: WhereDeclarations -> ()

Null WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

DeclaredNames WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ToConcrete WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs WhereDeclarations Source #

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-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "WhereDecls" 'PrefixI 'True) (S1 ('MetaSel ('Just "whereModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModuleName)) :*: S1 ('MetaSel ('Just "whereDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Declaration))))
type ConOfAbs WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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
Functor Clause' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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)

DeclaredNames Clause Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

LHSToSpine Clause SpineClause Source #

Clause instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

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

Defined in Agda.Syntax.Abstract

Methods

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

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

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)

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

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

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

Defined in Agda.Syntax.Abstract

Methods

rnf :: Clause' lhs -> ()

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

Defined in Agda.Syntax.Abstract

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

Defined in Agda.Syntax.Abstract

Methods

getRange :: Clause' a -> Range Source #

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

Defined in Agda.Syntax.Abstract.Views

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Clause' a) Source #

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-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "Clause" 'PrefixI 'True) ((S1 ('MetaSel ('Just "clauseLHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 lhs) :*: S1 ('MetaSel ('Just "clauseStrippedPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ProblemEq])) :*: (S1 ('MetaSel ('Just "clauseRHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RHS) :*: (S1 ('MetaSel ('Just "clauseWhereDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhereDeclarations) :*: S1 ('MetaSel ('Just "clauseCatchall") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))
type ConOfAbs (Clause' a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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
Eq ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

Show ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> ProblemEq -> ShowS

show :: ProblemEq -> String

showList :: [ProblemEq] -> ShowS

Generic ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep ProblemEq :: Type -> Type

Methods

from :: ProblemEq -> Rep ProblemEq x

to :: Rep ProblemEq x -> ProblemEq

NFData ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: ProblemEq -> ()

KillRange ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

Subst ProblemEq Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg ProblemEq Source #

PrettyTCM ProblemEq Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

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-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "ProblemEq" 'PrefixI 'True) (S1 ('MetaSel ('Just "problemInPat") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern) :*: (S1 ('MetaSel ('Just "problemInst") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :*: S1 ('MetaSel ('Just "problemType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Dom Type)))))
type SubstArg ProblemEq Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

data DataDefParams Source #

Constructors

DataDefParams 

Fields

Instances

Instances details
Eq 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

Show DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> DataDefParams -> ShowS

show :: DataDefParams -> String

showList :: [DataDefParams] -> ShowS

Generic DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep DataDefParams :: Type -> Type

NFData DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: DataDefParams -> ()

KillRange DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

ExprLike DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

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-LvHTW8pd3Vr2rIoKv0Upjq" '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
Eq 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

Show GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> GeneralizeTelescope -> ShowS

show :: GeneralizeTelescope -> String

showList :: [GeneralizeTelescope] -> ShowS

Generic GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep GeneralizeTelescope :: Type -> Type

NFData GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: GeneralizeTelescope -> ()

KillRange GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

ExprLike GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

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-LvHTW8pd3Vr2rIoKv0Upjq" '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
Eq TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

Show TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> TypedBinding -> ShowS

show :: TypedBinding -> String

showList :: [TypedBinding] -> ShowS

Generic TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep TypedBinding :: Type -> Type

NFData TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: TypedBinding -> ()

KillRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

LensHiding TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

ExprLike TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

PrettyTCM TypedBinding Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

ToConcrete TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs TypedBinding Source #

type Rep TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

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
Eq LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

Show LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> LamBinding -> ShowS

show :: LamBinding -> String

showList :: [LamBinding] -> ShowS

Generic LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep LamBinding :: Type -> Type

Methods

from :: LamBinding -> Rep LamBinding x

to :: Rep LamBinding x -> LamBinding

NFData LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: LamBinding -> ()

KillRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

LensHiding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

ExprLike LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ToConcrete LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LamBinding Source #

type Rep LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

data Binder' a Source #

Constructors

Binder 

Fields

Instances

Instances details
Functor Binder' Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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)

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

Defined in Agda.Syntax.Abstract

Methods

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

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

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)

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

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

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

Defined in Agda.Syntax.Abstract

Methods

rnf :: Binder' a -> ()

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

Defined in Agda.Syntax.Abstract

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

Defined in Agda.Syntax.Abstract

Methods

getRange :: Binder' a -> Range Source #

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Binder' a) Source #

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-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "Binder" 'PrefixI 'True) (S1 ('MetaSel ('Just "binderPattern") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Pattern)) :*: S1 ('MetaSel ('Just "binderName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))
type ConOfAbs (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type TacticAttr = Maybe Expr Source #

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
Eq LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

Show LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> LetBinding -> ShowS

show :: LetBinding -> String

showList :: [LetBinding] -> ShowS

Generic LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep LetBinding :: Type -> Type

Methods

from :: LetBinding -> Rep LetBinding x

to :: Rep LetBinding x -> LetBinding

NFData LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: LetBinding -> ()

KillRange LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

ExprLike LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ToConcrete LetBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LetBinding Source #

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-LvHTW8pd3Vr2rIoKv0Upjq" 'False) ((C1 ('MetaCons "LetBind" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LetInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: C1 ('MetaCons "LetPatBind" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LetInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: (C1 ('MetaCons "LetApply" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleApplication) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeCopyInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective)))) :+: (C1 ('MetaCons "LetOpen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))) :+: C1 ('MetaCons "LetDeclaredVariable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName)))))
type ConOfAbs LetBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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
Eq Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

Show Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> Pragma -> ShowS

show :: Pragma -> String

showList :: [Pragma] -> ShowS

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

NFData Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: Pragma -> ()

DeclaredNames Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

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-LvHTW8pd3Vr2rIoKv0Upjq" '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
Eq ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

Show ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> ModuleApplication -> ShowS

show :: ModuleApplication -> String

showList :: [ModuleApplication] -> ShowS

Generic ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep ModuleApplication :: Type -> Type

NFData ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: ModuleApplication -> ()

KillRange ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

ExprLike ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ToConcrete ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ModuleApplication Source #

type Rep ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

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
Eq Declaration Source #

Does not compare ScopeInfo fields.

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

Show Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> Declaration -> ShowS

show :: Declaration -> String

showList :: [Declaration] -> ShowS

Generic Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep Declaration :: Type -> Type

Methods

from :: Declaration -> Rep Declaration x

to :: Rep Declaration x -> Declaration

NFData Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: Declaration -> ()

KillRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

AnyAbstract Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

anyAbstract :: Declaration -> Bool Source #

DeclaredNames Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ExprLike Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

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

Methods

showHead :: Declaration -> String Source #

ToConcrete (Constr Constructor) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Constr Constructor) Source #

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-LvHTW8pd3Vr2rIoKv0Upjq" 'False) ((((C1 ('MetaCons "Axiom" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe [Occurrence])) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: C1 ('MetaCons "Generalize" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set QName)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))) :+: (C1 ('MetaCons "Field" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Expr)))) :+: C1 ('MetaCons "Primitive" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Expr)))))) :+: ((C1 ('MetaCons "Mutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MutualInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])) :+: C1 ('MetaCons "Section" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralizeTelescope) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])))) :+: (C1 ('MetaCons "Apply" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleApplication) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeCopyInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective)))) :+: (C1 ('MetaCons "Import" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))) :+: C1 ('MetaCons "Pragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pragma)))))) :+: (((C1 ('MetaCons "Open" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))) :+: C1 ('MetaCons "FunDef" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Delayed) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause])))) :+: (C1 ('MetaCons "DataSig" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralizeTelescope) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: (C1 ('MetaCons "DataDef" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataDefParams) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Constructor])))) :+: C1 ('MetaCons "RecSig" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralizeTelescope) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))))) :+: ((C1 ('MetaCons "RecDef" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck))) :*: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RecordDirectives) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataDefParams)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])))) :+: C1 ('MetaCons "PatternSynDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Arg BindName]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' Void))))) :+: (C1 ('MetaCons "UnquoteDecl" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MutualInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefInfo])) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: (C1 ('MetaCons "UnquoteDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefInfo]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: C1 ('MetaCons "ScopedDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])))))))
type ConOfAbs Declaration Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Constr Constructor) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

data ScopeCopyInfo Source #

Instances

Instances details
Eq 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

Show ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> ScopeCopyInfo -> ShowS

show :: ScopeCopyInfo -> String

showList :: [ScopeCopyInfo] -> ShowS

Generic ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep ScopeCopyInfo :: Type -> Type

NFData ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: ScopeCopyInfo -> ()

Pretty ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange 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-LvHTW8pd3Vr2rIoKv0Upjq" '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
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

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

Show Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> Expr -> ShowS

show :: Expr -> String

showList :: [Expr] -> ShowS

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

NFData Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: Expr -> ()

KillRange Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

getRange :: Expr -> Range Source #

Underscore Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

IsProjP Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

SubstExpr Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

ExprLike Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

MapNamedArgPattern NAP Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

PrettyTCM Expr Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

ToConcrete Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Pattern Source #

ToConcrete LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHSCore Source #

ToConcrete Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Expr Source #

Reify Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Expr Source #

Methods

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

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

IsFlexiblePattern Pattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS

Methods

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

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

PrettyTCM (NamedArg Expr) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Arg Expr) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

ToConcrete (Maybe Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe Pattern) Source #

Methods

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

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

ToAbstract (Expr, Elims) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elims) Source #

ToAbstract (Expr, Elim) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elim) 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 Rep Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ReifiesTo Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ConOfAbs (Maybe Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Maybe Pattern) = Maybe Pattern
type AbsOfRef (Expr, Elims) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Expr, Elim) 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
Eq BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

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

Ord BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

compare :: BindName -> BindName -> Ordering

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

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

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

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

max :: BindName -> BindName -> BindName

min :: BindName -> BindName -> BindName

Show BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> BindName -> ShowS

show :: BindName -> String

showList :: [BindName] -> ShowS

NFData BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: BindName -> ()

KillRange BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

SetRange BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

ExprLike BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

EmbPrj BindName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: BindName -> S Int32 Source #

icod_ :: BindName -> S Int32 Source #

value :: Int32 -> R BindName Source #

ToConcrete BindName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs BindName Source #

ToConcrete (Maybe BindName) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe BindName) Source #

Methods

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

bindToConcrete :: Maybe BindName -> (ConOfAbs (Maybe BindName) -> AbsToCon b) -> AbsToCon b 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 (Maybe BindName) = Maybe Name
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