Libraries.Text.Bounded

Definitions

record Bounds : Type

Totality: total
Visibility: public export
Constructor: 

MkBounds : Int -> Int -> Int -> Int -> Bounds

Projections:

.endCol : Bounds -> Int

  0-based first column after bound

.endLine : Bounds -> Int

  0-based last line of bound

.startCol : Bounds -> Int

  0-based first col

.startLine : Bounds -> Int

  0-based first line

Hints:

Eq Bounds

Show Bounds

.startLine : Bounds -> Int

  0-based first line

Totality: total
Visibility: public export

startLine : Bounds -> Int

  0-based first line

Totality: total
Visibility: public export

.startCol : Bounds -> Int

  0-based first col

Totality: total
Visibility: public export

startCol : Bounds -> Int

  0-based first col

Totality: total
Visibility: public export

.endLine : Bounds -> Int

  0-based last line of bound

Totality: total
Visibility: public export

endLine : Bounds -> Int

  0-based last line of bound

Totality: total
Visibility: public export

.endCol : Bounds -> Int

  0-based first column after bound

Totality: total
Visibility: public export

endCol : Bounds -> Int

  0-based first column after bound

Totality: total
Visibility: public export

startBounds : Bounds -> (Int, Int)

Totality: total
Visibility: export

endBounds : Bounds -> (Int, Int)

Totality: total
Visibility: export

union : Bounds -> Bounds -> Bounds

Totality: total
Visibility: export

record WithBounds : Type -> Type

Totality: total
Visibility: public export
Constructor: 

MkBounded : ty -> Bool -> Bounds -> WithBounds ty

Projections:

.bounds : WithBounds ty -> Bounds

.isIrrelevant : WithBounds ty -> Bool

.val : WithBounds ty -> ty

Hints:

Eq ty => Eq (WithBounds ty)

Foldable WithBounds

Functor WithBounds

Show ty => Show (WithBounds ty)

Traversable WithBounds

.val : WithBounds ty -> ty

Totality: total
Visibility: public export

val : WithBounds ty -> ty

Totality: total
Visibility: public export

.isIrrelevant : WithBounds ty -> Bool

Totality: total
Visibility: public export

isIrrelevant : WithBounds ty -> Bool

Totality: total
Visibility: public export

.bounds : WithBounds ty -> Bounds

Totality: total
Visibility: public export

bounds : WithBounds ty -> Bounds

Totality: total
Visibility: public export

start : WithBounds ty -> (Int, Int)

Totality: total
Visibility: export

end : WithBounds ty -> (Int, Int)

Totality: total
Visibility: export

irrelevantBounds : ty -> WithBounds ty

Totality: total
Visibility: export

removeIrrelevance : WithBounds ty -> WithBounds ty

Totality: total
Visibility: export

mergeBounds : WithBounds ty -> WithBounds ty' -> WithBounds ty'

Totality: total
Visibility: export

joinBounds : WithBounds (WithBounds ty) -> WithBounds ty

Totality: total
Visibility: export