Idris2Doc : Text.Bounded

Text.Bounded

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

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

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