Agda-2.6.1.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

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

| p, for with-patterns.

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 #

IsFlexiblePattern Pattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS

UniverseBi Declaration Pattern Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete Pattern Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToAbstract HoleContent HoleContent Source #

Content of interaction hole.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

UniverseBi Declaration (NamedArg Pattern) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (Pattern' Void) Source # 
Instance details

Defined in Agda.Syntax.Abstract

APatternLike a (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

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

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

ToAbstract Pattern (Pattern' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract Pattern (Names, Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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 #

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

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Pattern' a -> m (Pattern' a) Source #

foldExpr :: Monoid m => (Expr -> m) -> Pattern' a -> m Source #

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Pattern' a -> m (Pattern' a) Source #

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

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

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

NamesIn (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Pattern' a -> Set QName Source #

ExpandPatternSynonyms (Pattern' e) Source # 
Instance details

Defined in Agda.TypeChecking.Patterns.Abstract

ToConcrete (Maybe Pattern) (Maybe Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

UniverseBi Declaration (NamedArg LHSCore) Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToAbstract LHSCore (LHSCore' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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 #

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

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LHSCore' a -> m (LHSCore' a) Source #

foldExpr :: Monoid m => (Expr -> m) -> LHSCore' a -> m Source #

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> LHSCore' a -> m (LHSCore' a) Source #

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

ToAbstract (LHSCore' Expr) (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 #

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 #

AllNames Clause Source # 
Instance details

Defined in Agda.Syntax.Abstract

ExprLike LHS Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LHS -> m LHS Source #

foldExpr :: Monoid m => (Expr -> m) -> LHS -> m Source #

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> LHS -> m LHS Source #

mapExpr :: (Expr -> Expr) -> LHS -> 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

ToConcrete LHS LHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Reify NamedClause Clause Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

ToAbstract Clause Clause Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract (QNamed Clause) Clause Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Reify (QNamed Clause) Clause Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

ToAbstract [QNamed Clause] [Clause] Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Reify (QNamed System) [Clause] Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

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

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

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

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> SpineLHS -> m SpineLHS Source #

foldExpr :: Monoid m => (Expr -> m) -> SpineLHS -> m Source #

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> SpineLHS -> m SpineLHS Source #

mapExpr :: (Expr -> Expr) -> SpineLHS -> 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

ToConcrete SpineLHS LHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

data RHS Source #

Constructors

RHS 

Fields

AbsurdRHS 
WithRHS QName [WithHiding Expr] [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 #

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 #

AllNames RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

allNames :: RHS -> Seq QName Source #

ExprLike RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> RHS -> m RHS Source #

foldExpr :: Monoid m => (Expr -> m) -> RHS -> m Source #

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> RHS -> m RHS Source #

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

ToAbstract AbstractRHS RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToConcrete RHS (RHS, [RewriteEqn], [WithHiding Expr], [Declaration]) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

data WhereDeclarations Source #

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

KillRange WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

AllNames WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

ExprLike WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ToConcrete WhereDeclarations WhereClause 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) #

AllNames Clause Source # 
Instance details

Defined in Agda.Syntax.Abstract

LHSToSpine Clause SpineClause Source #

Clause instance.

Instance details

Defined in Agda.Syntax.Abstract.Pattern

Reify NamedClause Clause Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

ToAbstract Clause Clause Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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 #

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

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Clause' a -> m (Clause' a) Source #

foldExpr :: Monoid m => (Expr -> m) -> Clause' a -> m Source #

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Clause' a -> m (Clause' a) Source #

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

ToAbstract (QNamed Clause) Clause Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Reify (QNamed Clause) Clause Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

ToConcrete a LHS => ToConcrete (Clause' a) [Declaration] Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToAbstract [QNamed Clause] [Clause] Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Reify (QNamed System) [Clause] Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

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.

Instances

Instances details
Eq ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

KillRange ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

PrettyTCM ProblemEq Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Subst Term 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

KillRange DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

ExprLike DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

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

KillRange GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

ExprLike GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

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 [NamedArg Binder] Expr

As in telescope (x y z : A) or type (x y z : A) -> B.

TLet Range [LetBinding]

E.g. (let x = e) or (let open M).

Instances

Instances details
Eq TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

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

SubstExpr TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

AllNames 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

UniverseBi Declaration TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete TypedBinding TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Reify Telescope Telescope Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

ToAbstract TypedBinding TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

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

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

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

AllNames LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

ExprLike LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

UniverseBi Declaration LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete LamBinding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToAbstract LamBinding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data Binder' a Source #

Constructors

Binder 

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 #

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 #

ToAbstract (Binder' (NewName BoundName)) Binder Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

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

KillRange LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

SubstExpr LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

AllNames LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

ExprLike LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

UniverseBi Declaration LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete LetBinding [Declaration] Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToAbstract ModuleAssignment (ModuleName, [LetBinding]) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

ExprLike Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Pragma -> m Pragma Source #

foldExpr :: Monoid m => (Expr -> m) -> Pragma -> m Source #

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Pragma -> m Pragma Source #

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

ToAbstract Pragma [Pragma] Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

KillRange ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

AllNames ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

ExprLike ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ToConcrete ModuleApplication ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

data Declaration Source #

Constructors

Axiom Axiom 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 Expr

primitive function

Mutual MutualInfo [Declaration]

a bunch of mutually recursive definitions

Section ModuleInfo 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]

the LamBindings are DomainFree and bind the parameters of the datatype.

RecSig DefInfo QName GeneralizeTelescope Expr

lone record signature

RecDef DefInfo QName UniverseCheck (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe QName) DataDefParams Expr [Declaration]

The LamBindings are DomainFree and bind the parameters of the datatype. The Expr gives the constructor type telescope, (x1 : A1)..(xn : An) -> Prop, and the optional name is the constructor's name.

PatternSynDef QName [Arg Name] (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

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

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

AllNames Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

ExprLike Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

ShowHead Declaration Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Decl

UniverseBi Declaration Quantity Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration QName Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration Pattern Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

universeBi :: Declaration -> [Expr]

ToAbstract NiceDeclaration Declaration Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

UniverseBi Declaration (NamedArg Pattern) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg LHSCore) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg Expr) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg BindName) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (Pattern' Void) Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete Declaration [Declaration] Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete (Constr Constructor) Declaration Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToAbstract [Declaration] [Declaration] Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Pretty ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Ren a = [(a, a)] Source #

Renaming (generic).

data Axiom Source #

Is a type signature a postulate or a function signature?

Constructors

FunSig

A function signature.

NoFunSig

Not a function signature, i.e., a postulate (in user input) or another (e.g. data/record) type signature (internally).

Instances

Instances details
Eq Axiom Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

Data Axiom 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) -> Axiom -> c Axiom #

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

toConstr :: Axiom -> Constr #

dataTypeOf :: Axiom -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> Axiom -> Axiom #

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

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

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

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

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

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

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

Ord Axiom Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

compare :: Axiom -> Axiom -> Ordering #

(<) :: Axiom -> Axiom -> Bool #

(<=) :: Axiom -> Axiom -> Bool #

(>) :: Axiom -> Axiom -> Bool #

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

max :: Axiom -> Axiom -> Axiom #

min :: Axiom -> Axiom -> Axiom #

Show Axiom Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> Axiom -> ShowS #

show :: Axiom -> String #

showList :: [Axiom] -> ShowS #

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

Constant: axiom, function, data or record type.

Proj ProjOrigin AmbiguousQName

Projection (overloaded).

Con AmbiguousQName

Constructor (overloaded).

PatternSyn AmbiguousQName

Pattern synonym.

Macro QName

Macro.

Lit 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 QName [Clause] 
Pi ExprInfo Telescope 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.

Set ExprInfo Integer

Set, Set1, Set2, ...

Prop ExprInfo Integer

Prop, Prop1, Prop2, ...

Let ExprInfo [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 ...

Tactic ExprInfo Expr [NamedArg Expr]
tactic e x1 .. xn
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 #

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

Defined in Agda.Syntax.Abstract

Methods

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

SubstExpr Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

AllNames Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

allNames :: Expr -> Seq QName Source #

ExprLike Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Expr -> m Expr Source #

foldExpr :: Monoid m => (Expr -> m) -> Expr -> m Source #

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Expr -> m Expr Source #

mapExpr :: (Expr -> Expr) -> Expr -> Expr Source #

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 #

IsFlexiblePattern Pattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS

UniverseBi Declaration Pattern Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

universeBi :: Declaration -> [Expr]

ToConcrete Pattern Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete LHSCore Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete Expr Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToAbstract Literal Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract Sort Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract Term Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Reify MetaId Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Reify Literal Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Reify Level Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Level -> m Expr Source #

reifyWhen :: MonadReify m => Bool -> Level -> m Expr Source #

Reify Sort Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Sort -> m Expr Source #

reifyWhen :: MonadReify m => Bool -> Sort -> m Expr Source #

Reify Type Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Type -> m Expr Source #

reifyWhen :: MonadReify m => Bool -> Type -> m Expr Source #

Reify Term Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Term -> m Expr Source #

reifyWhen :: MonadReify m => Bool -> Term -> m Expr Source #

Reify Expr Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Expr -> m Expr Source #

reifyWhen :: MonadReify m => Bool -> Expr -> m Expr Source #

Reify DisplayTerm Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

ToAbstract HoleContent HoleContent Source #

Content of interaction hole.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract Expr Expr Source #

Scope check an expression.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract OldQName Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

UniverseBi Declaration (NamedArg Pattern) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg LHSCore) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (NamedArg Expr) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Reify ProblemConstraint (Closure (OutputForm Expr Expr)) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

ToAbstract Pattern (Names, Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Reify Constraint (OutputConstraint Expr Expr) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToConcrete (Maybe Pattern) (Maybe Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToAbstract [Arg Term] [NamedArg Expr] Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract (LHSCore' Expr) (LHSCore' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract (Expr, Elims) Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract (Expr, Elim) Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract (RewriteEqn' () Pattern Expr) RewriteEqn 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

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

Show BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

KillRange BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

SetRange BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

EmbPrj BindName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

ToConcrete BindName BoundName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

UniverseBi Declaration (NamedArg BindName) Source # 
Instance details

Defined in Agda.Syntax.Abstract

ToAbstract (Binder' (NewName BoundName)) Binder Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract (NewName BoundName) BindName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Smart constructor for Generalized

class SubstExpr a where Source #

Methods

substExpr :: [(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 TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

SubstExpr LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

SubstExpr Assign Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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 (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

Defined in Agda.Syntax.Abstract

Methods

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

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

Defined in Agda.Syntax.Abstract

Methods

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

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

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

Defined in Agda.Syntax.Abstract

Methods

anyAbstract :: [a] -> Bool Source #

class AllNames a where Source #

Extracts all the names which are declared in a Declaration. This does not include open public or let expressions, but it does include local modules, where clauses and the names of extended lambdas.

Methods

allNames :: a -> Seq QName Source #

Instances

Instances details
AllNames QName Source # 
Instance details

Defined in Agda.Syntax.Abstract

AllNames RHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

allNames :: RHS -> Seq QName Source #

AllNames Clause Source # 
Instance details

Defined in Agda.Syntax.Abstract

AllNames WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

AllNames TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

AllNames LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

AllNames LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

AllNames ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

AllNames Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

AllNames Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

allNames :: Expr -> Seq QName Source #

AllNames CallInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

AllNames CallPath Source # 
Instance details

Defined in Agda.Termination.Monad

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

Defined in Agda.Syntax.Abstract

Methods

allNames :: [a] -> Seq QName Source #

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

Defined in Agda.Syntax.Abstract

Methods

allNames :: Maybe a -> Seq QName Source #

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

Defined in Agda.Syntax.Abstract

Methods

allNames :: Arg a -> Seq QName Source #

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

Defined in Agda.Syntax.Abstract

Methods

allNames :: (a, b) -> Seq QName Source #

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

Defined in Agda.Syntax.Abstract

Methods

allNames :: Named name a -> Seq QName Source #

(AllNames a, AllNames b, AllNames c) => AllNames (a, b, c) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

allNames :: (a, b, c) -> Seq QName Source #

(AllNames qn, AllNames e) => AllNames (RewriteEqn' qn p e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

allNames :: RewriteEqn' qn p e -> Seq QName Source #

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 #

class IsNoName a where Source #

Check whether a name is the empty name "_".

Minimal complete definition

Nothing

Methods

isNoName :: a -> Bool Source #

default isNoName :: (Foldable t, IsNoName b, t b ~ a) => a -> Bool Source #

Instances

Instances details
IsNoName String Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: String -> Bool Source #

IsNoName ByteString Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

IsNoName QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: QName -> Bool Source #

IsNoName Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: Name -> Bool Source #

IsNoName Name Source #

An abstract name is empty if its concrete name is empty.

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

isNoName :: Name -> Bool Source #

IsNoName a => IsNoName (Ranged a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

isNoName :: Ranged a -> Bool Source #

IsNoName a => IsNoName (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

class MkName a where Source #

Make a Name from some kind of string.

Minimal complete definition

mkName

Methods

mkName :: Range -> NameId -> a -> Name Source #

The Range sets the definition site of the name, not the use site.

mkName_ :: NameId -> a -> Name Source #

Instances

Instances details
MkName String Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

class IsProjP a where Source #

Check whether we are a projection pattern.

Instances

Instances details
IsProjP Void Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

IsProjP Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

Defined in Agda.Syntax.Abstract.Name

IsProjP (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

IsProjP (Pattern' e) Source # 
Instance details

Defined in Agda.Syntax.Abstract

IsProjP a => IsProjP (Named n a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

newtype AmbiguousQName Source #

Ambiguous qualified names. Used for overloaded constructors.

Invariant: All the names in the list must have the same concrete, unqualified name. (This implies that they all have the same Range).

Constructors

AmbQ 

Fields

Instances

Instances details
Eq AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Data AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

toConstr :: AmbiguousQName -> Constr #

dataTypeOf :: AmbiguousQName -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> AmbiguousQName -> AmbiguousQName #

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

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

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

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

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

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

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

Ord AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Show AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Pretty AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

KillRange AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

HasRange AmbiguousQName Source #

The range of an AmbiguousQName is the range of any of its disambiguations (they are the same concrete name).

Instance details

Defined in Agda.Syntax.Abstract.Name

NumHoles AmbiguousQName Source #

We can have an instance for ambiguous names as all share a common concrete name.

Instance details

Defined in Agda.Syntax.Abstract.Name

EmbPrj AmbiguousQName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

NamesIn AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

UniverseBi Declaration AmbiguousQName 
Instance details

Defined in Agda.Syntax.Abstract

newtype ModuleName Source #

A module name is just a qualified name.

The SetRange instance for module names sets all individual ranges to the given one.

Constructors

MName 

Fields

Instances

Instances details
Eq ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Data ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

toConstr :: ModuleName -> Constr #

dataTypeOf :: ModuleName -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> ModuleName -> ModuleName #

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

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

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

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

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

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

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

Ord ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Show ModuleName Source #

Only use this show function in debugging! To convert an abstract ModuleName into a string use prettyShow.

Instance details

Defined in Agda.Syntax.Abstract.Name

NFData ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: ModuleName -> () #

Sized ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

size :: ModuleName -> Int Source #

Pretty ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

KillRange ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

KillRange Sections Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

SetRange ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

HasRange ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

SetBindingSite ModuleName Source #

Sets the binding site of all names in the path.

Instance details

Defined in Agda.Syntax.Scope.Base

SubstExpr ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract

ExprLike ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

EmbPrj ModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

PrettyTCM ModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

InstantiateFull ModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

UniverseBi Declaration ModuleName 
Instance details

Defined in Agda.Syntax.Abstract

ToConcrete ModuleName QName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToAbstract OldModuleName ModuleName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract NewModuleQName ModuleName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract NewModuleName ModuleName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract ModuleAssignment (ModuleName, [LetBinding]) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data QNamed a Source #

Something preceeded by a qualified name.

Constructors

QNamed 

Fields

Instances

Instances details
Functor QNamed Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

fmap :: (a -> b) -> QNamed a -> QNamed b #

(<$) :: a -> QNamed b -> QNamed a #

Foldable QNamed Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

fold :: Monoid m => QNamed m -> m #

foldMap :: Monoid m => (a -> m) -> QNamed a -> m #

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

foldr :: (a -> b -> b) -> b -> QNamed a -> b #

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

foldl :: (b -> a -> b) -> b -> QNamed a -> b #

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

foldr1 :: (a -> a -> a) -> QNamed a -> a #

foldl1 :: (a -> a -> a) -> QNamed a -> a #

toList :: QNamed a -> [a] #

null :: QNamed a -> Bool #

length :: QNamed a -> Int #

elem :: Eq a => a -> QNamed a -> Bool #

maximum :: Ord a => QNamed a -> a #

minimum :: Ord a => QNamed a -> a #

sum :: Num a => QNamed a -> a #

product :: Num a => QNamed a -> a #

Traversable QNamed Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

sequenceA :: Applicative f => QNamed (f a) -> f (QNamed a) #

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

sequence :: Monad m => QNamed (m a) -> m (QNamed a) #

Show a => Show (QNamed a) Source #

Use prettyShow to print names to the user.

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> QNamed a -> ShowS #

show :: QNamed a -> String #

showList :: [QNamed a] -> ShowS #

Pretty a => Pretty (QNamed a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

PrettyTCM (QNamed Clause) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

ToAbstract (QNamed Clause) Clause Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Reify (QNamed Clause) Clause Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

ToAbstract [QNamed Clause] [Clause] Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Reify (QNamed System) [Clause] Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

data QName Source #

Qualified names are non-empty lists of names. Equality on qualified names are just equality on the last name, i.e. the module part is just for show.

The SetRange instance for qualified names sets all individual ranges (including those of the module prefix) to the given one.

Constructors

QName 

Instances

Instances details
Eq QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

Data QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

toConstr :: QName -> Constr #

dataTypeOf :: QName -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> QName -> QName #

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

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

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

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

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

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

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

Ord QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

compare :: QName -> QName -> Ordering #

(<) :: QName -> QName -> Bool #

(<=) :: QName -> QName -> Bool #

(>) :: QName -> QName -> Bool #

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

max :: QName -> QName -> QName #

min :: QName -> QName -> QName #

Show QName Source #

Only use this show function in debugging! To convert an abstract QName into a string use prettyShow.

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> QName -> ShowS #

show :: QName -> String #

showList :: [QName] -> ShowS #

NFData QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: QName -> () #

Hashable QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

hashWithSalt :: Int -> QName -> Int

hash :: QName -> Int

Sized QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

size :: QName -> Int Source #

Pretty QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

KillRange QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

KillRange RewriteRuleMap Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Definitions Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

SetRange QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

setRange :: Range -> QName -> QName Source #

HasRange QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: QName -> Range Source #

LensFixity' QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

LensFixity QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

LensInScope QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

NumHoles QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

numHoles :: QName -> Int Source #

SetBindingSite QName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

TermLike QName Source # 
Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> QName -> m QName Source #

foldTerm :: Monoid m => (Term -> m) -> QName -> m Source #

AllNames QName Source # 
Instance details

Defined in Agda.Syntax.Abstract

ExprLike QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> QName -> m QName Source #

foldExpr :: Monoid m => (Expr -> m) -> QName -> m Source #

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> QName -> m QName Source #

mapExpr :: (Expr -> Expr) -> QName -> QName Source #

EmbPrj QName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

PrettyTCM QName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

NamesIn QName Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: QName -> Set QName Source #

InstantiateFull QName Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

FromTerm QName Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm QName Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimTerm QName Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: QName -> TCM Term Source #

Occurs QName Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Unquote QName Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

UniverseBi Declaration QName 
Instance details

Defined in Agda.Syntax.Abstract

Subst Term QName Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.Class

ToConcrete QName QName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #

Conversion TOM Type (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (MExp O) Source #

Conversion TOM Term (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Term -> TOM (MExp O) Source #

Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) Source #

Conversion MOT (Exp O) Type Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Type Source #

Conversion MOT (Exp O) Term Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Term Source #

Conversion TOM [Clause] [([Pat O], MExp O)] Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: [Clause] -> TOM [([Pat O], MExp O)] Source #

Conversion TOM (Arg Pattern) (Pat O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Arg Pattern -> TOM (Pat O) Source #

Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: MM a (RefInfo O) -> MOT b Source #

(Show a, ToQName a) => ToAbstract (OldName a) QName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToConcrete (Maybe QName) (Maybe Name) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data Name Source #

A name is a unique identifier and a suggestion for a concrete name. The concrete name contains the source location (if any) of the name. The source location of the binding site is also recorded.

Constructors

Name 

Fields

Instances

Instances details
Eq Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

Data Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

toConstr :: Name -> Constr #

dataTypeOf :: Name -> DataType #

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

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

gmapT :: (forall b. Data b => b -> b) -> Name -> Name #

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

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

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

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

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

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

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

Ord Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

compare :: Name -> Name -> Ordering #

(<) :: Name -> Name -> Bool #

(<=) :: Name -> Name -> Bool #

(>) :: Name -> Name -> Bool #

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

max :: Name -> Name -> Name #

min :: Name -> Name -> Name #

Show Name Source #

Only use this show function in debugging! To convert an abstract Name into a string use prettyShow.

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

showsPrec :: Int -> Name -> ShowS #

show :: Name -> String #

showList :: [Name] -> ShowS #

NFData Name Source #

The range is not forced.

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: Name -> () #

Hashable Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

hashWithSalt :: Int -> Name -> Int

hash :: Name -> Int

Pretty Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

KillRange Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

SetRange Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

setRange :: Range -> Name -> Name Source #

HasRange Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: Name -> Range Source #

LensFixity' Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

LensFixity Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

IsNoName Name Source #

An abstract name is empty if its concrete name is empty.

Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

isNoName :: Name -> Bool Source #

LensInScope Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

NumHoles Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

numHoles :: Name -> Int Source #

SetBindingSite Name Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Suggest Name Source # 
Instance details

Defined in Agda.Syntax.Internal

EmbPrj Name Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

PrettyTCM Name Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

AddContext Name Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => Name -> m a -> m a Source #

contextSize :: Name -> Nat Source #

InstantiateFull Name Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Subst Term Name Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

ToConcrete Name Name Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Reify Name Name Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Name -> m Name Source #

reifyWhen :: MonadReify m => Bool -> Name -> m Name Source #

ToAbstract Pattern (Names, Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

AddContext (Dom (Name, Type)) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => Dom (Name, Type) -> m a -> m a Source #

contextSize :: Dom (Name, Type) -> Nat Source #

ToAbstract (NewName Name) Name Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract r a => ToAbstract (Abs r) (a, Name) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: MonadReflectedToAbstract m => Abs r -> m (a, Name) Source #

(Free i, Reify i a) => Reify (Abs i) (Name, a) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Abs i -> m (Name, a) Source #

reifyWhen :: MonadReify m => Bool -> Abs i -> m (Name, a) Source #

AddContext ([NamedArg Name], Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source #

contextSize :: ([NamedArg Name], Type) -> Nat Source #

AddContext ([Arg Name], Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([Arg Name], Type) -> m a -> m a Source #

contextSize :: ([Arg Name], Type) -> Nat Source #

AddContext ([WithHiding Name], Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

AddContext ([Name], Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([Name], Dom Type) -> m a -> m a Source #

contextSize :: ([Name], Dom Type) -> Nat Source #

AddContext (Name, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => (Name, Dom Type) -> m a -> m a Source #

contextSize :: (Name, Dom Type) -> Nat Source #

ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

uglyShowName :: Name -> String Source #

Useful for debugging scoping problems

unambiguous :: QName -> AmbiguousQName Source #

A singleton "ambiguous" name.

headAmbQ :: AmbiguousQName -> QName Source #

Get the first of the ambiguous names.

isAmbiguous :: AmbiguousQName -> Bool Source #

Is a name ambiguous.

getUnambiguous :: AmbiguousQName -> Maybe QName Source #

Get the name if unambiguous.

isAnonymousModuleName :: ModuleName -> Bool Source #

A module is anonymous if the qualification path ends in an underscore.

withRangesOf :: ModuleName -> [Name] -> ModuleName Source #

Sets the ranges of the individual names in the module name to match those of the corresponding concrete names. If the concrete names are fewer than the number of module name name parts, then the initial name parts get the range noRange.

C.D.E `withRangesOf` [A, B] returns C.D.E but with ranges set as follows:

  • C: noRange.
  • D: the range of A.
  • E: the range of B.

Precondition: The number of module name name parts has to be at least as large as the length of the list.

withRangesOfQ :: ModuleName -> QName -> ModuleName Source #

Like withRangesOf, but uses the name parts (qualifier + name) of the qualified name as the list of concrete names.

qnameToConcrete :: QName -> QName Source #

Turn a qualified name into a concrete name. This should only be used as a fallback when looking up the right concrete name in the scope fails.

toTopLevelModuleName :: ModuleName -> TopLevelModuleName Source #

Computes the TopLevelModuleName corresponding to the given module name, which is assumed to represent a top-level module name.

Precondition: The module name must be well-formed.

qualify_ :: Name -> QName Source #

Convert a Name to a QName (add no module name).

isOperator :: QName -> Bool Source #

Is the name an operator?

isLeParentModuleOf :: ModuleName -> ModuleName -> Bool Source #

Is the first module a weak parent of the second?

isLtParentModuleOf :: ModuleName -> ModuleName -> Bool Source #

Is the first module a proper parent of the second?

isLeChildModuleOf :: ModuleName -> ModuleName -> Bool Source #

Is the first module a weak child of the second?

isLtChildModuleOf :: ModuleName -> ModuleName -> Bool Source #

Is the first module a proper child of the second?

nextName :: Name -> Name Source #

Get the next version of the concrete name. For instance, nextName "x" = "x₁". The name must not be a NoName.