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

Data Delayed

Methods

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

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

toConstr :: Delayed -> Constr

dataTypeOf :: Delayed -> DataType

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

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

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

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

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

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

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

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

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

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

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

Data Induction

Methods

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

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

toConstr :: Induction -> Constr

dataTypeOf :: Induction -> DataType

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

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

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

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

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

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

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

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

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

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

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 Overlappable

Constructors

YesOverlap

NoOverlap

Instances

Eq Overlappable

Methods

(==) :: Overlappable -> Overlappable -> Bool

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

Data Overlappable

Methods

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

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

toConstr :: Overlappable -> Constr

dataTypeOf :: Overlappable -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Overlappable

Methods

compare :: Overlappable -> Overlappable -> Ordering

(<) :: Overlappable -> Overlappable -> Bool

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

(>) :: Overlappable -> Overlappable -> Bool

(>=) :: Overlappable -> Overlappable -> Bool

max :: Overlappable -> Overlappable -> Overlappable

min :: Overlappable -> Overlappable -> Overlappable

Show Overlappable

Methods

showsPrec :: Int -> Overlappable -> ShowS

show :: Overlappable -> String

showList :: [Overlappable] -> ShowS

Semigroup Overlappable

Just for the Hiding instance. Should never combine different overlapping.

Methods

(<>) :: Overlappable -> Overlappable -> Overlappable

sconcat :: NonEmpty Overlappable -> Overlappable

stimes :: Integral b => b -> Overlappable -> Overlappable

Monoid Overlappable

Methods

mempty :: Overlappable

mappend :: Overlappable -> Overlappable -> Overlappable

mconcat :: [Overlappable] -> Overlappable

NFData Overlappable

Methods

rnf :: Overlappable -> ()

data Hiding

Constructors

Hidden

Instance Overlappable

NotHidden

Instances

Eq Hiding

Methods

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

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

Data Hiding

Methods

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

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

toConstr :: Hiding -> Constr

dataTypeOf :: Hiding -> DataType

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

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

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

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

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

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

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

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

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

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

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

Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b)

Methods

convert :: Arg a -> TOM (Hiding, b)

data WithHiding a

Decorating something with Hiding information.

Constructors

WithHiding

Fields

• whHiding :: !Hiding
• whThing :: 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

liftA2 :: (a -> b -> c) -> WithHiding a -> WithHiding b -> WithHiding c

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

Data a => Data (WithHiding a)

Methods

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

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

toConstr :: WithHiding a -> Constr

dataTypeOf :: WithHiding a -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (WithHiding a))

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

gmapT :: (forall b. Data b => b -> b) -> WithHiding a -> WithHiding a

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

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

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

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

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

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

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

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.

visible :: LensHiding a => a -> Bool

NotHidden arguments are visible.

notVisible :: LensHiding a => a -> Bool

Instance and Hidden arguments are notVisible.

hidden :: LensHiding a => a -> Bool

Hidden arguments are hidden.

hide :: LensHiding a => a -> a

hideOrKeepInstance :: LensHiding a => a -> a

makeInstance :: LensHiding a => a -> a

makeInstance' :: LensHiding a => Overlappable -> a -> a

isOverlappable :: LensHiding a => a -> Bool

isInstance :: LensHiding a => a -> Bool

sameHiding :: (LensHiding a, LensHiding b) => a -> b -> Bool

Ignores Overlappable.

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

Data Big

Methods

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

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

toConstr :: Big -> Constr

dataTypeOf :: Big -> DataType

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

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

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

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

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

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

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

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

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

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

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.

Instances

Eq Relevance

Methods

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

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

Data Relevance

Methods

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

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

toConstr :: Relevance -> Constr

