Idris2Doc : Text.Bounded

Text.Bounded

recordBounds : Type
Totality: total
Constructor: 
MkBounds : Int -> Int -> Int -> Int -> Bounds

Projections:
.endCol : Bounds -> Int
.endLine : Bounds -> Int
.startCol : Bounds -> Int
.startLine : Bounds -> Int
recordWithBounds : Type -> Type
Totality: total
Constructor: 
MkBounded : ty -> Bool -> Bounds -> WithBoundsty

Projections:
.bounds : WithBoundsty -> Bounds
.isIrrelevant : WithBoundsty -> Bool
.val : WithBoundsty -> ty
end : WithBoundsty -> (Int, Int)
Totality: total
endBounds : Bounds -> (Int, Int)
Totality: total
irrelevantBounds : ty -> WithBoundsty
Totality: total
joinBounds : WithBounds (WithBoundsty) -> WithBoundsty
Totality: total
mergeBounds : WithBoundsty -> WithBoundsty' -> WithBoundsty'
Totality: total
removeIrrelevance : WithBoundsty -> WithBoundsty
Totality: total
start : WithBoundsty -> (Int, Int)
Totality: total
startBounds : Bounds -> (Int, Int)
Totality: total