val fits (x: int) : Tot prop
let fits x =
  FStar.Int.fits x I64.n == true /\
  x <= max_bound /\ x >= min_bound
val fits (x: int) : Tot prop
let fits x =
FStar.Int.fits x I64.n == true /\ x <= max_bound /\ x >= min_bound
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
Prims.int Prims.l_and Prims.eq2 Prims.bool FStar.Int.fits FStar.Int64.n Prims.b2t Prims.op_LessThanOrEqual FStar.Ghost.reveal FStar.PtrdiffT.max_bound Prims.op_GreaterThanOrEqual FStar.PtrdiffT.min_bound Prims.prop
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 max_bound : x:erased int { x >= pow2 15 - 1 }
let min_bound : erased int = hide (- (reveal max_bound + 1))

(** We also assume that size_t is wider than ptrdiff_t *)
assume
val bounds_lemma (_:unit) : Lemma (SizeT.bound > max_bound)

let t = x:I64.t{I64.v x >= min_bound /\ I64.v x <= max_bound }
val fits (x: int) : Tot prop
x: Prims.int -> Prims.prop