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

Eta-equality

data HasEta

Constructors

NoEta

YesEta

Instances

Eq HasEta

Methods

(==) :: HasEta -> HasEta -> Bool

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

Data HasEta

Methods

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

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

toConstr :: HasEta -> Constr

dataTypeOf :: HasEta -> DataType

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

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

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

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

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

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

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

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

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

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

Ord HasEta

Methods

compare :: HasEta -> HasEta -> Ordering

(<) :: HasEta -> HasEta -> Bool

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

(>) :: HasEta -> HasEta -> Bool

(>=) :: HasEta -> HasEta -> Bool

max :: HasEta -> HasEta -> HasEta

min :: HasEta -> HasEta -> HasEta

Show HasEta

Methods

showsPrec :: Int -> HasEta -> ShowS

show :: HasEta -> String

showList :: [HasEta] -> ShowS

NFData HasEta

Methods

rnf :: HasEta -> ()

KillRange HasEta

Methods

killRange :: KillRangeT HasEta

HasRange HasEta

Methods

getRange :: HasEta -> Range

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, MonadDebug 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.

Modalities

data Modality

We have a tuple of modalities, which might not be fully orthogonal. For instance, irrelevant stuff is also run-time irrelevant.

Constructors

Modality

Fields

• modRelevance :: Relevance

  Legacy irrelevance. See Pfenning, LiCS 2001; AbelVezzosiWinterhalter, ICFP 2017.

• modQuantity :: Quantity

  Cardinality / runtime erasure. See Conor McBride, I got plenty o' nutting, Wadlerfest 2016.

Instances

Eq Modality

Methods

(==) :: Modality -> Modality -> Bool

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

Data Modality

Methods

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

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

toConstr :: Modality -> Constr

dataTypeOf :: Modality -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Modality

Methods

compare :: Modality -> Modality -> Ordering

(<) :: Modality -> Modality -> Bool

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

(>) :: Modality -> Modality -> Bool

(>=) :: Modality -> Modality -> Bool

max :: Modality -> Modality -> Modality

min :: Modality -> Modality -> Modality

Show Modality

Methods

showsPrec :: Int -> Modality -> ShowS

show :: Modality -> String

showList :: [Modality] -> ShowS

Generic Modality

Associated Types

type Rep Modality :: * -> *

Methods

from :: Modality -> Rep Modality x

to :: Rep Modality x -> Modality

Semigroup Modality

Pointwise composition.

Methods

(<>) :: Modality -> Modality -> Modality

sconcat :: NonEmpty Modality -> Modality

stimes :: Integral b => b -> Modality -> Modality

Monoid Modality

Pointwise unit.

Methods

mempty :: Modality

mappend :: Modality -> Modality -> Modality

mconcat :: [Modality] -> Modality

NFData Modality

Methods

rnf :: Modality -> ()

PartialOrd Modality

Dominance ordering.

Methods

comparable :: Comparable Modality

POMonoid Modality

POSemigroup Modality

KillRange Modality

Methods

killRange :: KillRangeT Modality

LensRelevance Modality

Methods

getRelevance :: Modality -> Relevance

setRelevance :: Relevance -> Modality -> Modality

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

LensQuantity Modality

Methods

getQuantity :: Modality -> Quantity

setQuantity :: Quantity -> Modality -> Modality

mapQuantity :: (Quantity -> Quantity) -> Modality -> Modality

LensModality Modality

Methods

getModality :: Modality -> Modality

setModality :: Modality -> Modality -> Modality

mapModality :: (Modality -> Modality) -> Modality -> Modality

Unquote Modality

Methods

unquote :: Term -> UnquoteM Modality

type Rep Modality

type Rep Modality = D1 * (MetaData "Modality" "Agda.Syntax.Common" "Agda-2.5.3.20180519-9fcgArwWAGgCm0ECOSwfBe" False) (C1 * (MetaCons "Modality" PrefixI True) ((:*:) * (S1 * (MetaSel (Just Symbol "modRelevance") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Relevance)) (S1 * (MetaSel (Just Symbol "modQuantity") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Quantity))))

defaultModality :: Modality

class LensModality a where

Minimal complete definition

getModality

Methods

getModality :: a -> Modality

setModality :: Modality -> a -> a

mapModality :: (Modality -> Modality) -> a -> a

Instances

LensModality ArgInfo

Methods

getModality :: ArgInfo -> Modality

