Agda-2.5.2: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Common

Contents

Description

Some common syntactic entities are defined in this module.

Synopsis

Delayed

data Delayed #

Used to specify whether something should be delayed.

Constructors

Delayed 
NotDelayed 

Induction

Hiding

data Hiding #

Constructors

Hidden 
Instance 
NotHidden 

Instances

data WithHiding a #

Decorating something with Hiding information.

Constructors

WithHiding !Hiding a 

Instances

Functor WithHiding # 

Methods

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

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

Applicative WithHiding # 

Methods

pure :: a -> WithHiding a #

(<*>) :: WithHiding (a -> b) -> WithHiding a -> WithHiding b #

(*>) :: WithHiding a -> WithHiding b -> WithHiding b #

(<*) :: WithHiding a -> WithHiding b -> WithHiding a #

Foldable WithHiding # 

Methods

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

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

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

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

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

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

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

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

toList :: WithHiding a -> [a] #

null :: WithHiding a -> Bool #

length :: WithHiding a -> Int #

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

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

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

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

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

Traversable WithHiding # 

Methods

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

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

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

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

Decoration WithHiding # 

Methods

traverseF :: Functor m => (a -> m b) -> WithHiding a -> m (WithHiding b) #

distributeF :: Functor m => WithHiding (m a) -> m (WithHiding a) #

Eq a => Eq (WithHiding a) # 

Methods

(==) :: WithHiding a -> WithHiding a -> Bool #

(/=) :: WithHiding a -> WithHiding a -> Bool #

Ord a => Ord (WithHiding a) # 
Show a => Show (WithHiding a) # 
NFData a => NFData (WithHiding a) # 

Methods

rnf :: WithHiding a -> () #

KillRange a => KillRange (WithHiding a) # 
SetRange a => SetRange (WithHiding a) # 

Methods

setRange :: Range -> WithHiding a -> WithHiding a #

HasRange a => HasRange (WithHiding a) # 

Methods

getRange :: WithHiding a -> Range #

LensHiding (WithHiding a) # 
PrettyTCM a => PrettyTCM (WithHiding a) # 

Methods

prettyTCM :: WithHiding a -> TCM Doc #

ToConcrete a c => ToConcrete (WithHiding a) (WithHiding c) # 
ToAbstract c a => ToAbstract (WithHiding c) (WithHiding a) # 
AddContext ([WithHiding Name], Dom Type) # 

Methods

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

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

class LensHiding a where #

A lens to access the Hiding attribute in data structures. Minimal implementation: getHiding and one of setHiding or mapHiding.

Minimal complete definition

getHiding

Methods

getHiding :: a -> Hiding #

setHiding :: Hiding -> a -> a #

mapHiding :: (Hiding -> Hiding) -> a -> a #

Instances

LensHiding ArgInfo # 
LensHiding Hiding # 
LensHiding TypedBindings # 
LensHiding LamBinding # 
LensHiding TypedBindings # 
LensHiding LamBinding # 
LensHiding (Dom e) # 

Methods

getHiding :: Dom e -> Hiding #

setHiding :: Hiding -> Dom e -> Dom e #

mapHiding :: (Hiding -> Hiding) -> Dom e -> Dom e #

LensHiding (Arg e) # 

Methods

getHiding :: Arg e -> Hiding #

setHiding :: Hiding -> Arg e -> Arg e #

mapHiding :: (Hiding -> Hiding) -> Arg e -> Arg e #

LensHiding (WithHiding a) # 
LensHiding (FlexibleVar a) # 

mergeHiding :: LensHiding a => WithHiding a -> a #

Monoidal composition of Hiding information in some data.

notHidden :: LensHiding a => a -> Bool #

Visible (NotHidden) arguments are notHidden. (DEPRECATED, use visible.)

visible :: LensHiding a => a -> Bool #

NotHidden arguments are visible.

notVisible :: LensHiding a => a -> Bool #

Instance and Hidden arguments are notVisible.

hide :: LensHiding a => a -> a #

makeInstance :: LensHiding a => a -> a #

Relevance

data Big #

An constructor argument is big if the sort of its type is bigger than the sort of the data type. Only parameters (and maybe forced arguments) are allowed to be big. List : Set -> Set nil : (A : Set) -> List A A is big in constructor nil as the sort Set1 of its type Set is bigger than the sort Set of the data type List.

Constructors

Big 
Small 

Instances

Bounded Big # 

Methods

minBound :: Big #

maxBound :: Big #

Enum Big # 

Methods

succ :: Big -> Big #

pred :: Big -> Big #

toEnum :: Int -> Big #

fromEnum :: Big -> Int #

enumFrom :: Big -> [Big] #

enumFromThen :: Big -> Big -> [Big] #

enumFromTo :: Big -> Big -> [Big] #

enumFromThenTo :: Big -> Big -> Big -> [Big] #

Eq Big # 

Methods

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

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

Ord Big # 

Methods

compare :: Big -> Big -> Ordering #

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

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

(>) :: Big -> Big -> Bool #

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

max :: Big -> Big -> Big #

min :: Big -> Big -> Big #

Show Big # 

Methods

showsPrec :: Int -> Big -> ShowS #

show :: Big -> String #

showList :: [Big] -> ShowS #

NFData Big # 

Methods

rnf :: Big -> () #

data Relevance #

A function argument can be relevant or irrelevant. See Agda.TypeChecking.Irrelevance.

Constructors

Relevant

The argument is (possibly) relevant at compile-time.

NonStrict

The argument may never flow into evaluation position. Therefore, it is irrelevant at run-time. It is treated relevantly during equality checking.

