Agda.Syntax.Position

Position information for syntax. Crucial for giving good error messages.

Positions

type Position = Position' SrcFile

type PositionWithoutFile = Position' ()

data Position' a

Represents a point in the input.

If two positions have the same srcFile and posPos components, then the final two components should be the same as well, but since this can be hard to enforce the program should not rely too much on the last two components; they are mainly there to improve error messages for the user.

Note the invariant which positions have to satisfy: positionInvariant.

Constructors

Pn

Fields

• srcFile :: !a

  File.

• posPos :: !Int32

  Position, counting from 1.

• posLine :: !Int32

  Line number, counting from 1.

• posCol :: !Int32

  Column number, counting from 1.

Instances

Functor Position'

Defined in Agda.Syntax.Position

Methods

fmap :: (a -> b) -> Position' a -> Position' b

(<$) :: a -> Position' b -> Position' a

Show PositionWithoutFile

Defined in Agda.Syntax.Position

Methods

showsPrec :: Int -> PositionWithoutFile -> ShowS

show :: PositionWithoutFile -> String

showList :: [PositionWithoutFile] -> ShowS

Foldable Position'

Defined in Agda.Syntax.Position

Methods

fold :: Monoid m => Position' m -> m

foldMap :: Monoid m => (a -> m) -> Position' a -> m

foldMap' :: Monoid m => (a -> m) -> Position' a -> m

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

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

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

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

foldr1 :: (a -> a -> a) -> Position' a -> a

foldl1 :: (a -> a -> a) -> Position' a -> a

toList :: Position' a -> [a]

null :: Position' a -> Bool

length :: Position' a -> Int

elem :: Eq a => a -> Position' a -> Bool

maximum :: Ord a => Position' a -> a

minimum :: Ord a => Position' a -> a

sum :: Num a => Position' a -> a

product :: Num a => Position' a -> a

Traversable Position'

Defined in Agda.Syntax.Position

Methods

traverse :: Applicative f => (a -> f b) -> Position' a -> f (Position' b)

sequenceA :: Applicative f => Position' (f a) -> f (Position' a)

mapM :: Monad m => (a -> m b) -> Position' a -> m (Position' b)

sequence :: Monad m => Position' (m a) -> m (Position' a)

Pretty PositionWithoutFile

Defined in Agda.Syntax.Position

Methods

pretty :: PositionWithoutFile -> Doc

prettyPrec :: Int -> PositionWithoutFile -> Doc

prettyList :: [PositionWithoutFile] -> Doc

