Module Pickles_types.Nat

Representation of naturals for Pickles

Type definitions

type z =
| Z of z

z is uninhabited

type 'a s =
| Z
| S of 'a
type _ t =
| Z : z t
| S : 'n t -> 'n s t
type 'a nat = 'a t
type e =
| T : 'n nat -> e

Modules

module type Intf = sig ... end
module Adds : sig ... end
module Lte : sig ... end
module Add : sig ... end
module type I = Add.Intf_transparent

Module encoding naturals

module N0 : I with type 'a plus_n = 'a
module N1 : I with type 'a plus_n = 'a s
module N2 : I with type 'a plus_n = 'a N1.plus_n s
module N3 : I with type 'a plus_n = 'a N2.plus_n s
module N4 : I with type 'a plus_n = 'a N3.plus_n s
module N5 : I with type 'a plus_n = 'a N4.plus_n s
module N6 : I with type 'a plus_n = 'a N5.plus_n s
module N7 : I with type 'a plus_n = 'a N6.plus_n s
module N8 : I with type 'a plus_n = 'a N7.plus_n s
module N9 : I with type 'a plus_n = 'a N8.plus_n s
module N10 : I with type 'a plus_n = 'a N9.plus_n s
module N11 : I with type 'a plus_n = 'a N10.plus_n s
module N12 : I with type 'a plus_n = 'a N11.plus_n s
module N13 : I with type 'a plus_n = 'a N12.plus_n s
module N14 : I with type 'a plus_n = 'a N13.plus_n s
module N15 : I with type 'a plus_n = 'a N14.plus_n s
module N16 : I with type 'a plus_n = 'a N15.plus_n s
module N17 : I with type 'a plus_n = 'a N16.plus_n s
module N18 : I with type 'a plus_n = 'a N17.plus_n s
module N19 : I with type 'a plus_n = 'a N18.plus_n s
module N20 : I with type 'a plus_n = 'a N19.plus_n s
module N21 : I with type 'a plus_n = 'a N20.plus_n s
module N22 : I with type 'a plus_n = 'a N21.plus_n s
module N23 : I with type 'a plus_n = 'a N22.plus_n s
module N24 : I with type 'a plus_n = 'a N23.plus_n s
module N25 : I with type 'a plus_n = 'a N24.plus_n s
module N26 : I with type 'a plus_n = 'a N25.plus_n s
module N27 : I with type 'a plus_n = 'a N26.plus_n s
module N28 : I with type 'a plus_n = 'a N27.plus_n s
module N29 : I with type 'a plus_n = 'a N28.plus_n s
module N30 : I with type 'a plus_n = 'a N29.plus_n s
module N31 : I with type 'a plus_n = 'a N30.plus_n s
module N32 : I with type 'a plus_n = 'a N31.plus_n s
module N33 : I with type 'a plus_n = 'a N32.plus_n s
module N34 : I with type 'a plus_n = 'a N33.plus_n s
module N35 : I with type 'a plus_n = 'a N34.plus_n s
module N36 : I with type 'a plus_n = 'a N35.plus_n s
module N37 : I with type 'a plus_n = 'a N36.plus_n s
module N38 : I with type 'a plus_n = 'a N37.plus_n s
module N39 : I with type 'a plus_n = 'a N38.plus_n s
module N40 : I with type 'a plus_n = 'a N39.plus_n s
module N41 : I with type 'a plus_n = 'a N40.plus_n s
module N42 : I with type 'a plus_n = 'a N41.plus_n s
module N43 : I with type 'a plus_n = 'a N42.plus_n s
module N44 : I with type 'a plus_n = 'a N43.plus_n s
module N45 : I with type 'a plus_n = 'a N44.plus_n s
module N46 : I with type 'a plus_n = 'a N45.plus_n s
module N47 : I with type 'a plus_n = 'a N46.plus_n s
module N48 : I with type 'a plus_n = 'a N47.plus_n s
module Empty : sig ... end
module Not : sig ... end

Functions

val to_int : 'n. 'n t -> int
val of_int : int -> e
val lte_exn : 'a nat -> 'b nat -> ( 'a, 'b ) Lte.t
val eq_exn : 'n 'm. 'n nat -> 'm nat -> ( 'n, 'm ) Core_kernel.Type_equal.t
val compare : 'n 'm. 'n t -> 'm t -> [ `Lte of ( 'n, 'm ) Lte.t | `Gt of ( 'n, 'm ) Lte.t Not.t ]
val gt_implies_gte : 'n 'm. 'n nat -> 'm nat -> ( 'n, 'm ) Lte.t Not.t -> ( 'm, 'n ) Lte.t