Agda.Syntax.Common

Some common syntactic entities are defined in this module.

Delayed

data Delayed

Used to specify whether something should be delayed.

Constructors

Delayed

NotDelayed

Instances

Eq Delayed

Methods

(==) :: Delayed -> Delayed -> Bool

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

Ord Delayed

Methods

compare :: Delayed -> Delayed -> Ordering

(<) :: Delayed -> Delayed -> Bool

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

(>) :: Delayed -> Delayed -> Bool

(>=) :: Delayed -> Delayed -> Bool

max :: Delayed -> Delayed -> Delayed

min :: Delayed -> Delayed -> Delayed

Show Delayed

Methods

showsPrec :: Int -> Delayed -> ShowS

show :: Delayed -> String

showList :: [Delayed] -> ShowS

KillRange Delayed

Methods

killRange :: KillRangeT Delayed

Induction

data Induction

Constructors

Inductive

CoInductive

Instances

Eq Induction

Methods

(==) :: Induction -> Induction -> Bool

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

Ord Induction

Methods

compare :: Induction -> Induction -> Ordering

(<) :: Induction -> Induction -> Bool

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

(>) :: Induction -> Induction -> Bool

(>=) :: Induction -> Induction -> Bool

max :: Induction -> Induction -> Induction

min :: Induction -> Induction -> Induction

Show Induction

Methods

showsPrec :: Int -> Induction -> ShowS

show :: Induction -> String

showList :: [Induction] -> ShowS

NFData Induction

Methods

rnf :: Induction -> ()

KillRange Induction

Methods

killRange :: KillRangeT Induction

HasRange Induction

Methods

getRange :: Induction -> Range

Hiding

data Hiding

Constructors

Hidden

Instance

NotHidden

Instances

Eq Hiding

Methods

(==) :: Hiding -> Hiding -> Bool

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

Ord Hiding

Methods

compare :: Hiding -> Hiding -> Ordering

(<) :: Hiding -> Hiding -> Bool

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

(>) :: Hiding -> Hiding -> Bool

(>=) :: Hiding -> Hiding -> Bool

max :: Hiding -> Hiding -> Hiding

min :: Hiding -> Hiding -> Hiding

Show Hiding

Methods

showsPrec :: Int -> Hiding -> ShowS

show :: Hiding -> String

showList :: [Hiding] -> ShowS

Semigroup Hiding

Hiding is an idempotent partial monoid, with unit NotHidden. Instance and NotHidden are incompatible.

Methods

(<>) :: Hiding -> Hiding -> Hiding

sconcat :: NonEmpty Hiding -> Hiding

stimes :: Integral b => b -> Hiding -> Hiding

Monoid Hiding

Methods

mempty :: Hiding

mappend :: Hiding -> Hiding -> Hiding

mconcat :: [Hiding] -> Hiding

NFData Hiding

Methods

rnf :: Hiding -> ()

KillRange Hiding

Methods

killRange :: KillRangeT Hiding

LensHiding Hiding

Methods

getHiding :: Hiding -> Hiding

setHiding :: Hiding -> Hiding -> Hiding

mapHiding :: (Hiding -> Hiding) -> Hiding -> Hiding

ChooseFlex Hiding

Methods

chooseFlex :: Hiding -> Hiding -> FlexChoice

Unquote Hiding

Methods

unquote :: Term -> UnquoteM Hiding

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)

Methods

compare :: WithHiding a -> WithHiding a -> Ordering

(<) :: WithHiding a -> WithHiding a -> Bool

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

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

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

max :: WithHiding a -> WithHiding a -> WithHiding a

min :: WithHiding a -> WithHiding a -> WithHiding a

Show a => Show (WithHiding a)

Methods

showsPrec :: Int -> WithHiding a -> ShowS

show :: WithHiding a -> String

showList :: [WithHiding a] -> ShowS

NFData a => NFData (WithHiding a)

Methods

rnf :: WithHiding a -> ()

KillRange a => KillRange (WithHiding a)

Methods

killRange :: KillRangeT (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)

Methods

getHiding :: WithHiding a -> Hiding

setHiding :: Hiding -> WithHiding a -> WithHiding a

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

PrettyTCM a => PrettyTCM (WithHiding a)

Methods

prettyTCM :: WithHiding a -> TCM Doc

ToConcrete a c => ToConcrete (WithHiding a) (WithHiding c)

Methods

toConcrete :: WithHiding a -> AbsToCon (WithHiding c)

bindToConcrete :: WithHiding a -> (WithHiding c -> AbsToCon b) -> AbsToCon b

