package why3find

  1. Overview
  2. Docs

Module Why3findUtils.RangeSource

Sourcetype pos = private {
  1. line : int;
  2. col : int;
}

Boundaries, line and column internally starts at 0, but pretty-printed to starts at 1

Sourcetype range = pos * pos
Sourceval (<<) : pos -> pos -> bool
Sourceval (<<=) : pos -> pos -> bool
Sourceval (<<<) : range -> range -> bool
Sourceval start : pos
Sourceval next : pos -> pos
Sourceval prev : pos -> pos
Sourceval newline : pos -> pos
Sourceval after : pos -> char -> pos
Sourceval at : ?line:int -> ?col:int -> unit -> pos

Line and col starts at 0.

Sourceval pp_pos : Format.formatter -> pos -> unit
Sourceval pp_range : Format.formatter -> range -> unit
Sourceval pp_position : Format.formatter -> file:string -> range -> unit
Sourceval empty : range
Sourceval is_empty : range -> bool
Sourceval inside : pos -> range -> bool
Sourceval subset : range -> range -> bool
Sourceval disjoint : range -> range -> bool
Sourceval union : range -> range -> range
Sourceval diff : range -> range -> range
Sourceval first_line : range -> int
Sourceval last_line : range -> int