Irrelevant

The argument is irrelevant at compile- and runtime.

Forced Big

The argument can be skipped during equality checking because its value is already determined by the type. If a constructor argument is big, it has to be regarded absent, otherwise we get into paradoxes.

UnusedArg

The polarity checker has determined that this argument is unused in the definition. It can be skipped during equality checking but should be mined for solutions of meta-variables with relevance UnusedArg

class LensRelevance a where #

A lens to access the Relevance attribute in data structures. Minimal implementation: getRelevance and one of setRelevance or mapRelevance.

Minimal complete definition

getRelevance

Methods

getRelevance :: a -> Relevance #

setRelevance :: Relevance -> a -> a #

mapRelevance :: (Relevance -> Relevance) -> a -> a #

moreRelevant :: Relevance -> Relevance -> Bool #

Information ordering. Relevant `moreRelevant` UnusedArg `moreRelevant` Forced `moreRelevant` NonStrict `moreRelevant` Irrelevant

unusableRelevance :: Relevance -> Bool #

unusableRelevance rel == True iff we cannot use a variable of rel.

composeRelevance :: Relevance -> Relevance -> Relevance #

Relevance composition. Irrelevant is dominant, Relevant is neutral.

inverseComposeRelevance :: Relevance -> Relevance -> Relevance #

inverseComposeRelevance r x returns the most irrelevant y such that forall x, y we have x `moreRelevant` (r `composeRelevance` y) iff (r `inverseComposeRelevance` x) `moreRelevant` y (Galois connection).

ignoreForced :: Relevance -> Relevance #

For comparing Relevance ignoring Forced and UnusedArg.

irrToNonStrict :: Relevance -> Relevance #

Irrelevant function arguments may appear non-strictly in the codomain type.

nonStrictToRel :: Relevance -> Relevance #

Applied when working on types (unless --experimental-irrelevance).

Origin of arguments (user-written, inserted or reflected)

class LensOrigin a where #

Minimal complete definition

getOrigin

Methods

getOrigin :: a -> Origin #

setOrigin :: Origin -> a -> a #

mapOrigin :: (Origin -> Origin) -> a -> a #

Argument decoration

data ArgInfo #

A function argument can be hidden and/or irrelevant.

Instances

Eq ArgInfo # 

Methods

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

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

Ord ArgInfo # 
Show ArgInfo # 
NFData ArgInfo # 

Methods

rnf :: ArgInfo -> () #

KillRange ArgInfo # 
LensArgInfo ArgInfo # 
LensOrigin ArgInfo # 
LensRelevance ArgInfo # 
LensHiding ArgInfo # 
SynEq ArgInfo # 

Methods

synEq :: ArgInfo -> ArgInfo -> SynEqM (ArgInfo, ArgInfo)

synEq' :: ArgInfo -> ArgInfo -> SynEqM (ArgInfo, ArgInfo)

ToTerm ArgInfo # 
Unquote ArgInfo # 

class LensArgInfo a where #

Minimal complete definition

getArgInfo

Methods

getArgInfo :: a -> ArgInfo #

setArgInfo :: ArgInfo -> a -> a #

mapArgInfo :: (ArgInfo -> ArgInfo) -> a -> a #

Arguments

data Arg e #

Constructors

Arg 

Fields

Instances

Functor Arg # 

Methods

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

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

Foldable Arg # 

Methods

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

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

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

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

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

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

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

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

toList :: Arg a -> [a] #

null :: Arg a -> Bool #

length :: Arg a -> Int #

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

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

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

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

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

Traversable Arg # 

Methods

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

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

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

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

Decoration Arg # 

Methods

traverseF :: Functor m => (a -> m b) -> Arg a -> m (Arg b) #

distributeF :: Functor m => Arg (m a) -> m (Arg a) #

IsPrefixOf Args # 

Methods

isPrefixOf :: Args -> Args -> Maybe Elims #

UniverseBi Args Pattern # 

Methods

universeBi :: Args -> [Pattern] #

UniverseBi Args Term # 

Methods

universeBi :: Args -> [Term] #

Eq a => Eq (Arg a) # 

Methods

(==) :: Arg a -> Arg a -> Bool #

(/=) :: Arg a -> Arg a -> Bool #

Ord e => Ord (Arg e) # 

Methods

compare :: Arg e -> Arg e -> Ordering #

(<) :: Arg e -> Arg e -> Bool #

(<=) :: Arg e -> Arg e -> Bool #

(>) :: Arg e -> Arg e -> Bool #

(>=) :: Arg e -> Arg e -> Bool #

max :: Arg e -> Arg e -> Arg e #

min :: Arg e -> Arg e -> Arg e #

Show a => Show (Arg a) # 

Methods

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

show :: Arg a -> String #

showList :: [Arg a] -> ShowS #

NFData e => NFData (Arg e) # 

Methods

rnf :: Arg e -> () #

KillRange a => KillRange (Arg a) # 

Methods

killRange :: KillRangeT (Arg a) #

SetRange a => SetRange (Arg a) # 

Methods

setRange :: Range -> Arg a -> Arg a #

HasRange a => HasRange (Arg a) # 

Methods

getRange :: Arg a -> Range #

LensArgInfo (Arg a) # 

Methods

getArgInfo :: Arg a -> ArgInfo #

setArgInfo :: ArgInfo -> Arg a -> Arg a #

mapArgInfo :: (ArgInfo -> ArgInfo) -> Arg a -> Arg a #

LensOrigin (Arg e) # 

Methods

getOrigin :: Arg e -> Origin #

setOrigin :: Origin -> Arg e -> Arg e #