setModality :: Modality -> ArgInfo -> ArgInfo

mapModality :: (Modality -> Modality) -> ArgInfo -> ArgInfo

LensModality Modality

Methods

getModality :: Modality -> Modality

setModality :: Modality -> Modality -> Modality

mapModality :: (Modality -> Modality) -> Modality -> Modality

LensModality (Dom e)

Methods

getModality :: Dom e -> Modality

setModality :: Modality -> Dom e -> Dom e

mapModality :: (Modality -> Modality) -> Dom e -> Dom e

LensModality (Arg e)

Methods

getModality :: Arg e -> Modality

setModality :: Modality -> Arg e -> Arg e

mapModality :: (Modality -> Modality) -> Arg e -> Arg e

getRelevanceMod :: LensModality a => LensGet Relevance a

setRelevanceMod :: LensModality a => LensSet Relevance a

mapRelevanceMod :: LensModality a => LensMap Relevance a

getQuantityMod :: LensModality a => LensGet Quantity a

setQuantityMod :: LensModality a => LensSet Quantity a

mapQuantityMod :: LensModality a => LensMap Quantity a

Quantities

data Quantity

Quantity for linearity.

Constructors

Quantity0

Zero uses, erased at runtime. TODO: | Quantity1 -- ^ Linear use (could be updated destructively). (needs postponable constraints between quantities to compute uses).

Quantityω

Unrestricted use.

Instances

Bounded Quantity

Methods

minBound :: Quantity

maxBound :: Quantity

Enum Quantity

Methods

succ :: Quantity -> Quantity

pred :: Quantity -> Quantity

toEnum :: Int -> Quantity

fromEnum :: Quantity -> Int

enumFrom :: Quantity -> [Quantity]

enumFromThen :: Quantity -> Quantity -> [Quantity]

enumFromTo :: Quantity -> Quantity -> [Quantity]

enumFromThenTo :: Quantity -> Quantity -> Quantity -> [Quantity]

Eq Quantity

Methods

(==) :: Quantity -> Quantity -> Bool

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

Data Quantity

Methods

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

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

toConstr :: Quantity -> Constr

dataTypeOf :: Quantity -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Quantity

Note that the order is ω ≤ 0, more relevant is smaller.

Methods

compare :: Quantity -> Quantity -> Ordering

(<) :: Quantity -> Quantity -> Bool

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

(>) :: Quantity -> Quantity -> Bool

(>=) :: Quantity -> Quantity -> Bool

max :: Quantity -> Quantity -> Quantity

min :: Quantity -> Quantity -> Quantity

Show Quantity

Methods

showsPrec :: Int -> Quantity -> ShowS

show :: Quantity -> String

showList :: [Quantity] -> ShowS

Generic Quantity

Associated Types

type Rep Quantity :: * -> *

Methods

from :: Quantity -> Rep Quantity x

to :: Rep Quantity x -> Quantity

Semigroup Quantity

Composition of quantities (multiplication).

Quantity0 is dominant.

Methods

(<>) :: Quantity -> Quantity -> Quantity

sconcat :: NonEmpty Quantity -> Quantity

stimes :: Integral b => b -> Quantity -> Quantity

Monoid Quantity

In the absense of finite quantities besides 0, ω is the unit.

Methods

mempty :: Quantity

mappend :: Quantity -> Quantity -> Quantity

mconcat :: [Quantity] -> Quantity

NFData Quantity

Methods

rnf :: Quantity -> ()

PartialOrd Quantity

Methods

comparable :: Comparable Quantity

POMonoid Quantity

POSemigroup Quantity

KillRange Quantity

Methods

killRange :: KillRangeT Quantity

LensQuantity Quantity

Methods

getQuantity :: Quantity -> Quantity

setQuantity :: Quantity -> Quantity -> Quantity

mapQuantity :: (Quantity -> Quantity) -> Quantity -> Quantity

type Rep Quantity

type Rep Quantity = D1 * (MetaData "Quantity" "Agda.Syntax.Common" "Agda-2.5.3.20180519-9fcgArwWAGgCm0ECOSwfBe" False) ((:+:) * (C1 * (MetaCons "Quantity0" PrefixI False) (U1 *)) (C1 * (MetaCons "Quantity\969" PrefixI False) (U1 *)))

defaultQuantity :: Quantity

class LensQuantity a where

Minimal complete definition

getQuantity

