Idris2Doc : Text.Bounded

Text.Bounded

Definitions

recordBounds : Type
Totality: total
Visibility: public export
Constructor: 
MkBounds : Int->Int->Int->Int->Bounds

Projections:
.endCol : Bounds->Int
.endLine : Bounds->Int
.startCol : Bounds->Int
.startLine : Bounds->Int

Hints:
EqBounds
ShowBounds
.startLine : Bounds->Int
Totality: total
Visibility: public export
startLine : Bounds->Int
Totality: total
Visibility: public export
.startCol : Bounds->Int
Totality: total
Visibility: public export
startCol : Bounds->Int
Totality: total
Visibility: public export
.endLine : Bounds->Int
Totality: total
Visibility: public export
endLine : Bounds->Int
Totality: total
Visibility: public export
.endCol : Bounds->Int
Totality: total
Visibility: public export
endCol : Bounds->Int
Totality: total
Visibility: public export
startBounds : Bounds-> (Int, Int)
Totality: total
Visibility: export
endBounds : Bounds-> (Int, Int)
Totality: total
Visibility: export
recordWithBounds : Type->Type
Totality: total
Visibility: public export
Constructor: 
MkBounded : ty->Bool->Bounds->WithBoundsty

Projections:
.bounds : WithBoundsty->Bounds
.isIrrelevant : WithBoundsty->Bool
.val : WithBoundsty->ty

Hints:
Eqty=>Eq (WithBoundsty)
FoldableWithBounds
FunctorWithBounds
Showty=>Show (WithBoundsty)
TraversableWithBounds
.val : WithBoundsty->ty
Totality: total
Visibility: public export
val : WithBoundsty->ty
Totality: total
Visibility: public export
.isIrrelevant : WithBoundsty->Bool
Totality: total
Visibility: public export
isIrrelevant : WithBoundsty->Bool
Totality: total
Visibility: public export
.bounds : WithBoundsty->Bounds
Totality: total
Visibility: public export
bounds : WithBoundsty->Bounds
Totality: total
Visibility: public export
start : WithBoundsty-> (Int, Int)
Totality: total
Visibility: export
end : WithBoundsty-> (Int, Int)
Totality: total
Visibility: export
irrelevantBounds : ty->WithBoundsty
Totality: total
Visibility: export
removeIrrelevance : WithBoundsty->WithBoundsty
Totality: total
Visibility: export
mergeBounds : WithBoundsty->WithBoundsty'->WithBoundsty'
Totality: total
Visibility: export
joinBounds : WithBounds (WithBoundsty) ->WithBoundsty
Totality: total
Visibility: export