mapOrigin :: (Origin -> Origin) -> Arg e -> Arg e #

LensRelevance (Arg e) # 
LensHiding (Arg e) # 

Methods

getHiding :: Arg e -> Hiding #

setHiding :: Hiding -> Arg e -> Arg e #

mapHiding :: (Hiding -> Hiding) -> Arg e -> Arg e #

IsProjP a => IsProjP (Arg a) # 
ExprLike a => ExprLike (Arg a) # 

Methods

mapExpr :: (Expr -> Expr) -> Arg a -> Arg a #

traverseExpr :: Monad m => (Expr -> m Expr) -> Arg a -> m (Arg a) #

foldExpr :: Monoid m => (Expr -> m) -> Arg a -> m #

MaybePostfixProjP a => MaybePostfixProjP (Arg a) # 
SubstExpr a => SubstExpr (Arg a) # 

Methods

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

AllNames a => AllNames (Arg a) # 

Methods

allNames :: Arg a -> Seq QName #

ExprLike a => ExprLike (Arg a) # 

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Arg a -> m (Arg a) #

foldExpr :: Monoid m => (Expr -> m) -> Arg a -> m #

traverseExpr :: Monad m => (Expr -> m Expr) -> Arg a -> m (Arg a) #

mapExpr :: (Expr -> Expr) -> Arg a -> Arg a #

GetDefs a => GetDefs (Arg a) # 

Methods

getDefs :: MonadGetDefs m => Arg a -> m () #

TermLike a => TermLike (Arg a) # 

Methods

traverseTerm :: (Term -> Term) -> Arg a -> Arg a #

traverseTermM :: Monad m => (Term -> m Term) -> Arg a -> m (Arg a) #

foldTerm :: Monoid m => (Term -> m) -> Arg a -> m #

Free a => Free (Arg a) # 

Methods

freeVars' :: Arg a -> FreeT

NamesIn a => NamesIn (Arg a) # 

Methods

namesIn :: Arg a -> Set QName #

IsInstantiatedMeta a => IsInstantiatedMeta (Arg a) # 
MentionsMeta t => MentionsMeta (Arg t) # 

Methods

mentionsMeta :: MetaId -> Arg t -> Bool #

ExpandPatternSynonyms a => ExpandPatternSynonyms (Arg a) # 

Methods

expandPatternSynonyms :: Arg a -> TCM (Arg a) #

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Arg a) # 

Methods

prettyTCM :: Arg a -> TCM Doc #

InstantiateFull t => InstantiateFull (Arg t) # 

Methods

instantiateFull' :: Arg t -> ReduceM (Arg t) #

Normalise t => Normalise (Arg t) # 

Methods

normalise' :: Arg t -> ReduceM (Arg t) #

Simplify t => Simplify (Arg t) # 

Methods

simplify' :: Arg t -> ReduceM (Arg t) #

Reduce t => Reduce (Arg t) # 

Methods

reduce' :: Arg t -> ReduceM (Arg t) #

reduceB' :: Arg t -> ReduceM (Blocked (Arg t)) #

Instantiate t => Instantiate (Arg t) # 

Methods

instantiate' :: Arg t -> ReduceM (Arg t) #

Match a => Match (Arg a) # 

Methods

match :: Arg a -> Arg a -> MaybeT TCM [Term] #

SynEq a => SynEq (Arg a) # 

Methods

synEq :: Arg a -> Arg a -> SynEqM (Arg a, Arg a)

synEq' :: Arg a -> Arg a -> SynEqM (Arg a, Arg a)

Injectible a => Injectible (Arg a) # 
Evaluate a => Evaluate (Arg a) # 

Methods

evaluate :: Arg a -> Compile TCM (Arg a) #

HasPolarity a => HasPolarity (Arg a) # 

Methods

polarities :: Nat -> Arg a -> TCM [Polarity] #

NormaliseProjP a => NormaliseProjP (Arg a) # 

Methods

normaliseProjP :: HasConstInfo m => Arg a -> m (Arg a) #

FoldRigid a => FoldRigid (Arg a) # 

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Arg a -> TCM m #

Occurs a => Occurs (Arg a) # 

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Arg a -> TCM (Arg a) #

metaOccurs :: MetaId -> Arg a -> TCM () #

ComputeOccurrences a => ComputeOccurrences (Arg a) # 
RaiseNLP a => RaiseNLP (Arg a) # 

Methods

raiseNLPFrom :: Int -> Int -> Arg a -> Arg a #

raiseNLP :: Int -> Arg a -> Arg a #

NoProjectedVar a => NoProjectedVar (Arg a) # 
AbsTerm a => AbsTerm (Arg a) # 

Methods

absTerm :: Term -> Arg a -> Arg a #

IsFlexiblePattern a => IsFlexiblePattern (Arg a) # 
Unquote a => Unquote (Arg a) # 

Methods

unquote :: Term -> UnquoteM (Arg a) #

Free' a c => Free' (Arg a) c # 

Methods

freeVars' :: Arg a -> FreeM c #

ToConcrete a c => ToConcrete (Arg a) (Arg c) # 

Methods

toConcrete :: Arg a -> AbsToCon (Arg c) #

bindToConcrete :: Arg a -> (Arg c -> AbsToCon b) -> AbsToCon b #

ToAbstract [Arg Term] [NamedArg Expr] # 
ToAbstract r a => ToAbstract (Arg r) (NamedArg a) # 

Methods

toAbstract :: Arg r -> WithNames (NamedArg a) #

Reify i a => Reify (Dom i) (Arg a) # 

Methods

reify :: Dom i -> TCM (Arg a) #