Methods

getQuantity :: a -> Quantity

setQuantity :: Quantity -> a -> a

mapQuantity :: (Quantity -> Quantity) -> a -> a

Instances

LensQuantity ArgInfo

Methods

getQuantity :: ArgInfo -> Quantity

setQuantity :: Quantity -> ArgInfo -> ArgInfo

mapQuantity :: (Quantity -> Quantity) -> ArgInfo -> ArgInfo

LensQuantity Quantity

Methods

getQuantity :: Quantity -> Quantity

setQuantity :: Quantity -> Quantity -> Quantity

mapQuantity :: (Quantity -> Quantity) -> Quantity -> Quantity

LensQuantity Modality

Methods

getQuantity :: Modality -> Quantity

setQuantity :: Quantity -> Modality -> Modality

mapQuantity :: (Quantity -> Quantity) -> Modality -> Modality

LensQuantity (Dom e)

Methods

getQuantity :: Dom e -> Quantity

setQuantity :: Quantity -> Dom e -> Dom e

mapQuantity :: (Quantity -> Quantity) -> Dom e -> Dom e

LensQuantity (Arg e)

Methods

getQuantity :: Arg e -> Quantity

setQuantity :: Quantity -> Arg e -> Arg e

mapQuantity :: (Quantity -> Quantity) -> Arg e -> Arg e

Relevance

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.

Instances

Bounded Relevance

Methods

minBound :: Relevance

maxBound :: Relevance

Enum Relevance

Methods

succ :: Relevance -> Relevance

pred :: Relevance -> Relevance

toEnum :: Int -> Relevance

fromEnum :: Relevance -> Int

enumFrom :: Relevance -> [Relevance]

enumFromThen :: Relevance -> Relevance -> [Relevance]

enumFromTo :: Relevance -> Relevance -> [Relevance]

enumFromThenTo :: Relevance -> Relevance -> Relevance -> [Relevance]

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

More relevant is smaller.

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

Generic Relevance

Associated Types

type Rep Relevance :: * -> *

Methods

from :: Relevance -> Rep Relevance x

to :: Rep Relevance x -> Relevance

Semigroup Relevance

Relevance forms a semigroup under composition.

Methods

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

sconcat :: NonEmpty Relevance -> Relevance

stimes :: Integral b => b -> Relevance -> Relevance

Monoid Relevance

Relevant is the unit.

Methods

mempty :: Relevance

mappend :: Relevance -> Relevance -> Relevance

mconcat :: [Relevance] -> Relevance

NFData Relevance

Methods

rnf :: Relevance -> ()

PartialOrd Relevance

More relevant is smaller.

Methods

comparable :: Comparable Relevance

LeftClosedPOMonoid Relevance

Methods

inverseCompose :: Relevance -> Relevance -> Relevance

POMonoid Relevance

POSemigroup 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

type Rep Relevance

type Rep Relevance = D1 * (MetaData "Relevance" "Agda.Syntax.Common" "Agda-2.5.3.20180519-9fcgArwWAGgCm0ECOSwfBe" False) ((:+:) * (C1 * (MetaCons "Relevant" PrefixI False) (U1 *)) ((:+:) * (C1 * (MetaCons "NonStrict" PrefixI False) (U1 *)) (C1 * (MetaCons "Irrelevant" PrefixI False) (U1 *))))

allRelevances :: [Relevance]

defaultRelevance :: 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 Modality

Methods

getRelevance :: Modality -> Relevance

setRelevance :: Relevance -> Modality -> Modality

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

LensRelevance TypedBindings

Methods

getRelevance :: TypedBindings -> Relevance

setRelevance :: Relevance -> TypedBindings -> TypedBindings

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

LensRelevance VarOcc

Methods

getRelevance :: VarOcc -> Relevance

setRelevance :: Relevance -> VarOcc -> VarOcc

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

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

isNonStrict :: LensRelevance a => a -> Bool

moreRelevant :: Relevance -> Relevance -> Bool

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

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

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

Origin of arguments.

Constructors

UserWritten

From the source file / user input. (Preserve!)

Inserted

E.g. inserted hidden arguments.

Reflected

Produced by the reflection machinery.

CaseSplit

Produced by an interactive case split.

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 AppInfo

Methods

getOrigin :: AppInfo -> Origin

setOrigin :: Origin -> AppInfo -> AppInfo

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

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

Free variable annotations