ToAbstract c a => ToAbstract (WithHiding c) (WithHiding a)

Methods

toAbstract :: WithHiding c -> ScopeM (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

Methods

getHiding :: ArgInfo -> Hiding

setHiding :: Hiding -> ArgInfo -> ArgInfo

mapHiding :: (Hiding -> Hiding) -> ArgInfo -> ArgInfo

LensHiding Hiding

Methods

getHiding :: Hiding -> Hiding

setHiding :: Hiding -> Hiding -> Hiding

mapHiding :: (Hiding -> Hiding) -> Hiding -> Hiding

LensHiding TypedBindings

Methods

getHiding :: TypedBindings -> Hiding

setHiding :: Hiding -> TypedBindings -> TypedBindings

mapHiding :: (Hiding -> Hiding) -> TypedBindings -> TypedBindings

LensHiding LamBinding

Methods

getHiding :: LamBinding -> Hiding

setHiding :: Hiding -> LamBinding -> LamBinding

mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding

LensHiding TypedBindings

Methods

getHiding :: TypedBindings -> Hiding

setHiding :: Hiding -> TypedBindings -> TypedBindings

mapHiding :: (Hiding -> Hiding) -> TypedBindings -> TypedBindings

LensHiding LamBinding

Methods

getHiding :: LamBinding -> Hiding

setHiding :: Hiding -> LamBinding -> LamBinding

mapHiding :: (Hiding -> Hiding) -> LamBinding -> 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)

Methods

getHiding :: WithHiding a -> Hiding

setHiding :: Hiding -> WithHiding a -> WithHiding a

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

LensHiding (FlexibleVar a)

Methods

getHiding :: FlexibleVar a -> Hiding

setHiding :: Hiding -> FlexibleVar a -> FlexibleVar a

mapHiding :: (Hiding -> Hiding) -> FlexibleVar a -> 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

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

Instances

Eq Relevance

Methods

(==) :: Relevance -> Relevance -> Bool

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

Ord Relevance

Methods

compare :: Relevance -> Relevance -> Ordering

(<) :: Relevance -> Relevance -> Bool

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

(>) :: Relevance -> Relevance -> Bool

(>=) :: Relevance -> Relevance -> Bool

max :: Relevance -> Relevance -> Relevance

min :: Relevance -> Relevance -> Relevance

Show Relevance

Methods

showsPrec :: Int -> Relevance -> ShowS

show :: Relevance -> String

showList :: [Relevance] -> ShowS

NFData Relevance

Methods

rnf :: Relevance -> ()

KillRange Relevance

Methods

killRange :: KillRangeT Relevance

LensRelevance Relevance

Methods

getRelevance :: Relevance -> Relevance

setRelevance :: Relevance -> Relevance -> Relevance

mapRelevance :: (Relevance -> Relevance) -> Relevance -> Relevance

PrettyTCM Relevance

Methods

prettyTCM :: Relevance -> TCM Doc

Unquote Relevance

Methods

unquote :: Term -> UnquoteM Relevance

allRelevances :: [Relevance]

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

Instances

LensRelevance ArgInfo

Methods

getRelevance :: ArgInfo -> Relevance

setRelevance :: Relevance -> ArgInfo -> ArgInfo

mapRelevance :: (Relevance -> Relevance) -> ArgInfo -> ArgInfo

LensRelevance Relevance

Methods

getRelevance :: Relevance -> Relevance

setRelevance :: Relevance -> Relevance -> Relevance

mapRelevance :: (Relevance -> Relevance) -> Relevance -> Relevance

LensRelevance TypedBindings

Methods

getRelevance :: TypedBindings -> Relevance

setRelevance :: Relevance -> TypedBindings -> TypedBindings

mapRelevance :: (Relevance -> Relevance) -> TypedBindings -> TypedBindings

LensRelevance (Dom e)

Methods

getRelevance :: Dom e -> Relevance

setRelevance :: Relevance -> Dom e -> Dom e

mapRelevance :: (Relevance -> Relevance) -> Dom e -> Dom e

LensRelevance (Arg e)

Methods

getRelevance :: Arg e -> Relevance

setRelevance :: Relevance -> Arg e -> Arg e

mapRelevance :: (Relevance -> Relevance) -> Arg e -> Arg e

isRelevant :: LensRelevance a => a -> Bool

isIrrelevant :: LensRelevance a => a -> Bool

moreRelevant :: Relevance -> Relevance -> Bool

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

irrelevantOrUnused :: Relevance -> Bool

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

nonStrictToIrr :: Relevance -> Relevance

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

data Origin

Constructors