reifyWhen :: Bool -> Dom i -> TCM (Arg a) #

Reify i a => Reify (Arg i) (Arg a) #

Skip reification of implicit and irrelevant args if option is off.

Methods

reify :: Arg i -> TCM (Arg a) #

reifyWhen :: Bool -> Arg i -> TCM (Arg a) #

Match a b => Match (Arg a) (Arg b) # 

Methods

match :: Relevance -> Telescope -> Telescope -> Arg a -> Arg b -> NLM () #

PatternFrom a b => PatternFrom (Arg a) (Arg b) # 

Methods

patternFrom :: Relevance -> Int -> Arg a -> TCM (Arg b) #

ToAbstract c a => ToAbstract (Arg c) (Arg a) # 

Methods

toAbstract :: Arg c -> ScopeM (Arg a) #

LabelPatVars a b i => LabelPatVars (Arg a) (Arg b) i # 

Methods

labelPatVars :: Arg a -> State [i] (Arg b) #

unlabelPatVars :: Arg b -> Arg a #

defaultArg :: a -> Arg a #

withArgsFrom :: [a] -> [Arg b] -> [Arg a] #

xs `withArgsFrom` args translates xs into a list of Args, using the elements in args to fill in the non-unArg fields.

Precondition: The two lists should have equal length.

withNamedArgsFrom :: [a] -> [NamedArg b] -> [NamedArg a] #

Names

Function type domain

data Dom e #

Similar to Arg, but we need to distinguish an irrelevance annotation in a function domain (the domain itself is not irrelevant!) from an irrelevant argument.

Dom is used in Pi of internal syntax, in Context and Telescope. Arg is used for actual arguments (Var, Con, Def etc.) and in Abstract syntax and other situations.

Constructors

Dom 

Fields

Instances

Functor Dom # 

Methods

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

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

Foldable Dom # 

Methods

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

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

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

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

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

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

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

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

toList :: Dom a -> [a] #

null :: Dom a -> Bool #

length :: Dom a -> Int #

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

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

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

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

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

Traversable Dom # 

Methods

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

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

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

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

Decoration Dom # 

Methods

traverseF :: Functor m => (a -> m b) -> Dom a -> m (Dom b) #

distributeF :: Functor m => Dom (m a) -> m (Dom a) #

TeleNoAbs Telescope # 

Methods

teleNoAbs :: Telescope -> Term -> Term #

TeleNoAbs ListTel # 

Methods

teleNoAbs :: ListTel -> Term -> Term #

AddContext Telescope # 

Methods

addContext :: MonadTCM tcm => Telescope -> tcm a -> tcm a #

contextSize :: Telescope -> Nat #

DropArgs Telescope #

NOTE: This creates telescopes with unbound de Bruijn indices.

Methods

dropArgs :: Int -> Telescope -> Telescope #

PrettyTCM Telescope # 

Methods

prettyTCM :: Telescope -> TCM Doc #

Reduce Telescope # 
Instantiate Telescope # 
Reify Telescope Telescope # 
Eq a => Eq (Dom a) # 

Methods

(==) :: Dom a -> Dom a -> Bool #

(/=) :: Dom a -> Dom a -> Bool #

Ord e => Ord (Dom e) # 

Methods

compare :: Dom e -> Dom e -> Ordering #

(<) :: Dom e -> Dom e -> Bool #

(<=) :: Dom e -> Dom e -> Bool #

(>) :: Dom e -> Dom e -> Bool #

(>=) :: Dom e -> Dom e -> Bool #

max :: Dom e -> Dom e -> Dom e #

min :: Dom e -> Dom e -> Dom e #

Show a => Show (Dom a) # 

Methods

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

show :: Dom a -> String #

showList :: [Dom a] -> ShowS #

Pretty a => Pretty (Tele (Dom a)) # 

Methods

pretty :: Tele (Dom a) -> Doc #

prettyPrec :: Int -> Tele (Dom a) -> Doc #

KillRange a => KillRange (Dom a) # 

Methods

killRange :: KillRangeT (Dom a) #

HasRange a => HasRange (Dom a) # 

Methods

getRange :: Dom a -> Range #

LensArgInfo (Dom e) # 

Methods

getArgInfo :: Dom e -> ArgInfo #

setArgInfo :: ArgInfo -> Dom e -> Dom e #

mapArgInfo :: (ArgInfo -> ArgInfo) -> Dom e -> Dom e #

LensRelevance (Dom e) # 
LensHiding (Dom e) # 

Methods

getHiding :: Dom e -> Hiding #

setHiding :: Hiding -> Dom e -> Dom e #

mapHiding :: (Hiding -> Hiding) -> Dom e -> Dom e #

SgTel (Dom (ArgName, Type)) # 

Methods

sgTel :: Dom (ArgName, Type) -> Telescope #

SgTel (Dom Type) # 

Methods

sgTel :: Dom Type -> Telescope #

LensSort a => LensSort (Dom a) # 

Methods

lensSort :: Lens' Sort (Dom a) #

getSort :: Dom a -> Sort #

GetDefs a => GetDefs (Dom a) # 

Methods

getDefs :: MonadGetDefs m => Dom a -> m () #

TermLike a => TermLike (Dom a) # 

Methods

traverseTerm :: (Term -> Term) -> Dom a -> Dom a #

traverseTermM :: Monad m => (Term -> m Term) -> Dom a -> m (Dom a) #

foldTerm :: Monoid m => (Term -> m) -> Dom a -> m #

Free a => Free (Dom a) # 

Methods

freeVars' :: Dom a -> FreeT

NamesIn a => NamesIn (Dom a) # 

Methods