data FreeVariables

Constructors

UnknownFVs

KnownFVs IntSet

Instances

Eq FreeVariables

Methods

(==) :: FreeVariables -> FreeVariables -> Bool

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

Data FreeVariables

Methods

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

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

toConstr :: FreeVariables -> Constr

dataTypeOf :: FreeVariables -> DataType

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

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

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

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

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

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

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

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

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

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

Ord FreeVariables

Methods

compare :: FreeVariables -> FreeVariables -> Ordering

(<) :: FreeVariables -> FreeVariables -> Bool

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

(>) :: FreeVariables -> FreeVariables -> Bool

(>=) :: FreeVariables -> FreeVariables -> Bool

max :: FreeVariables -> FreeVariables -> FreeVariables

min :: FreeVariables -> FreeVariables -> FreeVariables

Show FreeVariables

Methods

showsPrec :: Int -> FreeVariables -> ShowS

show :: FreeVariables -> String

showList :: [FreeVariables] -> ShowS

Semigroup FreeVariables

Methods

(<>) :: FreeVariables -> FreeVariables -> FreeVariables

sconcat :: NonEmpty FreeVariables -> FreeVariables

stimes :: Integral b => b -> FreeVariables -> FreeVariables

Monoid FreeVariables

Methods

mempty :: FreeVariables

mappend :: FreeVariables -> FreeVariables -> FreeVariables

mconcat :: [FreeVariables] -> FreeVariables

NFData FreeVariables

Methods

rnf :: FreeVariables -> ()

LensFreeVariables FreeVariables

Methods

getFreeVariables :: FreeVariables -> FreeVariables

setFreeVariables :: FreeVariables -> FreeVariables -> FreeVariables

mapFreeVariables :: (FreeVariables -> FreeVariables) -> FreeVariables -> FreeVariables

unknownFreeVariables :: FreeVariables

noFreeVariables :: FreeVariables

oneFreeVariable :: Int -> FreeVariables

freeVariablesFromList :: [Int] -> FreeVariables

class LensFreeVariables a where

A lens to access the FreeVariables attribute in data structures. Minimal implementation: getFreeVariables and one of setFreeVariables or mapFreeVariables.

Minimal complete definition

getFreeVariables

Methods

getFreeVariables :: a -> FreeVariables

setFreeVariables :: FreeVariables -> a -> a

mapFreeVariables :: (FreeVariables -> FreeVariables) -> a -> a

Instances

LensFreeVariables ArgInfo

Methods

getFreeVariables :: ArgInfo -> FreeVariables

setFreeVariables :: FreeVariables -> ArgInfo -> ArgInfo

mapFreeVariables :: (FreeVariables -> FreeVariables) -> ArgInfo -> ArgInfo

LensFreeVariables FreeVariables

Methods

getFreeVariables :: FreeVariables -> FreeVariables

setFreeVariables :: FreeVariables -> FreeVariables -> FreeVariables

mapFreeVariables :: (FreeVariables -> FreeVariables) -> FreeVariables -> FreeVariables

LensFreeVariables (Dom e)

Methods

getFreeVariables :: Dom e -> FreeVariables

setFreeVariables :: FreeVariables -> Dom e -> Dom e

mapFreeVariables :: (FreeVariables -> FreeVariables) -> Dom e -> Dom e

LensFreeVariables (Arg e)

Methods

getFreeVariables :: Arg e -> FreeVariables

setFreeVariables :: FreeVariables -> Arg e -> Arg e

mapFreeVariables :: (FreeVariables -> FreeVariables) -> Arg e -> Arg e

hasNoFreeVariables :: LensFreeVariables a => a -> Bool

Argument decoration

data ArgInfo

A function argument can be hidden and/or irrelevant.

Constructors

ArgInfo

Fields

• argInfoHiding :: Hiding
• argInfoModality :: Modality
• argInfoOrigin :: Origin
• argInfoFreeVariables :: FreeVariables

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

LensFreeVariables ArgInfo

Methods

getFreeVariables :: ArgInfo -> FreeVariables

setFreeVariables :: FreeVariables -> ArgInfo -> ArgInfo

mapFreeVariables :: (FreeVariables -> FreeVariables) -> 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

LensQuantity ArgInfo

Methods

getQuantity :: ArgInfo -> Quantity

setQuantity :: Quantity -> ArgInfo -> ArgInfo

