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

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

UniverseBi Declaration (NamedArg Pattern) Source # 
Instance details

Defined in Agda.Syntax.Abstract

UniverseBi Declaration (Pattern' Void) Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

universeBi :: Declaration -> [Pattern' Void] Source #

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

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

Methods

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

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

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

NamesIn (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

ExpandPatternSynonyms (Pattern' e) Source # 
Instance details

Defined in Agda.TypeChecking.Patterns.Abstract

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data LHSCore' e Source #

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

Constructors

LHSHead

The head applied to ordinary patterns.

Fields

LHSProj

Projection.

Fields

LHSWith

With patterns.

Fields

Instances
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

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

Methods

allNames :: Clause -> Seq QName Source #

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

Defined in Agda.Syntax.Abstract

Methods

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

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

Data SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: SpineLHS -> Constr

dataTypeOf :: SpineLHS -> DataType

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

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

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

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

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

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

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

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

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

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

Show SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> SpineLHS -> ShowS

show :: SpineLHS -> String

showList :: [SpineLHS] -> ShowS

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

  • rhsExpr :: Expr
     
  • rhsConcrete :: Maybe Expr

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

AbsurdRHS 
WithRHS QName [Expr] [Clause]

The QName is the name of the with function.

RewriteRHS 

Fields

Instances
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 :: (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, [Expr], [Expr], [Declaration]) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

data WhereDeclarations Source #

Constructors

WhereDecls 
Instances
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WhereDeclarations -> r

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

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

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

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

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

Show WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> WhereDeclarations -> ShowS

show :: WhereDeclarations -> String

showList :: [WhereDeclarations] -> ShowS

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

Methods

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

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

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

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

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

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

Methods

allNames :: Clause -> Seq QName Source #

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

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

Defined in Agda.Syntax.Translation.ReflectedToAbstract

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

Defined in Agda.Syntax.Abstract

Methods

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

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

Data ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: ProblemEq -> Constr

dataTypeOf :: ProblemEq -> DataType

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

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

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

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

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

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

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

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

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

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

Show ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> ProblemEq -> ShowS

show :: ProblemEq -> String

showList :: [ProblemEq] -> ShowS

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
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataDefParams -> r

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

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

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

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

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

Show DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> DataDefParams -> ShowS

show :: DataDefParams -> String

showList :: [DataDefParams] -> ShowS

KillRange DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract

ExprLike DataDefParams Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

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

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

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

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

data GeneralizeTelescope Source #

Constructors

GeneralizeTel 

Fields

Instances
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GeneralizeTelescope -> r

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

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

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

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

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

Show GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> GeneralizeTelescope -> ShowS

show :: GeneralizeTelescope -> String

showList :: [GeneralizeTelescope] -> ShowS

KillRange GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract

ExprLike GeneralizeTelescope Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

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

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

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

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

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 [NamedArg BindName] 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
Eq TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

Data TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: TypedBinding -> Constr

dataTypeOf :: TypedBinding -> DataType

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

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

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

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

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

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

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

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

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

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

Show TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> TypedBinding -> ShowS

show :: TypedBinding -> String

showList :: [TypedBinding] -> ShowS

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

Methods

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

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

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

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

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 (NamedArg BindName)

. x or {x} or .x or {x = y}

DomainFull TypedBinding

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

Instances
Eq LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

Data LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: LamBinding -> Constr

dataTypeOf :: LamBinding -> DataType

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

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

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

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

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

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

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

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

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

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

Show LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> LamBinding -> ShowS

show :: LamBinding -> String

showList :: [LamBinding] -> ShowS

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

Methods

allNames :: LamBinding -> Seq QName Source #

ExprLike LamBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

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

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

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

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

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

Defined in Agda.Syntax.Abstract

Methods

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

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

Data LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: LetBinding -> Constr

dataTypeOf :: LetBinding -> DataType

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

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

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

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

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

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

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

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

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

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

Show LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> LetBinding -> ShowS

show :: LetBinding -> String

showList :: [LetBinding] -> ShowS

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

Methods

allNames :: LetBinding -> Seq QName Source #

ExprLike LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

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

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

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

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

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

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

BuiltinNoDefPragma String QName

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

RewritePragma QName 
CompilePragma String QName String 
StaticPragma QName 
EtaPragma QName

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

InjectivePragma QName 
InlinePragma Bool QName 
DisplayPragma QName [NamedArg Pattern] Expr 
Instances
Eq Pragma 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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pragma -> r

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

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

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

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

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

Show Pragma Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> Pragma -> ShowS

show :: Pragma -> String

showList :: [Pragma] -> ShowS

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
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModuleApplication -> r

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

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

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

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

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

Show ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> ModuleApplication -> ShowS

show :: ModuleApplication -> String

showList :: [ModuleApplication] -> ShowS

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

Methods

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

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

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

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

ToConcrete ModuleApplication ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

class GetDefInfo a where Source #

Methods

getDefInfo :: a -> Maybe DefInfo Source #

Instances
GetDefInfo Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

Does not compare ScopeInfo fields.

Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

Data Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: Declaration -> Constr

dataTypeOf :: Declaration -> DataType

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

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

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

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

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

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

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

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

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

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

Show Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> Declaration -> ShowS

show :: Declaration -> String

showList :: [Declaration] -> ShowS

KillRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

HasRange Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

GetDefInfo Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

AnyAbstract Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

anyAbstract :: Declaration -> Bool Source #

AllNames Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

allNames :: Declaration -> Seq QName Source #

ExprLike Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

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

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

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

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

ShowHead Declaration Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Decl

Methods

showHead :: Declaration -> String Source #

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

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

Methods

universeBi :: Declaration -> [Pattern' Void] Source #

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
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ScopeCopyInfo -> r

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

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

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

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

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

Show ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> ScopeCopyInfo -> ShowS

show :: ScopeCopyInfo -> String

showList :: [ScopeCopyInfo] -> ShowS

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
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 :: (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.

QuoteGoal ExprInfo Name Expr

Binds Name to current type in Expr.

QuoteContext ExprInfo

Returns the current context.

Quote ExprInfo

Quote an identifier QName.

QuoteTerm ExprInfo

Quote a term.

Unquote ExprInfo

The splicing construct: unquote ...

Tactic ExprInfo Expr [NamedArg Expr] [NamedArg Expr]
tactic e x1 .. xn | y1 | .. | yn
DontCare Expr

For printing DontCare from Syntax.Internal.

Instances
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 :: (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 :: Expr -> TCM 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

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

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

Reify MetaId Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MetaId -> TCM Expr Source #

reifyWhen :: Bool -> MetaId -> TCM Expr Source #

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 :: Level -> TCM Expr Source #

reifyWhen :: Bool -> Level -> TCM Expr Source #

Reify Sort Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Sort -> TCM Expr Source #

reifyWhen :: Bool -> Sort -> TCM Expr Source #

Reify Type Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Type -> TCM Expr Source #

reifyWhen :: Bool -> Type -> TCM Expr Source #

Reify Term Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Term -> TCM Expr Source #

reifyWhen :: Bool -> Term -> TCM Expr Source #

Reify Expr Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Expr -> TCM Expr Source #

reifyWhen :: Bool -> Expr -> TCM 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 # 
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 [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

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

Defined in Agda.Syntax.Abstract

Methods

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

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

Data BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

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

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

toConstr :: BindName -> Constr

dataTypeOf :: BindName -> DataType

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

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

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

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

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

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

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

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

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

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

Ord BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

compare :: BindName -> BindName -> Ordering

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

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

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

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

max :: BindName -> BindName -> BindName

min :: BindName -> BindName -> BindName

Show BindName Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> BindName -> ShowS

show :: BindName -> String

showList :: [BindName] -> ShowS

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

Methods

icode :: BindName -> S Int32 Source #

icod_ :: BindName -> S Int32 Source #

value :: Int32 -> R BindName Source #

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

Methods

nameExpr :: a -> Expr Source #

Instances
NameToExpr ResolvedName Source #

Assumes name is not UnknownName.

Instance details

Defined in Agda.Syntax.Abstract

NameToExpr AbstractName Source #

Turn an AbstractName to 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
AnyAbstract Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

anyAbstract :: Declaration -> Bool Source #

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

Defined in Agda.Syntax.Abstract

Methods

anyAbstract :: [a] -> Bool Source #

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

Defined in Agda.Syntax.Abstract

Methods

allNames :: QName -> Seq QName Source #

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

Methods

allNames :: Clause -> Seq QName Source #

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

Methods

allNames :: LamBinding -> Seq QName Source #

AllNames LetBinding Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

allNames :: LetBinding -> Seq QName Source #

AllNames ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Abstract

AllNames Declaration Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

allNames :: Declaration -> Seq QName Source #

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

Methods

allNames :: CallInfo -> Seq QName Source #

AllNames CallPath Source # 
Instance details

Defined in Agda.Termination.Monad

Methods

allNames :: CallPath -> Seq QName Source #

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 #

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 "_".

Methods

isNoName :: a -> Bool Source #

Instances
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

Methods

isNoName :: ByteString -> Bool Source #

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 #

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

Defined in Agda.Syntax.Abstract.Name

Methods

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

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

class IsProjP a where Source #

Check whether we are a projection pattern.

Methods

isProjP :: a -> Maybe (ProjOrigin, AmbiguousQName) Source #

Instances
IsProjP Void Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

isProjP :: Void -> Maybe (ProjOrigin, AmbiguousQName) Source #

IsProjP Expr Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

Defined in Agda.Syntax.Abstract.Name

Methods

isProjP :: Arg a -> Maybe (ProjOrigin, AmbiguousQName) Source #

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

Methods

isProjP :: Named n a -> Maybe (ProjOrigin, AmbiguousQName) Source #

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 
Instances
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 :: (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

Methods

showsPrec :: Int -> AmbiguousQName -> ShowS

show :: AmbiguousQName -> String

showList :: [AmbiguousQName] -> ShowS

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

Methods

numHoles :: AmbiguousQName -> Int Source #

EmbPrj AmbiguousQName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: AmbiguousQName -> S Int32 Source #

icod_ :: AmbiguousQName -> S Int32 Source #

value :: Int32 -> R AmbiguousQName Source #

NamesIn AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

UniverseBi Declaration AmbiguousQName Source # 
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
Eq ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

(==) :: ModuleName -> ModuleName -> Bool

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

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

Methods

showsPrec :: Int -> ModuleName -> ShowS

show :: ModuleName -> String

showList :: [ModuleName] -> ShowS

NFData ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

rnf :: ModuleName -> ()

Pretty ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Sized ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

size :: ModuleName -> Int Source #

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

SubstExpr ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract

ExprLike ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

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

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

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

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

EmbPrj ModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: ModuleName -> S Int32 Source #

icod_ :: ModuleName -> S Int32 Source #

value :: Int32 -> R ModuleName Source #

PrettyTCM ModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

InstantiateFull ModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

UniverseBi Declaration ModuleName Source # 
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
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

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

Methods

pretty :: QNamed a -> Doc Source #

prettyPrec :: Int -> QNamed a -> Doc Source #

prettyList :: [QNamed a] -> Doc Source #

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

Pretty QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Sized QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

size :: QName -> Int Source #

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 #

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 #

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

Methods

allNames :: QName -> Seq QName Source #

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

Methods

icode :: QName -> S Int32 Source #

icod_ :: QName -> S Int32 Source #

value :: Int32 -> R QName Source #

PrettyTCM QName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: QName -> TCM 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

Occurs QName Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

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 #

Unquote QName Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

UniverseBi Declaration QName Source # 
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

Methods

toConcrete :: Maybe QName -> AbsToCon (Maybe Name) Source #

bindToConcrete :: Maybe QName -> (Maybe Name -> AbsToCon b) -> AbsToCon b Source #

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.

Instances
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 :: (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

Methods

pretty :: Name -> Doc Source #

prettyPrec :: Int -> Name -> Doc Source #

prettyList :: [Name] -> Doc Source #

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 #

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 #

EmbPrj Name Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Name -> S Int32 Source #

icod_ :: Name -> S Int32 Source #

value :: Int32 -> R Name Source #

PrettyTCM Name Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Name -> TCM Doc Source #

AddContext Name Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => Name -> tcm a -> tcm 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 :: Name -> TCM Name Source #

reifyWhen :: Bool -> Name -> TCM Name Source #

Suggest Name (Abs b) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

suggest :: Name -> Abs b -> String 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 :: (MonadTCM tcm, MonadDebug tcm) => Dom (Name, Type) -> tcm a -> tcm 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 :: Abs r -> WithNames (a, Name) Source #

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Abs i -> TCM (Name, a) Source #

reifyWhen :: Bool -> Abs i -> TCM (Name, a) Source #

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

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => ([NamedArg Name], Type) -> tcm a -> tcm a Source #

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

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

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => ([Arg Name], Type) -> tcm a -> tcm a Source #

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

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

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => ([WithHiding Name], Dom Type) -> tcm a -> tcm a Source #

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

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

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => ([Name], Dom Type) -> tcm a -> tcm a Source #

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

AddContext (Name, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => (Name, Dom Type) -> tcm a -> tcm 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.

showQNameId :: QName -> String Source #

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?

nextName :: Name -> Name Source #

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

sameRoot :: Name -> Name -> Bool Source #