namesIn :: Dom a -> Set QName #

AddContext (Dom (String, Type)) # 

Methods

addContext :: MonadTCM tcm => Dom (String, Type) -> tcm a -> tcm a #

contextSize :: Dom (String, Type) -> Nat #

AddContext (Dom (Name, Type)) # 

Methods

addContext :: MonadTCM tcm => Dom (Name, Type) -> tcm a -> tcm a #

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

AddContext (Dom Type) # 

Methods

addContext :: MonadTCM tcm => Dom Type -> tcm a -> tcm a #

contextSize :: Dom Type -> Nat #

MentionsMeta t => MentionsMeta (Dom t) # 

Methods

mentionsMeta :: MetaId -> Dom t -> Bool #

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Dom a) # 

Methods

prettyTCM :: Dom a -> TCM Doc #

InstantiateFull t => InstantiateFull (Dom t) # 

Methods

instantiateFull' :: Dom t -> ReduceM (Dom t) #

Normalise t => Normalise (Dom t) # 

Methods

normalise' :: Dom t -> ReduceM (Dom t) #

Simplify t => Simplify (Dom t) # 

Methods

simplify' :: Dom t -> ReduceM (Dom t) #

Reduce t => Reduce (Dom t) # 

Methods

reduce' :: Dom t -> ReduceM (Dom t) #

reduceB' :: Dom t -> ReduceM (Blocked (Dom t)) #

Instantiate t => Instantiate (Dom t) # 

Methods

instantiate' :: Dom t -> ReduceM (Dom t) #

SynEq a => SynEq (Dom a) # 

Methods

synEq :: Dom a -> Dom a -> SynEqM (Dom a, Dom a)

synEq' :: Dom a -> Dom a -> SynEqM (Dom a, Dom a)

HasPolarity a => HasPolarity (Dom a) # 

Methods

polarities :: Nat -> Dom a -> TCM [Polarity] #

FoldRigid a => FoldRigid (Dom a) # 

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Dom a -> TCM m #

Occurs a => Occurs (Dom a) # 

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Dom a -> TCM (Dom a) #

metaOccurs :: MetaId -> Dom a -> TCM () #

ComputeOccurrences a => ComputeOccurrences (Dom a) # 
RaiseNLP a => RaiseNLP (Dom a) # 

Methods

raiseNLPFrom :: Int -> Int -> Dom a -> Dom a #

raiseNLP :: Int -> Dom a -> Dom a #

AbsTerm a => AbsTerm (Dom a) # 

Methods

absTerm :: Term -> Dom a -> Dom a #

Unquote a => Unquote (Dom a) # 

Methods

unquote :: Term -> UnquoteM (Dom a) #

Free' a c => Free' (Dom a) c # 

Methods

freeVars' :: Dom a -> FreeM c #

Reify i a => Reify (Dom i) (Arg a) # 

Methods

reify :: Dom i -> TCM (Arg a) #

reifyWhen :: Bool -> Dom i -> TCM (Arg a) #

Match a b => Match (Dom a) (Dom b) # 

Methods

match :: Relevance -> Telescope -> Telescope -> Dom a -> Dom b -> NLM () #

PatternFrom a b => PatternFrom (Dom a) (Dom b) # 

Methods

patternFrom :: Relevance -> Int -> Dom a -> TCM (Dom b) #

SgTel (ArgName, Dom Type) # 

Methods

sgTel :: (ArgName, Dom Type) -> Telescope #

AddContext ([WithHiding Name], Dom Type) # 

Methods

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

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

AddContext ([Name], Dom Type) # 

Methods

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

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

AddContext (String, Dom Type) # 

Methods

addContext :: MonadTCM tcm => (String, Dom Type) -> tcm a -> tcm a #

contextSize :: (String, Dom Type) -> Nat #

AddContext (Name, Dom Type) # 

Methods

addContext :: MonadTCM tcm => (Name, Dom Type) -> tcm a -> tcm a #

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

ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBindings # 

argFromDom :: Dom a -> Arg a #

domFromArg :: Arg a -> Dom a #

defaultDom :: a -> Dom a #

Named arguments

data Named name a #

Something potentially carrying a name.

Constructors

Named 

Fields

Instances

Functor (Named name) # 

Methods

fmap :: (a -> b) -> Named name a -> Named name b #

(<$) :: a -> Named name b -> Named name a #

Show a => Show (Named_ a) # 

Methods

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

show :: Named_ a -> String #

showList :: [Named_ a] -> ShowS #

Foldable (Named name) # 

Methods

fold :: Monoid m => Named name m -> m #

foldMap :: Monoid m => (a -> m) -> Named name a -> m #

foldr :: (a -> b -> b) -> b -> Named name a -> b #

foldr' :: (a -> b -> b) -> b -> Named name a -> b #

foldl :: (b -> a -> b) -> b -> Named name a -> b #

foldl' :: (b -> a -> b) -> b -> Named name a -> b #

foldr1 :: (a -> a -> a) -> Named name a -> a #

foldl1 :: (a -> a -> a) -> Named name a -> a #

toList :: Named name a -> [a] #

null :: Named name a -> Bool #

length :: Named name a -> Int #

elem :: Eq a => a -> Named name a -> Bool #

maximum :: Ord a => Named name a -> a #

minimum :: Ord a => Named name a -> a #

sum :: Num a => Named name a -> a #

product :: Num a => Named name a -> a #

Traversable (Named name) # 

Methods

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

sequenceA :: Applicative f => Named name (f a) -> f (Named name a) #

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

sequence :: Monad m => Named name (m a) -> m (Named name a) #