mapQuantity :: (Quantity -> Quantity) -> ArgInfo -> ArgInfo

LensModality ArgInfo

Methods

getModality :: ArgInfo -> Modality

setModality :: Modality -> ArgInfo -> ArgInfo

mapModality :: (Modality -> Modality) -> 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

getHidingArgInfo :: LensArgInfo a => LensGet Hiding a

setHidingArgInfo :: LensArgInfo a => LensSet Hiding a

mapHidingArgInfo :: LensArgInfo a => LensMap Hiding a

getModalityArgInfo :: LensArgInfo a => LensGet Modality a

setModalityArgInfo :: LensArgInfo a => LensSet Modality a

mapModalityArgInfo :: LensArgInfo a => LensMap Modality a

getOriginArgInfo :: LensArgInfo a => LensGet Origin a

setOriginArgInfo :: LensArgInfo a => LensSet Origin a

mapOriginArgInfo :: LensArgInfo a => LensMap Origin a

getFreeVariablesArgInfo :: LensArgInfo a => LensGet FreeVariables a

setFreeVariablesArgInfo :: LensArgInfo a => LensSet FreeVariables a

mapFreeVariablesArgInfo :: LensArgInfo a => LensMap FreeVariables a

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)

MapNamedArgPattern a (NamedArg (Pattern' a))

Modify the content of VarP, and the closest surrounding NamedArg.

Note: the mapNamedArg for Pattern' is not expressible simply by fmap or traverse etc., since ConP has NamedArg subpatterns, which are taken into account by mapNamedArg.

Methods

mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)

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)

Ignores Quantity, Relevance, Origin, and FreeVariables. Ignores content of argument if Irrelevant.

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

LensFreeVariables (Arg e)

Methods

getFreeVariables :: Arg e -> FreeVariables

setFreeVariables :: FreeVariables -> Arg e -> Arg e

mapFreeVariables :: (FreeVariables -> FreeVariables) -> Arg e -> Arg e

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

LensQuantity (Arg e)

Methods

getQuantity :: Arg e -> Quantity

setQuantity :: Quantity -> Arg e -> Arg e

mapQuantity :: (Quantity -> Quantity) -> Arg e -> Arg e

LensModality (Arg e)

Methods

getModality :: Arg e -> Modality

setModality :: Modality -> Arg e -> Arg e

mapModality :: (Modality -> Modality) -> 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)

CPatternLike p => CPatternLike (Arg p)

Methods

foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Arg p -> m

traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Arg p -> m (Arg p)

traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Arg p -> m (Arg p)

IsWithP p => IsWithP (Arg p)

Methods

isWithP :: Arg p -> Maybe (Arg p)

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

PrecomputeFreeVars a => PrecomputeFreeVars (Arg a)

Methods

precomputeFreeVars :: Arg a -> FV (Arg a)

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

CountPatternVars a => CountPatternVars (Arg a)

Methods

countPatternVars :: Arg a -> Int

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 :: (Applicative m, 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

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

Methods

prettyTCM :: Arg a -> TCM Doc

NamesIn a => NamesIn (Arg a)

Methods

namesIn :: Arg a -> Set QName

IsInstantiatedMeta a => IsInstantiatedMeta (Arg a)

Methods

isInstantiatedMeta :: Arg a -> TCM Bool

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]

UsableRelevance a => UsableRelevance (Arg a)

Methods

usableRel :: Relevance -> Arg a -> TCM Bool

ForcedVariables a => ForcedVariables (Arg a)

Methods

forcedVariables :: Arg a -> [(Modality, Nat)]

ComputeOccurrences a => ComputeOccurrences (Arg a)

Methods

occurrences :: Arg a -> OccM OccurrencesBuilder

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

ReduceAndEtaContract a => ReduceAndEtaContract (Arg a)

Methods

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

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

PatternVarModalities a x => PatternVarModalities (Arg a) x

Methods

patternVarModalities :: Arg a -> [(x, Modality)]

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

Methods

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

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

TermToPattern a b => TermToPattern (Arg a) (Arg b)

Methods

