`module Lb: ``sig end`

The module

`Lb`

specifies the set of constant lower bounds.`type t `

The type of constant lower bound.

`val bottom : ``t`

`bottom`

is a distinguished lower bound. It is the bottom
element of the semi-lattice.`val is_bottom : ``t -> bool`

`is_bottom lb`

must return `true`

if and only if `lb`

is `bottom`

.`val union : ``t -> t -> t`

`union lb1 lb2`

gives the union (according to the semi-lattice
structure) of the lower bounds `lb1`

and `lb2`

.`val leq : ``t -> t -> bool`

`leq env lb1 lb2`

tells wether `lb1`

is less than or equal to
`lb2`

in the semi-lattice of constant lower bounds, i.e.:
for all alpha, `lb2 < alpha`

implies `lb1 < alpha`

.`val compare : ``t -> t -> int`

A comparison function on constant lower bounds has to be
provided. It is just used for computation and has no semantical
meaning.

`val normalize : ``t -> t`

`normalize lb`

internally normalizes the lower bound lb.`val fprint : ``Format.formatter -> t -> unit`

`fprint ppf lb`

pretty-prints the constant lower bound `lb`

on
the formatter `ppf`

. (This function is used for printing of
constants in constraints.)`val fprint_in_term : ``int -> Format.formatter -> t -> unit`

`fprint_in_term ppf lb`

is used to prints the constant lower
bound `lb`

on the formatter `ppf`

when it appears in a term, in
place of a non-negative variable which has no predecessor.
An usual implementation may be:
let fprint_in_term _ ppf lb =
Format.fprintf ppf "`> %a`

" fprint lb

`val draw : ``t -> string list`