Decoration (Named name) # 

Methods

traverseF :: Functor m => (a -> m b) -> Named name a -> m (Named name b) #

distributeF :: Functor m => Named name (m a) -> m (Named name a) #

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a) # 

Methods

prettyTCM :: Named_ a -> TCM Doc #

NormaliseProjP a => NormaliseProjP (Named_ a) # 

Methods

normaliseProjP :: HasConstInfo m => Named_ a -> m (Named_ a) #

ToAbstract [Arg Term] [NamedArg Expr] # 
ToAbstract r a => ToAbstract (Arg r) (NamedArg a) # 

Methods

toAbstract :: Arg r -> WithNames (NamedArg a) #

(Eq a, Eq name) => Eq (Named name a) # 

Methods

(==) :: Named name a -> Named name a -> Bool #

(/=) :: Named name a -> Named name a -> Bool #

(Ord a, Ord name) => Ord (Named name a) # 

Methods

compare :: Named name a -> Named name a -> Ordering #

(<) :: Named name a -> Named name a -> Bool #

(<=) :: Named name a -> Named name a -> Bool #

(>) :: Named name a -> Named name a -> Bool #

(>=) :: Named name a -> Named name a -> Bool #

max :: Named name a -> Named name a -> Named name a #

min :: Named name a -> Named name a -> Named name a #

(NFData name, NFData a) => NFData (Named name a) # 

Methods

rnf :: Named name a -> () #

(KillRange name, KillRange a) => KillRange (Named name a) # 

Methods

killRange :: KillRangeT (Named name a) #

SetRange a => SetRange (Named name a) # 

Methods

setRange :: Range -> Named name a -> Named name a #

HasRange a => HasRange (Named name a) # 

Methods

getRange :: Named name a -> Range #

IsProjP a => IsProjP (Named n a) # 
ExprLike a => ExprLike (Named name a) # 

Methods

mapExpr :: (Expr -> Expr) -> Named name a -> Named name a #

traverseExpr :: Monad m => (Expr -> m Expr) -> Named name a -> m (Named name a) #

foldExpr :: Monoid m => (Expr -> m) -> Named name a -> m #

MaybePostfixProjP a => MaybePostfixProjP (Named n a) # 
SubstExpr a => SubstExpr (Named name a) # 

Methods

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

AllNames a => AllNames (Named name a) # 

Methods

allNames :: Named name a -> Seq QName #

ExprLike a => ExprLike (Named x a) # 

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Named x a -> m (Named x a) #

foldExpr :: Monoid m => (Expr -> m) -> Named x a -> m #

traverseExpr :: Monad m => (Expr -> m Expr) -> Named x a -> m (Named x a) #

mapExpr :: (Expr -> Expr) -> Named x a -> Named x a #

NamesIn a => NamesIn (Named n a) # 

Methods

namesIn :: Named n a -> Set QName #

ExpandPatternSynonyms a => ExpandPatternSynonyms (Named n a) # 

Methods

expandPatternSynonyms :: Named n a -> TCM (Named n a) #

InstantiateFull t => InstantiateFull (Named name t) # 

Methods

instantiateFull' :: Named name t -> ReduceM (Named name t) #

Normalise t => Normalise (Named name t) # 

Methods

normalise' :: Named name t -> ReduceM (Named name t) #

Simplify t => Simplify (Named name t) # 

Methods

simplify' :: Named name t -> ReduceM (Named name t) #

IsFlexiblePattern a => IsFlexiblePattern (Named name a) # 
ToConcrete a c => ToConcrete (Named name a) (Named name c) # 

Methods

toConcrete :: Named name a -> AbsToCon (Named name c) #

bindToConcrete :: Named name a -> (Named name c -> AbsToCon b) -> AbsToCon b #

ToAbstract r a => ToAbstract (Named name r) (Named name a) # 

Methods

toAbstract :: Named name r -> WithNames (Named name a) #

Reify i a => Reify (Named n i) (Named n a) # 

Methods

reify :: Named n i -> TCM (Named n a) #

reifyWhen :: Bool -> Named n i -> TCM (Named n a) #

ToAbstract c a => ToAbstract (Named name c) (Named name a) # 

Methods

toAbstract :: Named name c -> ScopeM (Named name a) #

LabelPatVars a b i => LabelPatVars (Named x a) (Named x b) i # 

Methods

labelPatVars :: Named x a -> State [i] (Named x b) #

unlabelPatVars :: Named x b -> Named x a #

type Named_ = Named RString #

Standard naming.

unnamed :: a -> Named name a #

named :: name -> a -> Named name a #

type NamedArg a = Arg (Named_ a) #

Only Hidden arguments can have names.

namedArg :: NamedArg a -> a #

Get the content of a NamedArg.

updateNamedArg :: (a -> b) -> NamedArg a -> NamedArg b #

The functor instance for NamedArg would be ambiguous, so we give it another name here.

Range decoration.

data Ranged a #

Thing with range info.

Constructors

Ranged 

Fields

Instances

Functor Ranged # 

Methods

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

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

Foldable Ranged # 

Methods

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

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

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

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

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

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

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

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

toList :: Ranged a -> [a] #

null :: Ranged a -> Bool #

length :: Ranged a -> Int #

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

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

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

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

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

Traversable Ranged # 

Methods

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

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

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

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

Decoration Ranged # 

Methods

traverseF :: Functor m => (a -> m b) -> Ranged a -> m (Ranged b) #

distributeF :: Functor m => Ranged (m a) -> m (Ranged a) #

UniverseBi Declaration RString # 
Eq a => Eq (Ranged a) # 

Methods