UserWritten

Inserted

Reflected

Instances

Eq Origin

Methods

(==) :: Origin -> Origin -> Bool

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

Ord Origin

Methods

compare :: Origin -> Origin -> Ordering

(<) :: Origin -> Origin -> Bool

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

(>) :: Origin -> Origin -> Bool

(>=) :: Origin -> Origin -> Bool

max :: Origin -> Origin -> Origin

min :: Origin -> Origin -> Origin

Show Origin

Methods

showsPrec :: Int -> Origin -> ShowS

show :: Origin -> String

showList :: [Origin] -> ShowS

NFData Origin

Methods

rnf :: Origin -> ()

KillRange Origin

Methods

killRange :: KillRangeT Origin

LensOrigin Origin

Methods

getOrigin :: Origin -> Origin

setOrigin :: Origin -> Origin -> Origin

mapOrigin :: (Origin -> Origin) -> Origin -> Origin

class LensOrigin a where

Minimal complete definition

getOrigin

Methods

getOrigin :: a -> Origin

setOrigin :: Origin -> a -> a

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

Instances

LensOrigin ArgInfo

Methods

getOrigin :: ArgInfo -> Origin

setOrigin :: Origin -> ArgInfo -> ArgInfo

mapOrigin :: (Origin -> Origin) -> ArgInfo -> ArgInfo

LensOrigin Origin

Methods

getOrigin :: Origin -> Origin

setOrigin :: Origin -> Origin -> Origin

mapOrigin :: (Origin -> Origin) -> Origin -> Origin

LensOrigin (Arg e)

Methods

getOrigin :: Arg e -> Origin

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

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

Argument decoration

data ArgInfo

A function argument can be hidden and/or irrelevant.

Constructors

ArgInfo

Fields

• argInfoHiding :: Hiding
• argInfoRelevance :: Relevance
• argInfoOrigin :: Origin
• argInfoOverlappable :: Bool

Instances

Eq ArgInfo

Methods

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

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

Ord ArgInfo

Methods

compare :: ArgInfo -> ArgInfo -> Ordering

(<) :: ArgInfo -> ArgInfo -> Bool

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

(>) :: ArgInfo -> ArgInfo -> Bool

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

max :: ArgInfo -> ArgInfo -> ArgInfo

min :: ArgInfo -> ArgInfo -> ArgInfo

Show ArgInfo

Methods

showsPrec :: Int -> ArgInfo -> ShowS

show :: ArgInfo -> String

showList :: [ArgInfo] -> ShowS

NFData ArgInfo

Methods

rnf :: ArgInfo -> ()

KillRange ArgInfo

Methods

killRange :: KillRangeT ArgInfo

LensArgInfo ArgInfo

Methods

getArgInfo :: ArgInfo -> ArgInfo

setArgInfo :: ArgInfo -> ArgInfo -> ArgInfo

mapArgInfo :: (ArgInfo -> ArgInfo) -> ArgInfo -> ArgInfo

LensOrigin ArgInfo

Methods

getOrigin :: ArgInfo -> Origin

setOrigin :: Origin -> ArgInfo -> ArgInfo

mapOrigin :: (Origin -> Origin) -> ArgInfo -> ArgInfo

LensRelevance ArgInfo

Methods

getRelevance :: ArgInfo -> Relevance

setRelevance :: Relevance -> ArgInfo -> ArgInfo

mapRelevance :: (Relevance -> Relevance) -> ArgInfo -> ArgInfo

LensHiding ArgInfo

Methods

getHiding :: ArgInfo -> Hiding

setHiding :: Hiding -> ArgInfo -> ArgInfo

mapHiding :: (Hiding -> Hiding) -> ArgInfo -> ArgInfo

SynEq ArgInfo

Methods

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

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

ToTerm ArgInfo

Methods

toTerm :: TCM (ArgInfo -> Term)

toTermR :: TCM (ArgInfo -> ReduceM Term)

Unquote ArgInfo

Methods

unquote :: Term -> UnquoteM ArgInfo

class LensArgInfo a where

Minimal complete definition

getArgInfo

Methods

getArgInfo :: a -> ArgInfo

setArgInfo :: ArgInfo -> a -> a

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

Instances

LensArgInfo ArgInfo

Methods

getArgInfo :: ArgInfo -> ArgInfo

setArgInfo :: ArgInfo -> ArgInfo -> ArgInfo

mapArgInfo :: (ArgInfo -> ArgInfo) -> ArgInfo -> ArgInfo

LensArgInfo (Dom e)

Methods

getArgInfo :: Dom e -> ArgInfo

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

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

