Agda- A dependently typed functional programming language and proof assistant

Safe HaskellSafe-Infered






data Range Source

Character ranges. The first character in the file has position 1. Note that the to position is considered to be outside of the range.

Invariant: from <= to.




from :: Integer
to :: Integer

rangeInvariant :: Range -> BoolSource

The Range invariant.

overlapping :: Range -> Range -> BoolSource

True iff the ranges overlap.

The ranges are assumed to be well-formed.

toList :: Range -> [Integer]Source

Converts a range to a list of positions.

getRanges :: Name -> ([Range], Bool)Source

Calculates a set of ranges associated with a name.

For an operator the ranges associated with the NameParts are returned. Otherwise the range associated with the Name is returned.

A boolean, indicating operatorness, is also returned.

getRangesA :: QName -> ([Range], Bool)Source

Like getRanges, but for QNames. Note that the module part of the name is thrown away; only the base part is used.

rToR :: Range -> [Range]Source

Converts a Range to a list of Ranges.

tests :: IO BoolSource

All the properties.