(==) :: Ranged a -> Ranged a -> Bool #

(/=) :: Ranged a -> Ranged a -> Bool #

Ord a => Ord (Ranged a) # 

Methods

compare :: Ranged a -> Ranged a -> Ordering #

(<) :: Ranged a -> Ranged a -> Bool #

(<=) :: Ranged a -> Ranged a -> Bool #

(>) :: Ranged a -> Ranged a -> Bool #

(>=) :: Ranged a -> Ranged a -> Bool #

max :: Ranged a -> Ranged a -> Ranged a #

min :: Ranged a -> Ranged a -> Ranged a #

Show a => Show (Ranged a) # 

Methods

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

show :: Ranged a -> String #

showList :: [Ranged a] -> ShowS #

Show a => Show (Named_ a) # 

Methods

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

show :: Named_ a -> String #

showList :: [Named_ a] -> ShowS #

NFData a => NFData (Ranged a) #

Ranges are not forced.

Methods

rnf :: Ranged a -> () #

KillRange (Ranged a) # 
HasRange (Ranged a) # 

Methods

getRange :: Ranged a -> Range #

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a) # 

Methods

prettyTCM :: Named_ a -> TCM Doc #

NormaliseProjP a => NormaliseProjP (Named_ a) # 

Methods

normaliseProjP :: HasConstInfo m => Named_ a -> m (Named_ a) #

ToAbstract [Arg Term] [NamedArg Expr] # 
ToAbstract r a => ToAbstract (Arg r) (NamedArg a) # 

Methods

toAbstract :: Arg r -> WithNames (NamedArg a) #

unranged :: a -> Ranged a #

Thing with no range info.

Raw names (before parsing into name parts).

type RawName = String #

A RawName is some sort of string.

type RString = Ranged RawName #

String with range info.

Further constructor and projection info

data ConOrigin #

Where does the ConP or Con come from?

Constructors

ConOSystem

Inserted by system or expanded from an implicit pattern.

ConOCon

User wrote a constructor (pattern).

ConORec

User wrote a record (pattern).

bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin #

Prefer user-written over system-inserted.

Infixity, access, abstract, etc.

data IsInfix #

Functions can be defined in both infix and prefix style. See LHS.

Constructors

InfixDef 
PrefixDef 

data Access #

Access modifier.

Constructors

PrivateAccess Origin

Store the Origin of the private block that lead to this qualifier. This is needed for more faithful printing of declarations.

PublicAccess 
OnlyQualified

Visible from outside, but not exported when opening the module Used for qualified constructors.

data IsMacro #

Is this a macro definition?

Constructors

MacroDef 
NotMacroDef 

type Nat = Int #

type Arity = Nat #

NameId

data NameId #

The unique identifier of a name. Second argument is the top-level module identifier.

Constructors

NameId !Word64 !Word64 

Instances

Enum NameId # 
Eq NameId # 

Methods

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

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

Ord NameId # 
Show NameId # 
Generic NameId # 

Associated Types

type Rep NameId :: * -> * #

Methods

from :: NameId -> Rep NameId x #

to :: Rep NameId x -> NameId #

NFData NameId # 

Methods

rnf :: NameId -> () #

Hashable NameId # 

Methods

hashWithSalt :: Int -> NameId -> Int #

hash :: NameId -> Int #

KillRange NameId # 
HasFresh NameId # 
type Rep NameId # 
type Rep NameId = D1 (MetaData "NameId" "Agda.Syntax.Common" "Agda-2.5.2-75ei4uCcbjhBaJJCNAC8Q3" False) (C1 (MetaCons "NameId" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) SourceUnpack SourceStrict DecidedUnpack) (Rec0 Word64)) (S1 (MetaSel (Nothing Symbol) SourceUnpack SourceStrict DecidedUnpack) (Rec0 Word64))))

Meta variables

newtype MetaId #

A meta variable identifier is just a natural number.

Constructors

MetaId 

Fields

Instances

Enum MetaId # 
Eq MetaId # 

Methods

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

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

Integral MetaId # 
Num MetaId # 
Ord MetaId # 
Real MetaId # 
Show MetaId #

Show non-record version of this newtype.

NFData MetaId # 

Methods

rnf :: MetaId -> () #

Pretty MetaId # 

Methods

pretty :: MetaId -> Doc #

prettyPrec :: Int -> MetaId -> Doc #

GetDefs MetaId # 

Methods

getDefs :: MonadGetDefs m => MetaId -> m () #

HasFresh MetaId # 
UnFreezeMeta MetaId # 

Methods

unfreezeMeta :: MetaId -> TCM () #

IsInstantiatedMeta MetaId # 
PrettyTCM MetaId # 

Methods

prettyTCM :: MetaId -> TCM Doc #

FromTerm MetaId # 
ToTerm MetaId # 

Methods

toTerm :: TCM (MetaId -> Term) #

toTermR :: TCM (MetaId -> ReduceM Term) #

PrimTerm MetaId # 

Methods

primTerm :: MetaId -> TCM Term #

Unquote MetaId # 
Reify MetaId Expr # 

Methods

reify :: MetaId -> TCM Expr #

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

Placeholders (used to parse sections)

data PositionInName #

The position of a name part or underscore in a name.

Constructors

Beginning

The following underscore is at the beginning of the name: _foo.

Middle

The following underscore is in the middle of the name: foo_bar.

End

The following underscore is at the end of the name: foo_.

data MaybePlaceholder e #

Placeholders are used to represent the underscores in a section.

Constructors

Placeholder !PositionInName 
NoPlaceholder !(Maybe PositionInName) e

The second argument is used only (but not always) for name parts other than underscores.