LensArgInfo (Arg a)

Methods

getArgInfo :: Arg a -> ArgInfo

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

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

defaultArgInfo :: ArgInfo

Arguments

data Arg e

Constructors

Arg

Fields

• argInfo :: ArgInfo
• unArg :: e

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)

Methods

getRelevance :: Arg e -> Relevance

setRelevance :: Relevance -> Arg e -> Arg e

mapRelevance :: (Relevance -> Relevance) -> Arg e -> 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)

Methods

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

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)

Methods

maybePostfixProjP :: Arg a -> Maybe (ProjOrigin, AmbiguousQName)

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)

Methods

isInstantiatedMeta :: Arg a -> TCM Bool

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)

Methods

(<:) :: Arg a -> Arg a -> ReaderT * (Map QName InjectiveFun) (Compile TCM) InjConstraints

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)

Methods

occurrences :: Arg a -> OccM OccurrencesBuilder

RaiseNLP a => RaiseNLP (Arg a)

Methods

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

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

NoProjectedVar a => NoProjectedVar (Arg a)

Methods

noProjectedVar :: Arg a -> Either ProjVarExc ()

AbsTerm a => AbsTerm (Arg a)

Methods

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

IsFlexiblePattern a => IsFlexiblePattern (Arg a)

Methods

maybeFlexiblePattern :: Arg a -> MaybeT TCM FlexibleVarKind

isFlexiblePattern :: Arg a -> TCM Bool

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]

Methods

toAbstract :: [Arg Term] -> WithNames [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

class Eq a => Underscore a where

Minimal complete definition

underscore

Methods

underscore :: a

isUnderscore :: a -> Bool

Instances

Underscore String

Methods

underscore :: String

isUnderscore :: String -> Bool

Underscore ByteString

Methods

underscore :: ByteString

isUnderscore :: ByteString -> Bool

Underscore Doc

Methods

underscore :: Doc

isUnderscore :: Doc -> Bool

Underscore QName

Methods

underscore :: QName

isUnderscore :: QName -> Bool

Underscore Name

Methods

underscore :: Name

isUnderscore :: Name -> Bool

Underscore Expr

Methods

underscore :: Expr

isUnderscore :: Expr -> Bool

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

• domInfo :: ArgInfo
• unDom :: e

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

Methods

reduce' :: Telescope -> ReduceM Telescope

reduceB' :: Telescope -> ReduceM (Blocked Telescope)

Instantiate Telescope

Methods

instantiate' :: Telescope -> ReduceM Telescope

Reify Telescope Telescope

Methods

reify :: Telescope -> TCM Telescope

reifyWhen :: Bool -> Telescope -> TCM 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)

Methods

getRelevance :: Dom e -> Relevance

setRelevance :: Relevance -> Dom e -> Dom e

mapRelevance :: (Relevance -> Relevance) -> Dom e -> 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)

Methods

occurrences :: Dom a -> OccM OccurrencesBuilder

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

Methods

toAbstract :: (Dom r, Name) -> WithNames 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

• nameOf :: Maybe name
• namedThing :: a

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]

Methods

toAbstract :: [Arg Term] -> WithNames [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)

Methods

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

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)

Methods

maybePostfixProjP :: Named n a -> Maybe (ProjOrigin, AmbiguousQName)

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)

Methods

maybeFlexiblePattern :: Named name a -> MaybeT TCM FlexibleVarKind

isFlexiblePattern :: Named name a -> TCM Bool

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.

defaultNamedArg :: a -> NamedArg a

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

• rangeOf :: Range
• rangedThing :: a

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

Methods

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)

Methods

killRange :: KillRangeT (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]

Methods

