val min_bound:erased int
let min_bound : erased int = hide (- (reveal max_bound + 1))
val min_bound:erased int
let min_bound:erased int =
hide (- (reveal max_bound + 1))
FStar.PtrdiffT.fst.checked
prims.fst.checked FStar.SizeT.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lib.fst.checked FStar.Int64.fsti.checked FStar.Int.Cast.fst.checked FStar.Int.fsti.checked FStar.Ghost.fsti.checked
FStar.PtrdiffT.fst
FStar.Ghost.hide Prims.int Prims.op_Minus Prims.op_Addition FStar.Ghost.reveal FStar.PtrdiffT.max_bound
module FStar.PtrdiffT

module Cast = FStar.Int.Cast
module I64 = FStar.Int64

open FStar.Ghost

friend FStar.SizeT

(** We assume the existence of lower and upper bounds corresponding to PTRDIFF_MIN
    and PTRDIFF_MAX, which ensure that a ptrdiff_t has at least width 16 according to
    the C standard *)
assume
val min_bound:erased int
FStar.Ghost.erased Prims.int