Eq a => Eq (Position' a)

Defined in Agda.Syntax.Position

Methods

(==) :: Position' a -> Position' a -> Bool

(/=) :: Position' a -> Position' a -> Bool

Data a => Data (Position' a)

Defined in Agda.Syntax.Position

Methods

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

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

toConstr :: Position' a -> Constr

dataTypeOf :: Position' a -> DataType

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

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

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

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

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

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

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

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

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

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

Ord a => Ord (Position' a)

Defined in Agda.Syntax.Position

Methods

compare :: Position' a -> Position' a -> Ordering

(<) :: Position' a -> Position' a -> Bool

(<=) :: Position' a -> Position' a -> Bool

(>) :: Position' a -> Position' a -> Bool

(>=) :: Position' a -> Position' a -> Bool

max :: Position' a -> Position' a -> Position' a

min :: Position' a -> Position' a -> Position' a

Read a => Read (Position' a)

Defined in Agda.Interaction.Base

Methods

readsPrec :: Int -> ReadS (Position' a)

readList :: ReadS [Position' a]

readPrec :: ReadPrec (Position' a)

readListPrec :: ReadPrec [Position' a]

Show a => Show (Position' (Maybe a))

Defined in Agda.Syntax.Position

Methods

showsPrec :: Int -> Position' (Maybe a) -> ShowS

show :: Position' (Maybe a) -> String

showList :: [Position' (Maybe a)] -> ShowS

Generic (Position' a)

Defined in Agda.Syntax.Position

Associated Types

type Rep (Position' a) :: Type -> Type

Methods

from :: Position' a -> Rep (Position' a) x

to :: Rep (Position' a) x -> Position' a

ToJSON (Position' ())

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: Position' () -> Value

toEncoding :: Position' () -> Encoding

toJSONList :: [Position' ()] -> Value

toEncodingList :: [Position' ()] -> Encoding

Pretty a => Pretty (Position' (Maybe a))

Defined in Agda.Syntax.Position

Methods

pretty :: Position' (Maybe a) -> Doc

prettyPrec :: Int -> Position' (Maybe a) -> Doc

prettyList :: [Position' (Maybe a)] -> Doc

EmbPrj a => EmbPrj (Position' a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Position' a -> S Int32

icod_ :: Position' a -> S Int32

value :: Int32 -> R (Position' a)

EncodeTCM (Position' ())

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: Position' () -> TCM Value

type Rep (Position' a)

Defined in Agda.Syntax.Position

type Rep (Position' a) = D1 ('MetaData "Position'" "Agda.Syntax.Position" "Agda-2.6.1.2-5kYg11u3V8c52jrcc71Agq" 'False) (C1 ('MetaCons "Pn" 'PrefixI 'True) ((S1 ('MetaSel ('Just "srcFile") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a) :*: S1 ('MetaSel ('Just "posPos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int32)) :*: (S1 ('MetaSel ('Just "posLine") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int32) :*: S1 ('MetaSel ('Just "posCol") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int32))))

type SrcFile = Maybe AbsolutePath

positionInvariant :: Position' a -> Bool

startPos :: Maybe AbsolutePath -> Position

The first position in a file: position 1, line 1, column 1.

movePos :: Position' a -> Char -> Position' a

Advance the position by one character. A newline character ('n') moves the position to the first character in the next line. Any other character moves the position to the next column.

movePosByString :: Position' a -> String -> Position' a

Advance the position by a string.

movePosByString = foldl' movePos

backupPos :: Position' a -> Position' a

Backup the position by one character.

Precondition: The character must not be 'n'.

startPos' :: a -> Position' a

The first position in a file: position 1, line 1, column 1.

Intervals

type Interval = Interval' SrcFile

type IntervalWithoutFile = Interval' ()

data Interval' a

An interval. The iEnd position is not included in the interval.

Note the invariant which intervals have to satisfy: intervalInvariant.

Constructors

Interval

Fields

• iStart, iEnd :: !(Position' a)

Instances

Functor Interval'

Defined in Agda.Syntax.Position

Methods

fmap :: (a -> b) -> Interval' a -> Interval' b

(<$) :: a -> Interval' b -> Interval' a

Show IntervalWithoutFile

Defined in Agda.Syntax.Position

Methods

showsPrec :: Int -> IntervalWithoutFile -> ShowS

show :: IntervalWithoutFile -> String

showList :: [IntervalWithoutFile] -> ShowS

Foldable Interval'

Defined in Agda.Syntax.Position

Methods

fold :: Monoid m => Interval' m -> m

foldMap :: Monoid m => (a -> m) -> Interval' a -> m

foldMap' :: Monoid m => (a -> m) -> Interval' a -> m

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

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

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

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

foldr1 :: (a -> a -> a) -> Interval' a -> a

foldl1 :: (a -> a -> a) -> Interval' a -> a

toList :: Interval' a -> [a]

null :: Interval' a -> Bool

length :: Interval' a -> Int

elem :: Eq a => a -> Interval' a -> Bool

maximum :: Ord a => Interval' a -> a

minimum :: Ord a => Interval' a -> a

sum :: Num a => Interval' a -> a

product :: Num a => Interval' a -> a

Traversable Interval'

Defined in Agda.Syntax.Position

Methods

traverse :: Applicative f => (a -> f b) -> Interval' a -> f (Interval' b)

sequenceA :: Applicative f => Interval' (f a) -> f (Interval' a)

mapM :: Monad m => (a -> m b) -> Interval' a -> m (Interval' b)

sequence :: Monad m => Interval' (m a) -> m (Interval' a)

Pretty IntervalWithoutFile

Defined in Agda.Syntax.Position

Methods

pretty :: IntervalWithoutFile -> Doc

prettyPrec :: Int -> IntervalWithoutFile -> Doc

prettyList :: [IntervalWithoutFile] -> Doc

HasRange Interval

Defined in Agda.Syntax.Position

Methods

getRange :: Interval -> Range

Eq a => Eq (Interval' a)

Defined in Agda.Syntax.Position

Methods

(==) :: Interval' a -> Interval' a -> Bool

(/=) :: Interval' a -> Interval' a -> Bool

Data a => Data (Interval' a)

Defined in Agda.Syntax.Position

Methods

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

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

toConstr :: Interval' a -> Constr

dataTypeOf :: Interval' a -> DataType

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

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

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

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

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

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

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

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

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

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

Ord a => Ord (Interval' a)

Defined in Agda.Syntax.Position

Methods

compare :: Interval' a -> Interval' a -> Ordering

(<) :: Interval' a -> Interval' a -> Bool

(<=) :: Interval' a -> Interval' a -> Bool

(>) :: Interval' a -> Interval' a -> Bool

(>=) :: Interval' a -> Interval' a -> Bool

max :: Interval' a -> Interval' a -> Interval' a

min :: Interval' a -> Interval' a -> Interval' a

Read a => Read (Interval' a)

Defined in Agda.Interaction.Base

Methods

readsPrec :: Int -> ReadS (Interval' a)

readList :: ReadS [Interval' a]

readPrec :: ReadPrec (Interval' a)

readListPrec :: ReadPrec [Interval' a]

Show a => Show (Interval' (Maybe a))

Defined in Agda.Syntax.Position

Methods

showsPrec :: Int -> Interval' (Maybe a) -> ShowS

show :: Interval' (Maybe a) -> String

showList :: [Interval' (Maybe a)] -> ShowS

Generic (Interval' a)

Defined in Agda.Syntax.Position

Associated Types

type Rep (Interval' a) :: Type -> Type

Methods

from :: Interval' a -> Rep (Interval' a) x

to :: Rep (Interval' a) x -> Interval' a

Pretty a => Pretty (Interval' (Maybe a))

Defined in Agda.Syntax.Position

Methods

pretty :: Interval' (Maybe a) -> Doc

prettyPrec :: Int -> Interval' (Maybe a) -> Doc

prettyList :: [Interval' (Maybe a)] -> Doc

EmbPrj a => EmbPrj (Interval' a)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Interval' a -> S Int32

icod_ :: Interval' a -> S Int32

value :: Int32 -> R (Interval' a)

type Rep (Interval' a)

Defined in Agda.Syntax.Position

type Rep (Interval' a) = D1 ('MetaData "Interval'" "Agda.Syntax.Position" "Agda-2.6.1.2-5kYg11u3V8c52jrcc71Agq" 'False) (C1 ('MetaCons "Interval" 'PrefixI 'True) (S1 ('MetaSel ('Just "iStart") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Position' a)) :*: S1 ('MetaSel ('Just "iEnd") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Position' a))))

intervalInvariant :: Ord a => Interval' a -> Bool

posToInterval :: a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a

Converts a file name and two positions to an interval.

getIntervalFile :: Interval' a -> a

Gets the srcFile component of the interval. Because of the invariant, they are both the same.

iLength :: Interval' a -> Int32

The length of an interval.

fuseIntervals :: Ord a => Interval' a -> Interval' a -> Interval' a

Finds the least interval which covers the arguments.

Precondition: The intervals must point to the same file.

setIntervalFile :: a -> Interval' b -> Interval' a

Sets the srcFile components of the interval.

Ranges

type Range = Range' SrcFile

data Range' a

A range is a file name, plus a sequence of intervals, assumed to point to the given file. The intervals should be consecutive and separated.

Note the invariant which ranges have to satisfy: rangeInvariant.

Constructors

NoRange

Range !a (Seq IntervalWithoutFile)

Instances

Functor Range'

Defined in Agda.Syntax.Position

Methods

fmap :: (a -> b) -> Range' a -> Range' b

(<$) :: a -> Range' b -> Range' a

Foldable Range'

Defined in Agda.Syntax.Position

Methods

fold :: Monoid m => Range' m -> m

foldMap :: Monoid m => (a -> m) -> Range' a -> m

foldMap' :: Monoid m => (a -> m) -> Range' a -> m

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

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

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

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

foldr1 :: (a -> a -> a) -> Range' a -> a

foldl1 :: (a -> a -> a) -> Range' a -> a

toList :: Range' a -> [a]

null :: Range' a -> Bool

length :: Range' a -> Int

elem :: Eq a => a -> Range' a -> Bool

maximum :: Ord a => Range' a -> a

minimum :: Ord a => Range' a -> a

sum :: Num a => Range' a -> a

product :: Num a => Range' a -> a

Traversable Range'

Defined in Agda.Syntax.Position

Methods

traverse :: Applicative f => (a -> f b) -> Range' a -> f (Range' b)

sequenceA :: Applicative f => Range' (f a) -> f (Range' a)

mapM :: Monad m => (a -> m b) -> Range' a -> m (Range' b)

sequence :: Monad m => Range' (m a) -> m (Range' a)

ToJSON Range

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: Range -> Value

toEncoding :: Range -> Encoding

toJSONList :: [Range] -> Value

toEncodingList :: [Range] -> Encoding

KillRange Range

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT Range

SetRange Range

Defined in Agda.Syntax.Position

Methods

setRange :: Range -> Range -> Range

HasRange Range

Defined in Agda.Syntax.Position

Methods

getRange :: Range -> Range

FreshName Range

Defined in Agda.TypeChecking.Monad.Base

Methods

freshName_ :: MonadFresh NameId m => Range -> m Name

EmbPrj Range

Ranges are always deserialised as noRange.

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Range -> S Int32

icod_ :: Range -> S Int32

value :: Int32 -> R Range

PrettyTCM Range

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Range -> m Doc

EncodeTCM Range

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: Range -> TCM Value

Subst Term Range

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' Term -> Range -> Range

LensClosure Range MetaInfo

Defined in Agda.TypeChecking.Monad.Base

Methods

lensClosure :: Lens' (Closure Range) MetaInfo

LensClosure Range MetaVariable

Defined in Agda.TypeChecking.Monad.Base

Methods

lensClosure :: Lens' (Closure Range) MetaVariable

Eq a => Eq (Range' a)

Defined in Agda.Syntax.Position

Methods

(==) :: Range' a -> Range' a -> Bool

(/=) :: Range' a -> Range' a -> Bool

Data a => Data (Range' a)

Defined in Agda.Syntax.Position

Methods

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

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

toConstr :: Range' a -> Constr

dataTypeOf :: Range' a -> DataType

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

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

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

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

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

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

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

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

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

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

Ord a => Ord (Range' a)

Defined in Agda.Syntax.Position

Methods

compare :: Range' a -> Range' a -> Ordering

(<) :: Range' a -> Range' a -> Bool

(<=) :: Range' a -> Range' a -> Bool

(>) :: Range' a -> Range' a -> Bool

(>=) :: Range' a -> Range' a -> Bool

max :: Range' a -> Range' a -> Range' a

min :: Range' a -> Range' a -> Range' a

Read a => Read (Range' a)

Note that the grammar implemented by this instance does not necessarily match the current representation of ranges.

Defined in Agda.Interaction.Base

Methods

readsPrec :: Int -> ReadS (Range' a)

readList :: ReadS [Range' a]

readPrec :: ReadPrec (Range' a)

readListPrec :: ReadPrec [Range' a]

Show a => Show (Range' (Maybe a))

Defined in Agda.Syntax.Position

Methods

showsPrec :: Int -> Range' (Maybe a) -> ShowS

show :: Range' (Maybe a) -> String

showList :: [Range' (Maybe a)] -> ShowS

Show a => Show (Range' (Maybe a))

Defined in Agda.Syntax.Position

Methods

showsPrec :: Int -> Range' (Maybe a) -> ShowS

show :: Range' (Maybe a) -> String

showList :: [Range' (Maybe a)] -> ShowS

Generic (Range' a)

Defined in Agda.Syntax.Position

Associated Types

type Rep (Range' a) :: Type -> Type

Methods

from :: Range' a -> Rep (Range' a) x

to :: Rep (Range' a) x -> Range' a

Null (Range' a)

Defined in Agda.Syntax.Position

Methods

empty :: Range' a

null :: Range' a -> Bool

Pretty a => Pretty (Range' (Maybe a))

Defined in Agda.Syntax.Position

Methods

pretty :: Range' (Maybe a) -> Doc

prettyPrec :: Int -> Range' (Maybe a) -> Doc

prettyList :: [Range' (Maybe a)] -> Doc

FreshName (Range, String)

Defined in Agda.TypeChecking.Monad.Base

Methods

freshName_ :: MonadFresh NameId m => (Range, String) -> m Name

type Rep (Range' a)

Defined in Agda.Syntax.Position

type Rep (Range' a) = D1 ('MetaData "Range'" "Agda.Syntax.Position" "Agda-2.6.1.2-5kYg11u3V8c52jrcc71Agq" 'False) (C1 ('MetaCons "NoRange" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Range" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Seq IntervalWithoutFile))))

rangeInvariant :: Ord a => Range' a -> Bool

Range invariant.

consecutiveAndSeparated :: Ord a => [Interval' a] -> Bool

Are the intervals consecutive and separated, do they all point to the same file, and do they satisfy the interval invariant?

intervalsToRange :: a -> [IntervalWithoutFile] -> Range' a

Turns a file name plus a list of intervals into a range.

Precondition: consecutiveAndSeparated.

intervalToRange :: a -> IntervalWithoutFile -> Range' a

Converts a file name and an interval to a range.

rangeIntervals :: Range' a -> [IntervalWithoutFile]

The intervals that make up the range. The intervals are consecutive and separated (consecutiveAndSeparated).

rangeFile :: Range -> SrcFile

The file the range is pointing to.

rightMargin :: Range -> Range

Conflate a range to its right margin.

noRange :: Range' a

Ranges between two unknown positions

posToRange :: Position' a -> Position' a -> Range' a

Converts two positions to a range.

Precondition: The positions have to point to the same file.

posToRange' :: a -> PositionWithoutFile -> PositionWithoutFile -> Range' a

Converts a file name and two positions to a range.

rStart :: Range' a -> Maybe (Position' a)

The initial position in the range, if any.

rStart' :: Range' a -> Maybe PositionWithoutFile

The initial position in the range, if any.

rEnd :: Range' a -> Maybe (Position' a)

The position after the final position in the range, if any.

rEnd' :: Range' a -> Maybe PositionWithoutFile

The position after the final position in the range, if any.

rangeToInterval :: Range' a -> Maybe IntervalWithoutFile

Converts a range to an interval, if possible. Note that the information about the source file is lost.

rangeToIntervalWithFile :: Range' a -> Maybe (Interval' a)

Converts a range to an interval, if possible.

continuous :: Range' a -> Range' a

Returns the shortest continuous range containing the given one.

continuousPerLine :: Ord a => Range' a -> Range' a

Removes gaps between intervals on the same line.

newtype PrintRange a

Wrapper to indicate that range should be printed.

Constructors

PrintRange a

Instances

Eq a => Eq (PrintRange a)

Defined in Agda.Syntax.Position

Methods

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

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

Ord a => Ord (PrintRange a)

Defined in Agda.Syntax.Position

Methods

compare :: PrintRange a -> PrintRange a -> Ordering

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

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

(>) :: PrintRange a -> PrintRange a -> Bool

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

max :: PrintRange a -> PrintRange a -> PrintRange a

min :: PrintRange a -> PrintRange a -> PrintRange a

(Pretty a, HasRange a) => Pretty (PrintRange a)

Defined in Agda.Syntax.Position

Methods

pretty :: PrintRange a -> Doc

prettyPrec :: Int -> PrintRange a -> Doc

prettyList :: [PrintRange a] -> Doc

KillRange a => KillRange (PrintRange a)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (PrintRange a)

SetRange a => SetRange (PrintRange a)

Defined in Agda.Syntax.Position

Methods

setRange :: Range -> PrintRange a -> PrintRange a

HasRange a => HasRange (PrintRange a)

Defined in Agda.Syntax.Position

Methods

getRange :: PrintRange a -> Range

class HasRange t where

Things that have a range are instances of this class.

Methods

getRange :: t -> Range

Instances

HasRange Bool

Defined in Agda.Syntax.Position

Methods

getRange :: Bool -> Range

HasRange ()

Defined in Agda.Syntax.Position

Methods

getRange :: () -> Range

HasRange Range

Defined in Agda.Syntax.Position

Methods

getRange :: Range -> Range

HasRange Interval

Defined in Agda.Syntax.Position

Methods

getRange :: Interval -> Range

HasRange GenPart

Defined in Agda.Syntax.Common

Methods

getRange :: GenPart -> Range

HasRange Fixity

Defined in Agda.Syntax.Common

Methods

getRange :: Fixity -> Range

HasRange IsMacro

Defined in Agda.Syntax.Common

Methods

getRange :: IsMacro -> Range

HasRange IsInstance

Defined in Agda.Syntax.Common

Methods

getRange :: IsInstance -> Range

HasRange Access

Defined in Agda.Syntax.Common

Methods

getRange :: Access -> Range

HasRange Cohesion

Defined in Agda.Syntax.Common

Methods

getRange :: Cohesion -> Range

HasRange Relevance

Defined in Agda.Syntax.Common

Methods

getRange :: Relevance -> Range

HasRange Quantity

Defined in Agda.Syntax.Common

Methods

getRange :: Quantity -> Range

HasRange QωOrigin

Defined in Agda.Syntax.Common

Methods

getRange :: QωOrigin -> Range

HasRange Q1Origin

Defined in Agda.Syntax.Common

Methods

getRange :: Q1Origin -> Range

HasRange Q0Origin

Defined in Agda.Syntax.Common

Methods

getRange :: Q0Origin -> Range

HasRange Induction

Defined in Agda.Syntax.Common

Methods

getRange :: Induction -> Range

HasRange HasEta

Defined in Agda.Syntax.Common

Methods

getRange :: HasEta -> Range

HasRange Layer

Defined in Agda.Syntax.Parser.Literate

Methods

getRange :: Layer -> Range

HasRange TopLevelModuleName

Defined in Agda.Syntax.Concrete.Name

Methods

getRange :: TopLevelModuleName -> Range

HasRange QName

Defined in Agda.Syntax.Concrete.Name

Methods

getRange :: QName -> Range

HasRange Name

Defined in Agda.Syntax.Concrete.Name

Methods

getRange :: Name -> Range

HasRange TCWarning

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: TCWarning -> Range

HasRange TCErr

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: TCErr -> Range

HasRange ParseWarning

Defined in Agda.Syntax.Parser.Monad

Methods

getRange :: ParseWarning -> Range

HasRange ParseError

Defined in Agda.Syntax.Parser.Monad

Methods

getRange :: ParseError -> Range

HasRange AmbiguousQName

The range of an AmbiguousQName is the range of any of its disambiguations (they are the same concrete name).

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: AmbiguousQName -> Range

HasRange ModuleName

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: ModuleName -> Range

HasRange QName

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: QName -> Range

HasRange Name

Defined in Agda.Syntax.Abstract.Name

Methods

getRange :: Name -> Range

HasRange Literal

Defined in Agda.Syntax.Literal

Methods

getRange :: Literal -> Range

HasRange Token

Defined in Agda.Syntax.Parser.Tokens

Methods

getRange :: Token -> Range

HasRange Pragma

Defined in Agda.Syntax.Concrete

Methods

getRange :: Pragma -> Range

HasRange ModuleApplication

Defined in Agda.Syntax.Concrete

Methods

getRange :: ModuleApplication -> Range

HasRange Declaration

Defined in Agda.Syntax.Concrete

Methods

getRange :: Declaration -> Range

HasRange AsName

Defined in Agda.Syntax.Concrete

Methods

getRange :: AsName -> Range

HasRange LamClause

Defined in Agda.Syntax.Concrete

Methods

getRange :: LamClause -> Range

HasRange WhereClause

Defined in Agda.Syntax.Concrete

Methods

getRange :: WhereClause -> Range

HasRange RHS

Defined in Agda.Syntax.Concrete

Methods

getRange :: RHS -> Range

HasRange LHSCore

Defined in Agda.Syntax.Concrete

Methods

getRange :: LHSCore -> Range

HasRange LHS

Defined in Agda.Syntax.Concrete

Methods

getRange :: LHS -> Range

HasRange TypedBinding

Defined in Agda.Syntax.Concrete

Methods

getRange :: TypedBinding -> Range

HasRange BoundName

Defined in Agda.Syntax.Concrete

Methods

getRange :: BoundName -> Range

HasRange LamBinding

Defined in Agda.Syntax.Concrete

Methods

getRange :: LamBinding -> Range

HasRange Binder

Defined in Agda.Syntax.Concrete

Methods

getRange :: Binder -> Range

HasRange DoStmt

Defined in Agda.Syntax.Concrete

Methods

getRange :: DoStmt -> Range

HasRange Pattern

Defined in Agda.Syntax.Concrete

Methods

getRange :: Pattern -> Range

HasRange Expr

Defined in Agda.Syntax.Concrete

Methods

getRange :: Expr -> Range

HasRange ModuleAssignment

Defined in Agda.Syntax.Concrete

Methods

getRange :: ModuleAssignment -> Range

HasRange Attribute

Defined in Agda.Syntax.Concrete.Attribute

Methods

getRange :: Attribute -> Range

HasRange AbstractName

Defined in Agda.Syntax.Scope.Base

Methods

getRange :: AbstractName -> Range

HasRange ConPatInfo

Defined in Agda.Syntax.Info

Methods

getRange :: ConPatInfo -> Range

HasRange PatInfo

Defined in Agda.Syntax.Info

Methods

getRange :: PatInfo -> Range

HasRange LHSInfo

Defined in Agda.Syntax.Info

Methods

getRange :: LHSInfo -> Range

HasRange MutualInfo

Defined in Agda.Syntax.Info

Methods

getRange :: MutualInfo -> Range

HasRange DeclInfo

Defined in Agda.Syntax.Info

Methods

getRange :: DeclInfo -> Range

HasRange LetInfo

Defined in Agda.Syntax.Info

Methods

getRange :: LetInfo -> Range

HasRange ModuleInfo

Defined in Agda.Syntax.Info

Methods

getRange :: ModuleInfo -> Range

HasRange AppInfo

Defined in Agda.Syntax.Info

Methods

getRange :: AppInfo -> Range

HasRange ExprInfo

Defined in Agda.Syntax.Info

Methods

getRange :: ExprInfo -> Range

HasRange MetaInfo

Defined in Agda.Syntax.Info

Methods

getRange :: MetaInfo -> Range

HasRange Clause

Defined in Agda.Syntax.Internal

Methods

getRange :: Clause -> Range

HasRange ConHead

Defined in Agda.Syntax.Internal

Methods

getRange :: ConHead -> Range

HasRange LHS

Defined in Agda.Syntax.Abstract

Methods

getRange :: LHS -> Range

HasRange SpineLHS

Defined in Agda.Syntax.Abstract

Methods

getRange :: SpineLHS -> Range

HasRange RHS

Defined in Agda.Syntax.Abstract

Methods

getRange :: RHS -> Range

HasRange WhereDeclarations

Defined in Agda.Syntax.Abstract

Methods

getRange :: WhereDeclarations -> Range

HasRange TypedBinding

Defined in Agda.Syntax.Abstract

Methods

getRange :: TypedBinding -> Range

HasRange LamBinding

Defined in Agda.Syntax.Abstract

Methods

getRange :: LamBinding -> Range

HasRange LetBinding

Defined in Agda.Syntax.Abstract

Methods

getRange :: LetBinding -> Range

HasRange Declaration

Defined in Agda.Syntax.Abstract

Methods

getRange :: Declaration -> Range

HasRange Expr

Defined in Agda.Syntax.Abstract

Methods

getRange :: Expr -> Range

HasRange BindName

Defined in Agda.Syntax.Abstract

Methods

getRange :: BindName -> Range

HasRange DeclarationWarning

Defined in Agda.Syntax.Concrete.Definitions

Methods

getRange :: DeclarationWarning -> Range

HasRange DeclarationException

Defined in Agda.Syntax.Concrete.Definitions

Methods

getRange :: DeclarationException -> Range

HasRange NiceDeclaration

Defined in Agda.Syntax.Concrete.Definitions

Methods

getRange :: NiceDeclaration -> Range

HasRange Call

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: Call -> Range

HasRange CompilerPragma

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: CompilerPragma -> Range

HasRange MetaInfo

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: MetaInfo -> Range

HasRange MetaVariable

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: MetaVariable -> Range

HasRange Constraint

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: Constraint -> Range

HasRange ProblemConstraint

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: ProblemConstraint -> Range

HasRange Item

Defined in Agda.TypeChecking.Positivity

Methods

getRange :: Item -> Range

HasRange HaskellPragma

Defined in Agda.Compiler.MAlonzo.Pragmas

Methods

getRange :: HaskellPragma -> Range

HasRange a => HasRange [a]

Precondition: The ranges of the list elements must point to the same file (or be empty).

Defined in Agda.Syntax.Position

Methods

getRange :: [a] -> Range

HasRange a => HasRange (Maybe a)

Defined in Agda.Syntax.Position

Methods

getRange :: Maybe a -> Range

HasRange a => HasRange (NonEmpty a)

Precondition: The ranges of the list elements must point to the same file (or be empty).

Defined in Agda.Syntax.Position

Methods

getRange :: NonEmpty a -> Range

HasRange a => HasRange (PrintRange a)

Defined in Agda.Syntax.Position

Methods

getRange :: PrintRange a -> Range

HasRange a => HasRange (MaybePlaceholder a)

Defined in Agda.Syntax.Common

Methods

getRange :: MaybePlaceholder a -> Range

HasRange (Ranged a)

Defined in Agda.Syntax.Common

Methods

getRange :: Ranged a -> Range

HasRange a => HasRange (Arg a)

Defined in Agda.Syntax.Common

Methods

getRange :: Arg a -> Range

HasRange a => HasRange (WithOrigin a)

Defined in Agda.Syntax.Common

Methods

getRange :: WithOrigin a -> Range

HasRange a => HasRange (WithHiding a)

Defined in Agda.Syntax.Common

Methods

getRange :: WithHiding a -> Range

HasRange a => HasRange (FieldAssignment' a)

Defined in Agda.Syntax.Concrete

Methods

getRange :: FieldAssignment' a -> Range

HasRange e => HasRange (OpApp e)

Defined in Agda.Syntax.Concrete

Methods

getRange :: OpApp e -> Range

IsExpr e => HasRange (ExprView e)

Defined in Agda.Syntax.Concrete.Operators.Parser

Methods

getRange :: ExprView e -> Range

HasRange (DefInfo' t)

Defined in Agda.Syntax.Info

Methods

getRange :: DefInfo' t -> Range

HasRange (Pattern' e)

Defined in Agda.Syntax.Abstract

Methods

getRange :: Pattern' e -> Range

HasRange (LHSCore' e)

Defined in Agda.Syntax.Abstract

Methods

getRange :: LHSCore' e -> Range

HasRange a => HasRange (Clause' a)

Defined in Agda.Syntax.Abstract

Methods

getRange :: Clause' a -> Range

HasRange a => HasRange (Binder' a)

Defined in Agda.Syntax.Abstract

Methods

getRange :: Binder' a -> Range

HasRange a => HasRange (Closure a)

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: Closure a -> Range

(HasRange a, HasRange b) => HasRange (Either a b)

Defined in Agda.Syntax.Position

Methods

getRange :: Either a b -> Range

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

Precondition: The ranges of the tuple elements must point to the same file (or be empty).

Defined in Agda.Syntax.Position

Methods

getRange :: (a, b) -> Range

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

Defined in Agda.Syntax.Common

Methods

getRange :: Renaming' a b -> Range

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

Defined in Agda.Syntax.Common

Methods

getRange :: ImportedName' a b -> Range

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

Defined in Agda.Syntax.Common

Methods

getRange :: Using' a b -> Range

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

Defined in Agda.Syntax.Common

Methods

getRange :: ImportDirective' a b -> Range

HasRange a => HasRange (Named name a)

Defined in Agda.Syntax.Common

Methods

getRange :: Named name a -> Range

HasRange a => HasRange (Dom' t a)

Defined in Agda.Syntax.Internal

Methods

getRange :: Dom' t a -> Range

(HasRange a, HasRange b, HasRange c) => HasRange (a, b, c)

Precondition: The ranges of the tuple elements must point to the same file (or be empty).

Defined in Agda.Syntax.Position

Methods

getRange :: (a, b, c) -> Range

(HasRange qn, HasRange p, HasRange e) => HasRange (RewriteEqn' qn p e)

Defined in Agda.Syntax.Common

Methods

getRange :: RewriteEqn' qn p e -> Range

(HasRange a, HasRange b, HasRange c, HasRange d) => HasRange (a, b, c, d)

Precondition: The ranges of the tuple elements must point to the same file (or be empty).

Defined in Agda.Syntax.Position

Methods

getRange :: (a, b, c, d) -> Range

(HasRange a, HasRange b, HasRange c, HasRange d, HasRange e) => HasRange (a, b, c, d, e)

Precondition: The ranges of the tuple elements must point to the same file (or be empty).

Defined in Agda.Syntax.Position

Methods

getRange :: (a, b, c, d, e) -> Range

(HasRange a, HasRange b, HasRange c, HasRange d, HasRange e, HasRange f) => HasRange (a, b, c, d, e, f)

Precondition: The ranges of the tuple elements must point to the same file (or be empty).

Defined in Agda.Syntax.Position

Methods

getRange :: (a, b, c, d, e, f) -> Range

(HasRange a, HasRange b, HasRange c, HasRange d, HasRange e, HasRange f, HasRange g) => HasRange (a, b, c, d, e, f, g)

Precondition: The ranges of the tuple elements must point to the same file (or be empty).

Defined in Agda.Syntax.Position

Methods

getRange :: (a, b, c, d, e, f, g) -> Range

class HasRange t => SetRange t where

If it is also possible to set the range, this is the class.

Instances should satisfy getRange (setRange r x) == r.

Methods

setRange :: Range -> t -> t

Instances

SetRange Range

Defined in Agda.Syntax.Position

Methods

setRange :: Range -> Range -> Range

SetRange GenPart

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> GenPart -> GenPart

SetRange Cohesion

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> Cohesion -> Cohesion

SetRange Relevance

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> Relevance -> Relevance

SetRange Quantity

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> Quantity -> Quantity

SetRange QωOrigin

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> QωOrigin -> QωOrigin

SetRange Q1Origin

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> Q1Origin -> Q1Origin

SetRange Q0Origin

Defined in Agda.Syntax.Common

Methods

setRange :: Range -> Q0Origin -> Q0Origin

SetRange TopLevelModuleName

Defined in Agda.Syntax.Concrete.Name

Methods

setRange :: Range -> TopLevelModuleName -> TopLevelModuleName

SetRange QName

Defined in Agda.Syntax.Concrete.Name

Methods

setRange :: Range -> QName -> QName

SetRange Name

Defined in Agda.Syntax.Concrete.Name

Methods

setRange :: Range -> Name -> Name

SetRange ModuleName

Defined in Agda.Syntax.Abstract.Name

Methods

setRange :: Range -> ModuleName -> ModuleName

SetRange QName

Defined in Agda.Syntax.Abstract.Name

Methods

setRange :: Range -> QName -> QName

SetRange Name

Defined in Agda.Syntax.Abstract.Name

Methods

setRange :: Range -> Name -> Name

SetRange Literal

Defined in Agda.Syntax.Literal

Methods

setRange :: Range -> Literal -> Literal

SetRange TypedBinding

Defined in Agda.Syntax.Concrete

Methods

setRange :: Range -> TypedBinding -> TypedBinding

SetRange Pattern

Defined in Agda.Syntax.Concrete

Methods

setRange :: Range -> Pattern -> Pattern

SetRange Attribute

Defined in Agda.Syntax.Concrete.Attribute

Methods

setRange :: Range -> Attribute -> Attribute

SetRange AbstractName

Defined in Agda.Syntax.Scope.Base

Methods

setRange :: Range -> AbstractName -> AbstractName

SetRange ConPatInfo

Defined in Agda.Syntax.Info

Methods

setRange :: Range -> ConPatInfo -> ConPatInfo

SetRange PatInfo

Defined in Agda.Syntax.Info

Methods

setRange :: Range -> PatInfo -> PatInfo

SetRange DeclInfo

Defined in Agda.Syntax.Info

Methods

setRange :: Range -> DeclInfo -> DeclInfo

SetRange ModuleInfo

Defined in Agda.Syntax.Info

Methods

setRange :: Range -> ModuleInfo -> ModuleInfo

SetRange ConHead

Defined in Agda.Syntax.Internal

Methods

setRange :: Range -> ConHead -> ConHead

SetRange BindName

Defined in Agda.Syntax.Abstract

Methods

setRange :: Range -> BindName -> BindName

SetRange MetaInfo

Defined in Agda.TypeChecking.Monad.Base

Methods

setRange :: Range -> MetaInfo -> MetaInfo

SetRange MetaVariable

Defined in Agda.TypeChecking.Monad.Base

Methods

setRange :: Range -> MetaVariable -> MetaVariable

SetRange a => SetRange [a]

Defined in Agda.Syntax.Position

Methods

setRange :: Range -> [a] -> [a]

SetRange a => SetRange (Maybe a)

Defined in Agda.Syntax.Position

Methods

setRange :: Range -> Maybe a -> Maybe a

SetRange a => SetRange (PrintRange a)

Defined in Agda.Syntax.Position

Methods

setRange :: Range -> PrintRange a -> PrintRange a

SetRange a => SetRange (Arg a)

Defined in Agda.Syntax.Common

Methods

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

SetRange a => SetRange (WithOrigin a)

Defined in Agda.Syntax.Common

Methods

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

SetRange a => SetRange (WithHiding a)

Defined in Agda.Syntax.Common

Methods

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

SetRange (DefInfo' t)

Defined in Agda.Syntax.Info

Methods

setRange :: Range -> DefInfo' t -> DefInfo' t

SetRange (Pattern' a)

Defined in Agda.Syntax.Abstract

Methods

setRange :: Range -> Pattern' a -> Pattern' a

SetRange a => SetRange (Named name a)

Defined in Agda.Syntax.Common

Methods

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

class KillRange a where

Killing the range of an object sets all range information to noRange.

Methods

killRange :: KillRangeT a

Instances

KillRange Bool

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT Bool

KillRange Int

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT Int

KillRange Integer

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT Integer

KillRange ()

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT ()

KillRange String

Overlaps with KillRange [a].

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT String

KillRange Void

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT Void

KillRange Range

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT Range

KillRange Permutation

Defined in Agda.Utils.Permutation

Methods

killRange :: KillRangeT Permutation

KillRange GenPart

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT GenPart

KillRange ExpandedEllipsis

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT ExpandedEllipsis

KillRange CoverageCheck

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT CoverageCheck

KillRange UniverseCheck

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT UniverseCheck

KillRange PositivityCheck

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT PositivityCheck

KillRange Fixity'

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Fixity'

KillRange Fixity

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Fixity

KillRange InteractionId

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT InteractionId

KillRange NameId

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT NameId

KillRange IsMacro

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT IsMacro

KillRange IsInstance

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT IsInstance

KillRange IsAbstract

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT IsAbstract

KillRange Access

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Access

KillRange ProjOrigin

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT ProjOrigin

KillRange ConOrigin

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT ConOrigin

KillRange ArgInfo

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT ArgInfo

KillRange Origin

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Origin

KillRange Cohesion

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Cohesion

KillRange Relevance

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Relevance

KillRange Quantity

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Quantity

KillRange QωOrigin

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT QωOrigin

KillRange Q1Origin

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Q1Origin

KillRange Q0Origin

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Q0Origin

KillRange Modality

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Modality

KillRange Hiding

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Hiding

KillRange Induction

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Induction

KillRange HasEta

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT HasEta

KillRange Delayed

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Delayed

KillRange TopLevelModuleName

Defined in Agda.Syntax.Concrete.Name

Methods

killRange :: KillRangeT TopLevelModuleName

KillRange QName

Defined in Agda.Syntax.Concrete.Name

Methods

killRange :: KillRangeT QName

KillRange Name

Defined in Agda.Syntax.Concrete.Name

Methods

killRange :: KillRangeT Name

KillRange Polarity

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT Polarity

KillRange AmbiguousQName

Defined in Agda.Syntax.Abstract.Name

Methods

killRange :: KillRangeT AmbiguousQName

KillRange ModuleName

Defined in Agda.Syntax.Abstract.Name

Methods

killRange :: KillRangeT ModuleName

KillRange QName

Defined in Agda.Syntax.Abstract.Name

Methods

killRange :: KillRangeT QName

KillRange Name

Defined in Agda.Syntax.Abstract.Name

Methods

killRange :: KillRangeT Name

KillRange Literal

Defined in Agda.Syntax.Literal

Methods

killRange :: KillRangeT Literal

KillRange Compiled

Defined in Agda.Syntax.Treeless

Methods

killRange :: KillRangeT Compiled

KillRange Occurrence

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

killRange :: KillRangeT Occurrence

KillRange Pragma

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT Pragma

KillRange ModuleApplication

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT ModuleApplication

KillRange Declaration

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT Declaration

KillRange AsName

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT AsName

KillRange LamClause

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT LamClause

KillRange WhereClause

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT WhereClause

KillRange RHS

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT RHS

KillRange LHS

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT LHS

KillRange TypedBinding

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT TypedBinding

KillRange BoundName

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT BoundName

KillRange LamBinding

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT LamBinding

KillRange Binder

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT Binder

KillRange DoStmt

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT DoStmt

KillRange Pattern

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT Pattern

KillRange Expr

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT Expr

KillRange ModuleAssignment

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT ModuleAssignment

KillRange SplitTag

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

killRange :: KillRangeT SplitTag

KillRange Attribute

Defined in Agda.Syntax.Concrete.Attribute

Methods

killRange :: KillRangeT Attribute

KillRange ScopeInfo

Defined in Agda.Syntax.Scope.Base

Methods

killRange :: KillRangeT ScopeInfo

KillRange ConPatInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT ConPatInfo

KillRange PatInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT PatInfo

KillRange LHSInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT LHSInfo

KillRange MutualInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT MutualInfo

KillRange DeclInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT DeclInfo

KillRange LetInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT LetInfo

KillRange ModuleInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT ModuleInfo

KillRange AppInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT AppInfo

KillRange ExprInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT ExprInfo

KillRange MetaInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT MetaInfo

KillRange Substitution

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Substitution

KillRange ConPatternInfo

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT ConPatternInfo

KillRange DBPatVar

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT DBPatVar

KillRange PatOrigin

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT PatOrigin

KillRange PatternInfo

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT PatternInfo

KillRange Clause

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Clause

KillRange LevelAtom

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT LevelAtom

KillRange PlusLevel

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT PlusLevel

KillRange Level

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Level

KillRange Sort

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Sort

KillRange Term

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Term

KillRange ConHead

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT ConHead

KillRange CompiledClauses

Defined in Agda.TypeChecking.CompiledClause

Methods

killRange :: KillRangeT CompiledClauses

KillRange LHS

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT LHS

KillRange SpineLHS

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT SpineLHS

KillRange RHS

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT RHS

KillRange WhereDeclarations

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT WhereDeclarations

KillRange ProblemEq

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT ProblemEq

KillRange DataDefParams

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT DataDefParams

KillRange GeneralizeTelescope

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT GeneralizeTelescope

KillRange TypedBinding

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT TypedBinding

KillRange LamBinding

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT LamBinding

KillRange LetBinding

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT LetBinding

KillRange ModuleApplication

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT ModuleApplication

KillRange Declaration

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT Declaration

KillRange ScopeCopyInfo

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT ScopeCopyInfo

KillRange Expr

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT Expr

KillRange BindName

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT BindName

KillRange MutualId

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT MutualId

KillRange TermHead

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT TermHead

KillRange Defn

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT Defn

KillRange CompKit

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT CompKit

KillRange FunctionFlag

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT FunctionFlag

KillRange EtaEquality

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT EtaEquality

KillRange ProjLams

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT ProjLams

KillRange Projection

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT Projection

KillRange ExtLamInfo

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT ExtLamInfo

KillRange System

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT System

KillRange CompiledRepresentation

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT CompiledRepresentation

KillRange IsForced

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT IsForced

KillRange NumGeneralizableArgs

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT NumGeneralizableArgs

KillRange Definition

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT Definition

KillRange RewriteRule

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT RewriteRule

KillRange NLPSort

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT NLPSort

KillRange NLPType

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT NLPType

KillRange NLPat

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT NLPat

KillRange DisplayTerm

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT DisplayTerm

KillRange DisplayForm

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT DisplayForm

KillRange Section

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT Section

KillRange RewriteRuleMap

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT RewriteRuleMap

KillRange Definitions

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT Definitions

KillRange Sections

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT Sections

KillRange Signature

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT Signature

KillRange DoGeneralize

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT DoGeneralize

KillRange a => KillRange [a]

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT [a]

KillRange a => KillRange (Maybe a)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (Maybe a)

KillRange a => KillRange (NonEmpty a)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (NonEmpty a)

(Ord a, KillRange a) => KillRange (Set a)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (Set a)

KillRange a => KillRange (Maybe a)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (Maybe a)

KillRange a => KillRange (PrintRange a)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (PrintRange a)

KillRange a => KillRange (Drop a)

Defined in Agda.Utils.Permutation

Methods

killRange :: KillRangeT (Drop a)

KillRange m => KillRange (TerminationCheck m)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (TerminationCheck m)

KillRange a => KillRange (MaybePlaceholder a)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (MaybePlaceholder a)

KillRange (Ranged a)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (Ranged a)

KillRange a => KillRange (Arg a)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (Arg a)

KillRange a => KillRange (WithOrigin a)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (WithOrigin a)

KillRange a => KillRange (WithHiding a)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (WithHiding a)

KillRange x => KillRange (ThingWithFixity x)

Defined in Agda.Syntax.Fixity

Methods

killRange :: KillRangeT (ThingWithFixity x)

KillRange a => KillRange (FieldAssignment' a)

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT (FieldAssignment' a)

KillRange e => KillRange (OpApp e)

Defined in Agda.Syntax.Concrete

Methods

killRange :: KillRangeT (OpApp e)

KillRange a => KillRange (SplitTree' a)

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

killRange :: KillRangeT (SplitTree' a)

KillRange t => KillRange (DefInfo' t)

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT (DefInfo' t)

KillRange a => KillRange (Pattern' a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Pattern' a)

KillRange a => KillRange (Blocked a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Blocked a)

KillRange a => KillRange (Tele a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Tele a)

KillRange a => KillRange (Type' a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Type' a)

KillRange a => KillRange (Abs a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Abs a)

KillRange a => KillRange (Elim' a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Elim' a)

KillRange c => KillRange (Case c)

Defined in Agda.TypeChecking.CompiledClause

Methods

killRange :: KillRangeT (Case c)

KillRange c => KillRange (WithArity c)

Defined in Agda.TypeChecking.CompiledClause

Methods

killRange :: KillRangeT (WithArity c)

KillRange e => KillRange (Pattern' e)

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT (Pattern' e)

KillRange e => KillRange (LHSCore' e)

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT (LHSCore' e)

KillRange a => KillRange (Clause' a)

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT (Clause' a)

KillRange a => KillRange (Binder' a)

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT (Binder' a)

KillRange c => KillRange (FunctionInverse' c)

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT (FunctionInverse' c)

KillRange a => KillRange (Open a)

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT (Open a)

KillRange a => KillRange (Closure a)

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT (Closure a)

(KillRange a, KillRange b) => KillRange (Either a b)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (Either a b)

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

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (a, b)

KillRange a => KillRange (Map k a)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (Map k a)

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

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (Renaming' a b)

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

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (ImportedName' a b)

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

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (Using' a b)

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

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (ImportDirective' a b)

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

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (Named name a)

(KillRange t, KillRange a) => KillRange (Dom' t a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Dom' t a)

(KillRange a, KillRange b, KillRange c) => KillRange (a, b, c)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (a, b, c)

(KillRange qn, KillRange e, KillRange p) => KillRange (RewriteEqn' qn p e)

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT (RewriteEqn' qn p e)

(KillRange a, KillRange b, KillRange c, KillRange d) => KillRange (a, b, c, d)

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (a, b, c, d)

type KillRangeT a = a -> a

killRangeMap :: (KillRange k, KillRange v) => KillRangeT (Map k v)

Remove ranges in keys and values of a map.

killRange1 :: KillRange a => (a -> b) -> a -> b

killRange2 :: (KillRange a, KillRange b) => (a -> b -> c) -> a -> b -> c

killRange3 :: (KillRange a, KillRange b, KillRange c) => (a -> b -> c -> d) -> a -> b -> c -> d

killRange4 :: (KillRange a, KillRange b, KillRange c, KillRange d) => (a -> b -> c -> d -> e) -> a -> b -> c -> d -> e

killRange5 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e) => (a -> b -> c -> d -> e -> f) -> a -> b -> c -> d -> e -> f

killRange6 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f) => (a -> b -> c -> d -> e -> f -> g) -> a -> b -> c -> d -> e -> f -> g

killRange7 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g) => (a -> b -> c -> d -> e -> f -> g -> h) -> a -> b -> c -> d -> e -> f -> g -> h

killRange8 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h) => (a -> b -> c -> d -> e -> f -> g -> h -> i) -> a -> b -> c -> d -> e -> f -> g -> h -> i

killRange9 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j

killRange10 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k

killRange11 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l

killRange12 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m

killRange13 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n

killRange14 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o

killRange15 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p

killRange16 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o, KillRange p) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q

killRange17 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o, KillRange p, KillRange q) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r

killRange18 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o, KillRange p, KillRange q, KillRange r) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s

killRange19 :: (KillRange a, KillRange b, KillRange c, KillRange d, KillRange e, KillRange f, KillRange g, KillRange h, KillRange i, KillRange j, KillRange k, KillRange l, KillRange m, KillRange n, KillRange o, KillRange p, KillRange q, KillRange r, KillRange s) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s -> t) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m -> n -> o -> p -> q -> r -> s -> t

withRangeOf :: (SetRange t, HasRange u) => t -> u -> t

x `withRangeOf` y sets the range of x to the range of y.

fuseRange :: (HasRange u, HasRange t) => u -> t -> Range

Precondition: The ranges must point to the same file (or be empty).

fuseRanges :: Ord a => Range' a -> Range' a -> Range' a

fuseRanges r r' unions the ranges r and r'.

Meaning it finds the least range r0 that covers r and r'.

Precondition: The ranges must point to the same file (or be empty).

beginningOf :: Range -> Range

beginningOf r is an empty range (a single, empty interval) positioned at the beginning of r. If r does not have a beginning, then noRange is returned.

beginningOfFile :: Range -> Range

beginningOfFile r is an empty range (a single, empty interval) at the beginning of r's starting position's file. If there is no such position, then an empty range is returned.

interleaveRanges :: HasRange a => [a] -> [a] -> ([a], [(a, a)])

Interleaves two streams of ranged elements

It will report the conflicts as a list of conflicting pairs. In case of conflict, the element with the earliest start position is placed first. In case of a tie, the element with the earliest ending position is placed first. If both tie, the element from the first list is placed first.