toAbstract :: [Arg Term] -> WithNames [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.

rawNameToString :: RawName -> String

stringToRawName :: String -> RawName

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

Instances

Bounded ConOrigin

Methods

minBound :: ConOrigin

maxBound :: ConOrigin

Enum ConOrigin

Methods

succ :: ConOrigin -> ConOrigin

pred :: ConOrigin -> ConOrigin

toEnum :: Int -> ConOrigin

fromEnum :: ConOrigin -> Int

enumFrom :: ConOrigin -> [ConOrigin]

enumFromThen :: ConOrigin -> ConOrigin -> [ConOrigin]

enumFromTo :: ConOrigin -> ConOrigin -> [ConOrigin]

enumFromThenTo :: ConOrigin -> ConOrigin -> ConOrigin -> [ConOrigin]

Eq ConOrigin

Methods

(==) :: ConOrigin -> ConOrigin -> Bool

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

Ord ConOrigin

Methods

compare :: ConOrigin -> ConOrigin -> Ordering

(<) :: ConOrigin -> ConOrigin -> Bool

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

(>) :: ConOrigin -> ConOrigin -> Bool

(>=) :: ConOrigin -> ConOrigin -> Bool

max :: ConOrigin -> ConOrigin -> ConOrigin

min :: ConOrigin -> ConOrigin -> ConOrigin

Show ConOrigin

Methods

showsPrec :: Int -> ConOrigin -> ShowS

show :: ConOrigin -> String

showList :: [ConOrigin] -> ShowS

KillRange ConOrigin

Methods

killRange :: KillRangeT ConOrigin

bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin

Prefer user-written over system-inserted.

data ProjOrigin

Where does a projection come from?

Constructors

ProjPrefix

User wrote a prefix projection.

ProjPostfix

User wrote a postfix projection.

ProjSystem

Projection was generated by the system.

Instances

Bounded ProjOrigin

Methods

minBound :: ProjOrigin

maxBound :: ProjOrigin

Enum ProjOrigin

Methods

succ :: ProjOrigin -> ProjOrigin

pred :: ProjOrigin -> ProjOrigin

toEnum :: Int -> ProjOrigin

fromEnum :: ProjOrigin -> Int

enumFrom :: ProjOrigin -> [ProjOrigin]

enumFromThen :: ProjOrigin -> ProjOrigin -> [ProjOrigin]

enumFromTo :: ProjOrigin -> ProjOrigin -> [ProjOrigin]

enumFromThenTo :: ProjOrigin -> ProjOrigin -> ProjOrigin -> [ProjOrigin]

Eq ProjOrigin

Methods

(==) :: ProjOrigin -> ProjOrigin -> Bool

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

Ord ProjOrigin

Methods

compare :: ProjOrigin -> ProjOrigin -> Ordering

(<) :: ProjOrigin -> ProjOrigin -> Bool

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

(>) :: ProjOrigin -> ProjOrigin -> Bool

(>=) :: ProjOrigin -> ProjOrigin -> Bool

max :: ProjOrigin -> ProjOrigin -> ProjOrigin

min :: ProjOrigin -> ProjOrigin -> ProjOrigin

Show ProjOrigin

Methods

showsPrec :: Int -> ProjOrigin -> ShowS

show :: ProjOrigin -> String

showList :: [ProjOrigin] -> ShowS

KillRange ProjOrigin

Methods

killRange :: KillRangeT ProjOrigin

Infixity, access, abstract, etc.

data IsInfix

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

Constructors

InfixDef

PrefixDef

Instances

Eq IsInfix

Methods

(==) :: IsInfix -> IsInfix -> Bool

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

Ord IsInfix

Methods

compare :: IsInfix -> IsInfix -> Ordering

(<) :: IsInfix -> IsInfix -> Bool

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

(>) :: IsInfix -> IsInfix -> Bool

(>=) :: IsInfix -> IsInfix -> Bool

max :: IsInfix -> IsInfix -> IsInfix

min :: IsInfix -> IsInfix -> IsInfix

Show IsInfix

Methods

showsPrec :: Int -> IsInfix -> ShowS

show :: IsInfix -> String

showList :: [IsInfix] -> ShowS

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.

Instances

Eq Access

Methods

(==) :: Access -> Access -> Bool

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

Ord Access

Methods

compare :: Access -> Access -> Ordering

(<) :: Access -> Access -> Bool

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

(>) :: Access -> Access -> Bool

(>=) :: Access -> Access -> Bool

max :: Access -> Access -> Access

min :: Access -> Access -> Access

Show Access

Methods

showsPrec :: Int -> Access -> ShowS

show :: Access -> String

showList :: [Access] -> ShowS

NFData Access

Methods

rnf :: Access -> ()

KillRange Access

Methods

killRange :: KillRangeT Access

HasRange Access

Methods

getRange :: Access -> Range

data IsAbstract

Abstract or concrete

Constructors

AbstractDef

ConcreteDef

Instances

Eq IsAbstract

Methods

(==) :: IsAbstract -> IsAbstract -> Bool

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

Ord IsAbstract

Methods

compare :: IsAbstract -> IsAbstract -> Ordering

(<) :: IsAbstract -> IsAbstract -> Bool

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

(>) :: IsAbstract -> IsAbstract -> Bool

(>=) :: IsAbstract -> IsAbstract -> Bool

max :: IsAbstract -> IsAbstract -> IsAbstract

min :: IsAbstract -> IsAbstract -> IsAbstract

Show IsAbstract

Methods

showsPrec :: Int -> IsAbstract -> ShowS

show :: IsAbstract -> String

showList :: [IsAbstract] -> ShowS

KillRange IsAbstract

Methods

killRange :: KillRangeT IsAbstract

data IsInstance

Is this definition eligible for instance search?

Constructors

InstanceDef

NotInstanceDef

Instances

Eq IsInstance

Methods

(==) :: IsInstance -> IsInstance -> Bool

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

Ord IsInstance

Methods

compare :: IsInstance -> IsInstance -> Ordering

(<) :: IsInstance -> IsInstance -> Bool

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

(>) :: IsInstance -> IsInstance -> Bool

(>=) :: IsInstance -> IsInstance -> Bool

max :: IsInstance -> IsInstance -> IsInstance

min :: IsInstance -> IsInstance -> IsInstance

Show IsInstance

Methods

showsPrec :: Int -> IsInstance -> ShowS

show :: IsInstance -> String

showList :: [IsInstance] -> ShowS

NFData IsInstance

Methods

rnf :: IsInstance -> ()

KillRange IsInstance

Methods

killRange :: KillRangeT IsInstance

HasRange IsInstance

Methods

getRange :: IsInstance -> Range

data IsMacro

Is this a macro definition?

Constructors

MacroDef

NotMacroDef

Instances

Eq IsMacro

Methods

(==) :: IsMacro -> IsMacro -> Bool

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

Ord IsMacro

Methods

compare :: IsMacro -> IsMacro -> Ordering

(<) :: IsMacro -> IsMacro -> Bool

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

(>) :: IsMacro -> IsMacro -> Bool

(>=) :: IsMacro -> IsMacro -> Bool

max :: IsMacro -> IsMacro -> IsMacro

min :: IsMacro -> IsMacro -> IsMacro

Show IsMacro

Methods

showsPrec :: Int -> IsMacro -> ShowS

show :: IsMacro -> String

showList :: [IsMacro] -> ShowS

KillRange IsMacro

Methods

killRange :: KillRangeT IsMacro

HasRange IsMacro

Methods

getRange :: IsMacro -> Range

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

Methods

succ :: NameId -> NameId

pred :: NameId -> NameId

toEnum :: Int -> NameId

fromEnum :: NameId -> Int

enumFrom :: NameId -> [NameId]

enumFromThen :: NameId -> NameId -> [NameId]

enumFromTo :: NameId -> NameId -> [NameId]

enumFromThenTo :: NameId -> NameId -> NameId -> [NameId]

Eq NameId

Methods

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

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

Ord NameId

Methods

compare :: NameId -> NameId -> Ordering

(<) :: NameId -> NameId -> Bool

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

(>) :: NameId -> NameId -> Bool

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

max :: NameId -> NameId -> NameId

min :: NameId -> NameId -> NameId

Show NameId

Methods

showsPrec :: Int -> NameId -> ShowS

show :: NameId -> String

showList :: [NameId] -> ShowS

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

Methods

killRange :: KillRangeT NameId

HasFresh NameId

Methods

freshLens :: Lens' NameId TCState

nextFresh' :: NameId -> NameId

type Rep NameId

type Rep NameId = D1 (MetaData "NameId" "Agda.Syntax.Common" "Agda-2.5.2-77GgoQxcAuy1fEffAhivOO" False) (C1 (MetaCons "NameId" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) SourceUnpack SourceStrict DecidedStrict) (Rec0 Word64)) (S1 (MetaSel (Nothing Symbol) SourceUnpack SourceStrict DecidedStrict) (Rec0 Word64))))

