Frama-C:
Plug-ins:
Libraries:

Frama-C API - Nat

type zero = |
type 'n succ = |
type 'n nat
type positive_or_null =
  1. | PositiveOrNull : 'n nat -> positive_or_null
type strictly_positive =
  1. | StrictlyPositive : 'n succ nat -> strictly_positive
val zero : zero nat
val one : zero succ nat
val succ : 'n nat -> 'n succ nat
val prev : 'n succ nat -> 'n nat
val to_int : 'n nat -> int
val of_int : int -> positive_or_null option
val of_strictly_positive_int : int -> strictly_positive option