dataTypeOf :: Relevance -> DataType

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

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

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

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

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

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

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

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

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

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

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` Forced `moreRelevant` NonStrict `moreRelevant` Irrelevant

irrelevant :: Relevance -> Bool

unusableRelevance :: LensRelevance a => a -> 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.

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

Data Origin

Methods

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

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

toConstr :: Origin -> Constr

dataTypeOf :: Origin -> DataType

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

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

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

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

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

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

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

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

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

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

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

ChooseFlex Origin

Methods

chooseFlex :: Origin -> Origin -> FlexChoice

data WithOrigin a

Decorating something with Origin information.

Constructors

WithOrigin

Fields

• woOrigin :: !Origin
• woThing :: a

Instances

Functor WithOrigin

Methods

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

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

Foldable WithOrigin

Methods

fold :: Monoid m => WithOrigin m -> m

foldMap :: Monoid m => (a -> m) -> WithOrigin a -> m

foldr :: (a -> b -> b) -> b -> WithOrigin a -> b

foldr' :: (a -> b -> b) -> b -> WithOrigin a -> b

foldl :: (b -> a -> b) -> b -> WithOrigin a -> b

foldl' :: (b -> a -> b) -> b -> WithOrigin a -> b

foldr1 :: (a -> a -> a) -> WithOrigin a -> a

foldl1 :: (a -> a -> a) -> WithOrigin a -> a

toList :: WithOrigin a -> [a]

null :: WithOrigin a -> Bool

length :: WithOrigin a -> Int

elem :: Eq a => a -> WithOrigin a -> Bool

maximum :: Ord a => WithOrigin a -> a

minimum :: Ord a => WithOrigin a -> a

sum :: Num a => WithOrigin a -> a

product :: Num a => WithOrigin a -> a

Traversable WithOrigin

Methods

traverse :: Applicative f => (a -> f b) -> WithOrigin a -> f (WithOrigin b)

sequenceA :: Applicative f => WithOrigin (f a) -> f (WithOrigin a)

mapM :: Monad m => (a -> m b) -> WithOrigin a -> m (WithOrigin b)

sequence :: Monad m => WithOrigin (m a) -> m (WithOrigin a)

Decoration WithOrigin

Methods

traverseF :: Functor m => (a -> m b) -> WithOrigin a -> m (WithOrigin b)

distributeF :: Functor m => WithOrigin (m a) -> m (WithOrigin a)

Eq a => Eq (WithOrigin a)

Methods

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

(/=) :: WithOrigin a -> WithOrigin a -> Bool

Data a => Data (WithOrigin a)

Methods

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

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

toConstr :: WithOrigin a -> Constr

dataTypeOf :: WithOrigin a -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (WithOrigin a))

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

gmapT :: (forall b. Data b => b -> b) -> WithOrigin a -> WithOrigin a

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

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

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

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

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

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

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

Ord a => Ord (WithOrigin a)

Methods

compare :: WithOrigin a -> WithOrigin a -> Ordering

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

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

(>) :: WithOrigin a -> WithOrigin a -> Bool

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

max :: WithOrigin a -> WithOrigin a -> WithOrigin a

min :: WithOrigin a -> WithOrigin a -> WithOrigin a

Show a => Show (WithOrigin a)

Methods

showsPrec :: Int -> WithOrigin a -> ShowS

show :: WithOrigin a -> String

showList :: [WithOrigin a] -> ShowS

NFData a => NFData (WithOrigin a)

Methods

rnf :: WithOrigin a -> ()

KillRange a => KillRange (WithOrigin a)

Methods

killRange :: KillRangeT (WithOrigin a)

SetRange a => SetRange (WithOrigin a)

Methods

setRange :: Range -> WithOrigin a -> WithOrigin a

HasRange a => HasRange (WithOrigin a)

Methods

getRange :: WithOrigin a -> Range

LensOrigin (WithOrigin a)

Methods

getOrigin :: WithOrigin a -> Origin

setOrigin :: Origin -> WithOrigin a -> WithOrigin a

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

class LensOrigin a where

A lens to access the Origin attribute in data structures. Minimal implementation: getOrigin and one of setOrigin or mapOrigin.

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

Methods

getOrigin :: Dom e -> Origin

setOrigin :: Origin -> Dom e -> Dom e

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

LensOrigin (Arg e)

Methods

getOrigin :: Arg e -> Origin

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

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

LensOrigin (WithOrigin a)

Methods

getOrigin :: WithOrigin a -> Origin

setOrigin :: Origin -> WithOrigin a -> WithOrigin a

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

LensOrigin (Elim' a)

This instance cheats on Proj, use with care. Projs are always assumed to be UserWritten, since they have no ArgInfo.

Methods

getOrigin :: Elim' a -> Origin

setOrigin :: Origin -> Elim' a -> Elim' a

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

LensOrigin (FlexibleVar a)

Methods

getOrigin :: FlexibleVar a -> Origin

setOrigin :: Origin -> FlexibleVar a -> FlexibleVar a

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

Argument decoration

data ArgInfo

A function argument can be hidden and/or irrelevant.

Constructors

ArgInfo

Fields

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

Instances

Eq ArgInfo

Methods

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

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

Data ArgInfo

Methods

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

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

toConstr :: ArgInfo -> Constr

dataTypeOf :: ArgInfo -> DataType

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

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

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

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

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

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

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

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

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

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

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)

MapNamedArgPattern NAP

Methods

mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP

IsPrefixOf Args

Methods

isPrefixOf :: Args -> Args -> Maybe Elims

UniverseBi Args Pattern

Methods

universeBi :: Args -> [Pattern]

UniverseBi Args Term

Methods

universeBi :: Args -> [Term]

Conversion TOM Args (MM (ArgList O) (RefInfo O))

Methods

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

PatternVars a (NamedArg (Pattern' a))

Methods

patternVars :: NamedArg (Pattern' a) -> [Arg (Either a Term)]

PatternVars a (Arg (Pattern' a))

Methods

patternVars :: Arg (Pattern' a) -> [Arg (Either a Term)]

PatternLike a b => PatternLike a (Arg b)

Methods

foldrPattern :: Monoid m => (Pattern' a -> m -> m) -> Arg b -> m

traversePatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Arg b -> m (Arg b)

APatternLike a b => APatternLike a (Arg b)

Methods

foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> Arg b -> m

traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Arg b -> m (Arg b)

Conversion TOM (Arg Pattern) (Pat O)

Methods

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

Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b)

Methods

convert :: Arg a -> TOM (Hiding, b)

Eq a => Eq (Arg a)

Methods

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

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

Data e => Data (Arg e)

Methods

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

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

toConstr :: Arg e -> Constr

dataTypeOf :: Arg e -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (Arg e))

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

gmapT :: (forall b. Data b => b -> b) -> Arg e -> Arg e

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

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

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

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

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

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

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

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

Free a => Free (Arg a)

Methods

freeVars' :: IsVarSet c => Arg a -> FreeM c

TermLike a => TermLike (Arg a)

Methods

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

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

GetDefs a => GetDefs (Arg a)

Methods

getDefs :: MonadGetDefs 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

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

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

Methods

prettyTCM :: Arg a -> TCM Doc

ExpandPatternSynonyms a => ExpandPatternSynonyms (Arg a)

Methods

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

MentionsMeta t => MentionsMeta (Arg t)

Methods

mentionsMeta :: MetaId -> Arg t -> Bool

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)

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)

SubstWithOrigin (Arg Term)

Methods

substWithOrigin :: Substitution -> [WithOrigin Term] -> Arg Term -> Arg Term

SubstWithOrigin (Arg DisplayTerm)

Methods

substWithOrigin :: Substitution -> [WithOrigin Term] -> Arg DisplayTerm -> Arg DisplayTerm

Match a => Match (Arg a)

Methods

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

NormaliseProjP a => NormaliseProjP (Arg a)

Methods

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

HasPolarity a => HasPolarity (Arg a)

Methods

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

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

NoProjectedVar a => NoProjectedVar (Arg a)

Methods

noProjectedVar :: Arg a -> Either ProjVarExc ()

Unquote a => Unquote (Arg a)

Methods

unquote :: Term -> UnquoteM (Arg a)

IsFlexiblePattern a => IsFlexiblePattern (Arg a)

Methods

maybeFlexiblePattern :: Arg a -> MaybeT TCM FlexibleVarKind

isFlexiblePattern :: Arg a -> TCM Bool

AbsTerm a => AbsTerm (Arg a)

Methods

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

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

Methods

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

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

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)

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)

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)

TelToArgs ListTel

Methods

telToArgs :: ListTel -> [Arg ArgName]

TelToArgs Telescope

Methods

telToArgs :: Telescope -> [Arg ArgName]

TeleNoAbs ListTel

Methods

teleNoAbs :: ListTel -> Term -> Term

TeleNoAbs Telescope

Methods

teleNoAbs :: Telescope -> Term -> Term

AddContext Telescope

Methods

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

contextSize :: Telescope -> Nat

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

DropArgs Telescope

NOTE: This creates telescopes with unbound de Bruijn indices.

Methods

dropArgs :: Int -> Telescope -> 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

Data e => Data (Dom e)

Methods

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

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

toConstr :: Dom e -> Constr

dataTypeOf :: Dom e -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (Dom e))

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

gmapT :: (forall b. Data b => b -> b) -> Dom e -> Dom e

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

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

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

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

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

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

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

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

prettyList :: [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

LensOrigin (Dom e)

Methods

getOrigin :: Dom e -> Origin

setOrigin :: Origin -> Dom e -> Dom e

mapOrigin :: (Origin -> Origin) -> 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

Free a => Free (Dom a)

Methods

freeVars' :: IsVarSet c => Dom a -> FreeM c

TermLike a => TermLike (Dom a)

Methods

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

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

GetDefs a => GetDefs (Dom a)

Methods

getDefs :: MonadGetDefs 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

IsSizeType a => IsSizeType (Dom a)

Methods

isSizeType :: Dom a -> TCM (Maybe BoundedSize)

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

AddContext (KeepNames Telescope)

Methods

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

contextSize :: KeepNames Telescope -> Nat

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

Methods

prettyTCM :: Dom a -> TCM Doc

MentionsMeta t => MentionsMeta (Dom t)

Methods

mentionsMeta :: MetaId -> Dom t -> Bool

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

Unquote a => Unquote (Dom a)

Methods

unquote :: Term -> UnquoteM (Dom a)

AbsTerm a => AbsTerm (Dom a)

Methods

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

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

AddContext (KeepNames String, Dom Type)

Methods

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

contextSize :: (KeepNames String, 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

MapNamedArgPattern NAP

Methods

mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP

PatternVars a (NamedArg (Pattern' a))

Methods

patternVars :: NamedArg (Pattern' a) -> [Arg (Either a Term)]

PatternLike a b => PatternLike a (Named x b)

Methods

foldrPattern :: Monoid m => (Pattern' a -> m -> m) -> Named x b -> m

traversePatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Named x b -> m (Named x b)

APatternLike a b => APatternLike a (Named n b)

Methods

foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> Named n b -> m

traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Named n b -> m (Named n b)

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

(Data a, Data name) => Data (Named name a)

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Named name a -> c (Named name a)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Named name a)

toConstr :: Named name a -> Constr

dataTypeOf :: Named name a -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (Named name a))

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Named name a))

gmapT :: (forall b. Data b => b -> b) -> Named name a -> Named name a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Named name a -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Named name a -> r

gmapQ :: (forall d. Data d => d -> u) -> Named name a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Named name a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Named name a -> m (Named name a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Named name a -> m (Named name a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Named name a -> m (Named name a)

(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

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 r a => ToAbstract (Named name r) (Named name a)

Methods

toAbstract :: Named name r -> WithNames (Named name 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.

setNamedArg :: NamedArg a -> b -> NamedArg b

setNamedArg a b = updateNamedArg (const b) a

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)

MapNamedArgPattern NAP

Methods

mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP

UniverseBi Declaration RString

Methods

universeBi :: Declaration -> [RString]

PatternVars a (NamedArg (Pattern' a))

Methods

patternVars :: NamedArg (Pattern' a) -> [Arg (Either a Term)]

Eq a => Eq (Ranged a)

Methods

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

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

Data a => Data (Ranged a)

Methods

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

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

toConstr :: Ranged a -> Constr

dataTypeOf :: Ranged a -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (Ranged a))

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

gmapT :: (forall b. Data b => b -> b) -> Ranged a -> Ranged a

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

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

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

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

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

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

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

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

Data ConOrigin

Methods

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

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

toConstr :: ConOrigin -> Constr

dataTypeOf :: ConOrigin -> DataType

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

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

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

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

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

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

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

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

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

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

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

Data ProjOrigin

Methods

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

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

toConstr :: ProjOrigin -> Constr

dataTypeOf :: ProjOrigin -> DataType

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

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

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

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

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

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

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

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

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

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

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

data DataOrRecord

Constructors

IsData

IsRecord

Instances

Eq DataOrRecord

Methods

(==) :: DataOrRecord -> DataOrRecord -> Bool

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

Data DataOrRecord

Methods

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

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

toConstr :: DataOrRecord -> Constr

dataTypeOf :: DataOrRecord -> DataType

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

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

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

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

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

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

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

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

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

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

Ord DataOrRecord

Methods

compare :: DataOrRecord -> DataOrRecord -> Ordering

(<) :: DataOrRecord -> DataOrRecord -> Bool

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

(>) :: DataOrRecord -> DataOrRecord -> Bool

(>=) :: DataOrRecord -> DataOrRecord -> Bool

max :: DataOrRecord -> DataOrRecord -> DataOrRecord

min :: DataOrRecord -> DataOrRecord -> DataOrRecord

Show DataOrRecord

Methods

showsPrec :: Int -> DataOrRecord -> ShowS

show :: DataOrRecord -> String

showList :: [DataOrRecord] -> ShowS

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

Data IsInfix

Methods

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

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

toConstr :: IsInfix -> Constr

dataTypeOf :: IsInfix -> DataType

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

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

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

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

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

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

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

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

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

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

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

Data Access

Methods

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

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

toConstr :: Access -> Constr

dataTypeOf :: Access -> DataType

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

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

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

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

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

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

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

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

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

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

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

Pretty Access

Methods

pretty :: Access -> Doc

prettyPrec :: Int -> Access -> Doc

prettyList :: [Access] -> Doc

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

Data IsAbstract

Methods

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

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

toConstr :: IsAbstract -> Constr

dataTypeOf :: IsAbstract -> DataType

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

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

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

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

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

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

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

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

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

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

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

Data IsInstance

Methods

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

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

toConstr :: IsInstance -> Constr

dataTypeOf :: IsInstance -> DataType

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

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

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

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

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

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

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

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

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

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

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

Data IsMacro

Methods

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

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

toConstr :: IsMacro -> Constr

dataTypeOf :: IsMacro -> DataType

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

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

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

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

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

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

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

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

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

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

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

Data NameId

Methods

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

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

toConstr :: NameId -> Constr

dataTypeOf :: NameId -> DataType

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

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

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

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

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

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

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

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

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

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

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.20170816-GHenzADqKzt4ualJbaFRMq" 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

Data MetaId

Methods

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

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

toConstr :: MetaId -> Constr

dataTypeOf :: MetaId -> DataType

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

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

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

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

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

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

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

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

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

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

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

prettyList :: [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

Data PositionInName

Methods

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

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

toConstr :: PositionInName -> Constr

dataTypeOf :: PositionInName -> DataType

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

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

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

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

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

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

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

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

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

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

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

Data e => Data (MaybePlaceholder e)

Methods

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

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

toConstr :: MaybePlaceholder e -> Constr

dataTypeOf :: MaybePlaceholder e -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (MaybePlaceholder e))

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

gmapT :: (forall b. Data b => b -> b) -> MaybePlaceholder e -> MaybePlaceholder e

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

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

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

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

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

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

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

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

Data InteractionId

Methods

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

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

toConstr :: InteractionId -> Constr

dataTypeOf :: InteractionId -> DataType

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

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

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

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

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

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

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

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

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

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

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

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

Methods

gfoldl :: (forall d c. Data d => c (d -> c) -> d -> c c) -> (forall g. g -> c g) -> ImportDirective' a b -> c (ImportDirective' a b)

gunfold :: (forall c r. Data c => c (c -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ImportDirective' a b)

toConstr :: ImportDirective' a b -> Constr

dataTypeOf :: ImportDirective' a b -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (ImportDirective' a b))

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ImportDirective' a b))

gmapT :: (forall c. Data c => c -> c) -> ImportDirective' a b -> ImportDirective' a b

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ImportDirective' a b -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ImportDirective' a b -> r

gmapQ :: (forall d. Data d => d -> u) -> ImportDirective' a b -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ImportDirective' a b -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ImportDirective' a b -> m (ImportDirective' a b)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ImportDirective' a b -> m (ImportDirective' a b)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ImportDirective' a b -> m (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)

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

(Data b, Data a) => Data (Using' a b)

Methods

gfoldl :: (forall d c. Data d => c (d -> c) -> d -> c c) -> (forall g. g -> c g) -> Using' a b -> c (Using' a b)

gunfold :: (forall c r. Data c => c (c -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Using' a b)

toConstr :: Using' a b -> Constr

dataTypeOf :: Using' a b -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (Using' a b))

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Using' a b))

gmapT :: (forall c. Data c => c -> c) -> Using' a b -> Using' a b

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Using' a b -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Using' a b -> r

gmapQ :: (forall d. Data d => d -> u) -> Using' a b -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Using' a b -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Using' a b -> m (Using' a b)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Using' a b -> m (Using' a b)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Using' a b -> m (Using' a b)

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

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

Methods

gfoldl :: (forall d c. Data d => c (d -> c) -> d -> c c) -> (forall g. g -> c g) -> ImportedName' a b -> c (ImportedName' a b)

gunfold :: (forall c r. Data c => c (c -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ImportedName' a b)

toConstr :: ImportedName' a b -> Constr

dataTypeOf :: ImportedName' a b -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (ImportedName' a b))

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ImportedName' a b))

gmapT :: (forall c. Data c => c -> c) -> ImportedName' a b -> ImportedName' a b

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ImportedName' a b -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ImportedName' a b -> r

gmapQ :: (forall d. Data d => d -> u) -> ImportedName' a b -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ImportedName' a b -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ImportedName' a b -> m (ImportedName' a b)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ImportedName' a b -> m (ImportedName' a b)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ImportedName' a b -> m (ImportedName' a b)

(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

(Data b, Data a) => Data (Renaming' a b)

Methods

gfoldl :: (forall d c. Data d => c (d -> c) -> d -> c c) -> (forall g. g -> c g) -> Renaming' a b -> c (Renaming' a b)

gunfold :: (forall c r. Data c => c (c -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Renaming' a b)

toConstr :: Renaming' a b -> Constr

dataTypeOf :: Renaming' a b -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (Renaming' a b))

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Renaming' a b))

gmapT :: (forall c. Data c => c -> c) -> Renaming' a b -> Renaming' a b

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Renaming' a b -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Renaming' a b -> r

gmapQ :: (forall d. Data d => d -> u) -> Renaming' a b -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Renaming' a b -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Renaming' a b -> m (Renaming' a b)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Renaming' a b -> m (Renaming' a b)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Renaming' a b -> m (Renaming' a b)

(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

Data m => Data (TerminationCheck m)

Methods

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

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

toConstr :: TerminationCheck m -> Constr

dataTypeOf :: TerminationCheck m -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (TerminationCheck m))

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

gmapT :: (forall b. Data b => b -> b) -> TerminationCheck m -> TerminationCheck m

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

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

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

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

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

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

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

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