Meta variables

newtype MetaId

A meta variable identifier is just a natural number.

Constructors

MetaId

Fields

• metaId :: Nat

Instances

Enum MetaId

Methods

succ :: MetaId -> MetaId

pred :: MetaId -> MetaId

toEnum :: Int -> MetaId

fromEnum :: MetaId -> Int

enumFrom :: MetaId -> [MetaId]

enumFromThen :: MetaId -> MetaId -> [MetaId]

enumFromTo :: MetaId -> MetaId -> [MetaId]

enumFromThenTo :: MetaId -> MetaId -> MetaId -> [MetaId]

Eq MetaId

Methods

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

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

Integral MetaId

Methods

quot :: MetaId -> MetaId -> MetaId

rem :: MetaId -> MetaId -> MetaId

div :: MetaId -> MetaId -> MetaId

mod :: MetaId -> MetaId -> MetaId

quotRem :: MetaId -> MetaId -> (MetaId, MetaId)

divMod :: MetaId -> MetaId -> (MetaId, MetaId)

toInteger :: MetaId -> Integer

Num MetaId

Methods

(+) :: MetaId -> MetaId -> MetaId

(-) :: MetaId -> MetaId -> MetaId

(*) :: MetaId -> MetaId -> MetaId

negate :: MetaId -> MetaId