Instances

Functor MaybePlaceholder # 

Methods

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

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

Foldable MaybePlaceholder # 

Methods

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

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

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

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

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

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

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

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

toList :: MaybePlaceholder a -> [a] #

null :: MaybePlaceholder a -> Bool #

length :: MaybePlaceholder a -> Int #

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

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

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

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

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

Traversable MaybePlaceholder # 

Methods

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

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

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

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

Eq e => Eq (MaybePlaceholder e) # 
Ord e => Ord (MaybePlaceholder e) # 
Show e => Show (MaybePlaceholder e) # 
NFData a => NFData (MaybePlaceholder a) # 

Methods

rnf :: MaybePlaceholder a -> () #

KillRange a => KillRange (MaybePlaceholder a) # 
HasRange a => HasRange (MaybePlaceholder a) # 
ExprLike a => ExprLike (MaybePlaceholder a) # 

Methods

mapExpr :: (Expr -> Expr) -> MaybePlaceholder a -> MaybePlaceholder a #

traverseExpr :: Monad m => (Expr -> m Expr) -> MaybePlaceholder a -> m (MaybePlaceholder a) #

foldExpr :: Monoid m => (Expr -> m) -> MaybePlaceholder a -> m #

noPlaceholder :: e -> MaybePlaceholder e #

An abbreviation: noPlaceholder = NoPlaceholder Nothing.

Interaction meta variables

newtype InteractionId #

Constructors

InteractionId 

Fields

Instances

Enum InteractionId # 
Eq InteractionId # 
Integral InteractionId # 
Num InteractionId # 
Ord InteractionId # 
Real InteractionId # 
Show InteractionId # 
KillRange InteractionId # 
HasFresh InteractionId # 
ToConcrete InteractionId Expr # 

Import directive

data ImportDirective' a b #

The things you are allowed to say when you shuffle names between name spaces (i.e. in import, namespace, or open declarations).

Constructors

ImportDirective 

Fields

Instances

(Eq b, Eq a) => Eq (ImportDirective' a b) # 
(NFData a, NFData b) => NFData (ImportDirective' a b) #

Ranges are not forced.

Methods

rnf :: ImportDirective' a b -> () #

(KillRange a, KillRange b) => KillRange (ImportDirective' a b) # 
(HasRange a, HasRange b) => HasRange (ImportDirective' a b) # 

Methods

getRange :: ImportDirective' a b -> Range #

data Using' a b #

Constructors

UseEverything 
Using [ImportedName' a b] 

Instances

(Eq b, Eq a) => Eq (Using' a b) # 

Methods

(==) :: Using' a b -> Using' a b -> Bool #

(/=) :: Using' a b -> Using' a b -> Bool #

Semigroup (Using' a b) # 

Methods

(<>) :: Using' a b -> Using' a b -> Using' a b #

sconcat :: NonEmpty (Using' a b) -> Using' a b #

stimes :: Integral b => b -> Using' a b -> Using' a b #

Monoid (Using' a b) # 

Methods

mempty :: Using' a b #

mappend :: Using' a b -> Using' a b -> Using' a b #

mconcat :: [Using' a b] -> Using' a b #

(NFData a, NFData b) => NFData (Using' a b) # 

Methods

rnf :: Using' a b -> () #

(KillRange a, KillRange b) => KillRange (Using' a b) # 

Methods

killRange :: KillRangeT (Using' a b) #

(HasRange a, HasRange b) => HasRange (Using' a b) # 

Methods

getRange :: Using' a b -> Range #

defaultImportDir :: ImportDirective' a b #

Default is directive is private (use everything, but do not export).

data ImportedName' a b #

An imported name can be a module or a defined name

Constructors

ImportedModule b 
ImportedName a 

Instances

(Eq a, Eq b) => Eq (ImportedName' a b) # 

Methods

(==) :: ImportedName' a b -> ImportedName' a b -> Bool #

(/=) :: ImportedName' a b -> ImportedName' a b -> Bool #

(Ord a, Ord b) => Ord (ImportedName' a b) # 
(Show a, Show b) => Show (ImportedName' a b) # 
(NFData a, NFData b) => NFData (ImportedName' a b) # 

Methods

rnf :: ImportedName' a b -> () #

(KillRange a, KillRange b) => KillRange (ImportedName' a b) # 
(HasRange a, HasRange b) => HasRange (ImportedName' a b) # 

Methods

getRange :: ImportedName' a b -> Range #

data Renaming' a b #

Constructors

Renaming 

Fields

Instances

(Eq b, Eq a) => Eq (Renaming' a b) # 

Methods

(==) :: Renaming' a b -> Renaming' a b -> Bool #

(/=) :: Renaming' a b -> Renaming' a b -> Bool #

(NFData a, NFData b) => NFData (Renaming' a b) #

Ranges are not forced.

Methods

rnf :: Renaming' a b -> () #

(KillRange a, KillRange b) => KillRange (Renaming' a b) # 
(HasRange a, HasRange b) => HasRange (Renaming' a b) # 

Methods

getRange :: Renaming' a b -> Range #

HasRange instances

KillRange instances

NFData instances

Termination

data TerminationCheck m #

Termination check? (Default = TerminationCheck).

Constructors

TerminationCheck

Run the termination checker.

NoTerminationCheck

Skip termination checking (unsafe).

NonTerminating

Treat as non-terminating.

Terminating

Treat as terminating (unsafe). Same effect as NoTerminationCheck.

TerminationMeasure Range m

Skip termination checking but use measure instead.

Positivity

type PositivityCheck = Bool #

Positivity check? (Default = True).