termToPattern :: Arg a -> TCM (Arg 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

PrettyTCM Telescope

Methods

prettyTCM :: Telescope -> TCM Doc

DropArgs Telescope

NOTE: This creates telescopes with unbound de Bruijn indices.

Methods

dropArgs :: Int -> Telescope -> Telescope

AddContext Telescope

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => Telescope -> tcm a -> tcm a

contextSize :: Telescope -> Nat

Reduce Telescope

Methods

reduce' :: Telescope -> ReduceM Telescope

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

Instantiate Telescope

Methods

instantiate' :: Telescope -> ReduceM Telescope

Reify Telescope Telescope

Methods

reify :: Telescope -> TCM Telescope

reifyWhen :: Bool -> Telescope -> TCM Telescope

Eq a => Eq (Dom a)

Ignores Origin and FreeVariables.

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

LensFreeVariables (Dom e)

Methods

getFreeVariables :: Dom e -> FreeVariables

setFreeVariables :: FreeVariables -> Dom e -> Dom e

mapFreeVariables :: (FreeVariables -> FreeVariables) -> 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

LensQuantity (Dom e)

Methods

getQuantity :: Dom e -> Quantity

setQuantity :: Quantity -> Dom e -> Dom e

mapQuantity :: (Quantity -> Quantity) -> Dom e -> Dom e

LensModality (Dom e)

Methods

getModality :: Dom e -> Modality

setModality :: Modality -> Dom e -> Dom e

mapModality :: (Modality -> Modality) -> 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

PrecomputeFreeVars a => PrecomputeFreeVars (Dom a)

Methods

precomputeFreeVars :: Dom a -> FV (Dom a)

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

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

Methods

prettyTCM :: Dom a -> TCM Doc

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, MonadDebug tcm) => Dom (String, Type) -> tcm a -> tcm a

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

AddContext (Dom (Name, Type))

Methods

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

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

AddContext (Dom Type)

Methods

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

contextSize :: Dom Type -> Nat

AddContext (KeepNames Telescope)

Methods

addContext :: (MonadTCM tcm, MonadDebug tcm) => KeepNames Telescope -> tcm a -> tcm a

contextSize :: KeepNames Telescope -> Nat

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]

UsableRelevance a => UsableRelevance (Dom a)

Methods

usableRel :: Relevance -> Dom a -> TCM Bool

ComputeOccurrences a => ComputeOccurrences (Dom a)

Methods

occurrences :: Dom a -> OccM OccurrencesBuilder

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

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, MonadDebug tcm) => ([WithHiding Name], Dom Type) -> tcm a -> tcm a

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

AddContext ([Name], Dom Type)

Methods

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

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

AddContext (String, Dom Type)

Methods

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

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

AddContext (Name, Dom Type)

Methods

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

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

AddContext (KeepNames String, Dom Type)

Methods

addContext :: (MonadTCM tcm, MonadDebug 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)]

MapNamedArgPattern a (NamedArg (Pattern' a))

Modify the content of VarP, and the closest surrounding NamedArg.

Note: the mapNamedArg for Pattern' is not expressible simply by fmap or traverse etc., since ConP has NamedArg subpatterns, which are taken into account by mapNamedArg.

Methods

mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)

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)

CPatternLike p => CPatternLike (Named n p)

Methods

foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Named n p -> m

traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Named n p -> m (Named n p)

traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Named n p -> m (Named n p)

IsWithP p => IsWithP (Named n p)

Methods

isWithP :: Named n p -> Maybe (Named n p)

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

CountPatternVars a => CountPatternVars (Named x a)

Methods

countPatternVars :: Named x a -> Int

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 :: (Applicative m, 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

PatternVarModalities a x => PatternVarModalities (Named s a) x

Methods

patternVarModalities :: Named s a -> [(x, Modality)]

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

TermToPattern a b => TermToPattern (Named c a) (Named c b)

Methods

termToPattern :: Named c a -> TCM (Named c 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)]

MapNamedArgPattern a (NamedArg (Pattern' a))

Modify the content of VarP, and the closest surrounding NamedArg.

Note: the mapNamedArg for Pattern' is not expressible simply by fmap or traverse etc., since ConP has NamedArg subpatterns, which are taken into account by mapNamedArg.

Methods

mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)

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

ConOSplit

Generated by interactive case splitting.

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.3.20180519-9fcgArwWAGgCm0ECOSwfBe" 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

PrettyTCM MetaId

Methods

prettyTCM :: MetaId -> TCM Doc

UnFreezeMeta MetaId

Methods

unfreezeMeta :: MetaId -> TCM ()

IsInstantiatedMeta MetaId

Methods

isInstantiatedMeta :: MetaId -> TCM Bool

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