abs :: MetaId -> MetaId

signum :: MetaId -> MetaId

fromInteger :: Integer -> MetaId

Ord MetaId

Methods

compare :: MetaId -> MetaId -> Ordering

(<) :: MetaId -> MetaId -> Bool

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

(>) :: MetaId -> MetaId -> Bool

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

max :: MetaId -> MetaId -> MetaId

min :: MetaId -> MetaId -> MetaId

Real MetaId

Methods

toRational :: MetaId -> Rational

Show MetaId

Show non-record version of this newtype.

Methods

showsPrec :: Int -> MetaId -> ShowS

show :: MetaId -> String

showList :: [MetaId] -> ShowS

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

Methods

freshLens :: Lens' MetaId TCState

nextFresh' :: MetaId -> MetaId

UnFreezeMeta MetaId

Methods

unfreezeMeta :: MetaId -> TCM ()

IsInstantiatedMeta MetaId

Methods

isInstantiatedMeta :: MetaId -> TCM Bool

PrettyTCM MetaId

Methods

prettyTCM :: MetaId -> TCM Doc

FromTerm MetaId

Methods

fromTerm :: TCM (FromTermFunction MetaId)

ToTerm MetaId

Methods

toTerm :: TCM (MetaId -> Term)

toTermR :: TCM (MetaId -> ReduceM Term)

PrimTerm MetaId

Methods

primTerm :: MetaId -> TCM Term

Unquote MetaId

Methods

unquote :: Term -> UnquoteM MetaId

Reify MetaId Expr

Methods

reify :: MetaId -> TCM Expr

reifyWhen :: Bool -> MetaId -> TCM Expr

newtype Constr a

Constructors

Constr a

Instances

ToConcrete (Constr Constructor) Declaration

Methods

toConcrete :: Constr Constructor -> AbsToCon Declaration

bindToConcrete :: Constr Constructor -> (Declaration -> AbsToCon b) -> AbsToCon b

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

Instances

Eq PositionInName

Methods

(==) :: PositionInName -> PositionInName -> Bool

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

Ord PositionInName

Methods

compare :: PositionInName -> PositionInName -> Ordering

(<) :: PositionInName -> PositionInName -> Bool

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

(>) :: PositionInName -> PositionInName -> Bool

(>=) :: PositionInName -> PositionInName -> Bool

max :: PositionInName -> PositionInName -> PositionInName

min :: PositionInName -> PositionInName -> PositionInName

Show PositionInName

Methods

showsPrec :: Int -> PositionInName -> ShowS

show :: PositionInName -> String

showList :: [PositionInName] -> ShowS

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)

Methods

(==) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool

(/=) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool

Ord e => Ord (MaybePlaceholder e)

Methods

compare :: MaybePlaceholder e -> MaybePlaceholder e -> Ordering

(<) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool

(<=) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool

(>) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool

(>=) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool

max :: MaybePlaceholder e -> MaybePlaceholder e -> MaybePlaceholder e

min :: MaybePlaceholder e -> MaybePlaceholder e -> MaybePlaceholder e

Show e => Show (MaybePlaceholder e)

Methods

showsPrec :: Int -> MaybePlaceholder e -> ShowS

show :: MaybePlaceholder e -> String

showList :: [MaybePlaceholder e] -> ShowS

NFData a => NFData (MaybePlaceholder a)

Methods

rnf :: MaybePlaceholder a -> ()

KillRange a => KillRange (MaybePlaceholder a)

Methods

killRange :: KillRangeT (MaybePlaceholder a)

HasRange a => HasRange (MaybePlaceholder a)

Methods

getRange :: MaybePlaceholder a -> Range

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

• interactionId :: Nat

Instances

Enum InteractionId

Methods

succ :: InteractionId -> InteractionId

pred :: InteractionId -> InteractionId

toEnum :: Int -> InteractionId

fromEnum :: InteractionId -> Int

enumFrom :: InteractionId -> [InteractionId]

enumFromThen :: InteractionId -> InteractionId -> [InteractionId]

enumFromTo :: InteractionId -> InteractionId -> [InteractionId]

enumFromThenTo :: InteractionId -> InteractionId -> InteractionId -> [InteractionId]

Eq InteractionId

Methods

(==) :: InteractionId -> InteractionId -> Bool

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

Integral InteractionId

Methods

quot :: InteractionId -> InteractionId -> InteractionId

rem :: InteractionId -> InteractionId -> InteractionId

div :: InteractionId -> InteractionId -> InteractionId

mod :: InteractionId -> InteractionId -> InteractionId

quotRem :: InteractionId -> InteractionId -> (InteractionId, InteractionId)

divMod :: InteractionId -> InteractionId -> (InteractionId, InteractionId)

toInteger :: InteractionId -> Integer

Num InteractionId

Methods

(+) :: InteractionId -> InteractionId -> InteractionId

(-) :: InteractionId -> InteractionId -> InteractionId

(*) :: InteractionId -> InteractionId -> InteractionId

negate :: InteractionId -> InteractionId

abs :: InteractionId -> InteractionId

signum :: InteractionId -> InteractionId

fromInteger :: Integer -> InteractionId

Ord InteractionId

Methods

compare :: InteractionId -> InteractionId -> Ordering

(<) :: InteractionId -> InteractionId -> Bool

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

(>) :: InteractionId -> InteractionId -> Bool

(>=) :: InteractionId -> InteractionId -> Bool

max :: InteractionId -> InteractionId -> InteractionId

min :: InteractionId -> InteractionId -> InteractionId

Real InteractionId

Methods

toRational :: InteractionId -> Rational

Show InteractionId

Methods

showsPrec :: Int -> InteractionId -> ShowS

show :: InteractionId -> String

showList :: [InteractionId] -> ShowS

KillRange InteractionId

Methods

killRange :: KillRangeT InteractionId

HasFresh InteractionId

Methods

freshLens :: Lens' InteractionId TCState

nextFresh' :: InteractionId -> InteractionId

ToConcrete InteractionId Expr

Methods

toConcrete :: InteractionId -> AbsToCon Expr

bindToConcrete :: InteractionId -> (Expr -> AbsToCon b) -> AbsToCon b

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

• importDirRange :: Range
• using :: Using' a b
• hiding :: [ImportedName' a b]
• impRenaming :: [Renaming' a b]
• publicOpen :: Bool

  Only for open. Exports the opened names from the current module.

Instances

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

Methods

(==) :: ImportDirective' a b -> ImportDirective' a b -> Bool

(/=) :: ImportDirective' a b -> ImportDirective' a b -> Bool

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

Methods

killRange :: KillRangeT (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).

isDefaultImportDir :: ImportDirective' a b -> Bool

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)

Methods

compare :: ImportedName' a b -> ImportedName' a b -> Ordering

(<) :: ImportedName' a b -> ImportedName' a b -> Bool

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

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

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

max :: ImportedName' a b -> ImportedName' a b -> ImportedName' a b

min :: ImportedName' a b -> ImportedName' a b -> ImportedName' a b

(Show a, Show b) => Show (ImportedName' a b)

Methods

showsPrec :: Int -> ImportedName' a b -> ShowS

show :: ImportedName' a b -> String

showList :: [ImportedName' a b] -> ShowS

(NFData a, NFData b) => NFData (ImportedName' a b)

Methods

rnf :: ImportedName' a b -> ()

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

Methods

killRange :: KillRangeT (ImportedName' a b)

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

Methods

getRange :: ImportedName' a b -> Range

setImportedName :: ImportedName' a a -> a -> ImportedName' a a

data Renaming' a b

Constructors

Renaming

Fields

• renFrom :: ImportedName' a b

  Rename from this name.

• renTo :: ImportedName' a b

  To this one. Must be same kind as renFrom.

• renToRange :: Range

  The range of the "to" keyword. Retained for highlighting purposes.

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)

Methods

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

Instances

Functor TerminationCheck

Methods

fmap :: (a -> b) -> TerminationCheck a -> TerminationCheck b

(<$) :: a -> TerminationCheck b -> TerminationCheck a

Eq m => Eq (TerminationCheck m)

Methods

(==) :: TerminationCheck m -> TerminationCheck m -> Bool

(/=) :: TerminationCheck m -> TerminationCheck m -> Bool

Show m => Show (TerminationCheck m)

Methods

showsPrec :: Int -> TerminationCheck m -> ShowS

show :: TerminationCheck m -> String

showList :: [TerminationCheck m] -> ShowS

NFData a => NFData (TerminationCheck a)

Methods

rnf :: TerminationCheck a -> ()

KillRange m => KillRange (TerminationCheck m)

Methods

killRange :: KillRangeT (TerminationCheck m)

Positivity

type PositivityCheck = Bool

Positivity check? (Default = True).