val option_to_string : (#a : Type) -> (a -> Tac string) -> option a -> Tac string
let option_to_string #a f x =
  match x with
  | None -> "None"
  | Some x' -> "Some (" ^ f x' ^ ")"
val option_to_string : (#a : Type) -> (a -> Tac string) -> option a -> Tac string
let option_to_string #a f x =
match x with
| None -> "None"
| Some x' -> "Some (" ^ f x' ^ ")"
FStar.InteractiveHelpers.Base.fst.checked
prims.fst.checked FStar.Tactics.Util.fst.checked FStar.Tactics.fst.checked FStar.Sealed.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Order.fst.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked
FStar.InteractiveHelpers.Base.fst
Prims.string FStar.Pervasives.Native.option Prims.op_Hat
module FStar.InteractiveHelpers.Base

open FStar.List
open FStar.Tactics
open FStar.Mul

#push-options "--z3rlimit 15 --fuel 0 --ifuel 1"

(*** Utilities *)
val bv_eq : bv -> bv -> Tot bool
let bv_eq (bv1 bv2 : bv) =
  let bvv1 = inspect_bv bv1 in
  let bvv2 = inspect_bv bv2 in
  (* We don't check for type equality: the fact that no two different binders
   * have the same name and index is an invariant which must be enforced -
   * and actually we could limit ourselves to checking the index *)
  bvv1.bv_index = bvv2.bv_index

val fv_eq : fv -> fv -> Tot bool
let fv_eq fv1 fv2 =
  let n1 = inspect_fv fv1 in
  let n2 = inspect_fv fv2 in
  n1 = n2

// TODO: use everywhere
val fv_eq_name : fv -> name -> Tot bool
let fv_eq_name fv n =
  let fvn = inspect_fv fv in
  fvn = n

// TODO: use more
val opt_apply (#a #b : Type) (f : a -> Tot b) (x : option a) : Tot (option b)
let opt_apply #a #b f x =
  match x with
  | None -> None
  | Some x' -> Some (f x')

val opt_tapply (#a #b : Type) (f : a -> Tac b) (x : option a) : Tac (option b)
let opt_tapply #a #b f x =
  match x with
  | None -> None
  | Some x' -> Some (f x')

val option_to_string : (#a : Type) -> (a -> Tac string) -> option a -> Tac string
val option_to_string : (#a : Type) -> (a -> Tac string) -> option a -> Tac string
f: (_: a -> FStar.Tactics.Effect.Tac Prims.string) -> x: FStar.Pervasives.Native.option a
  -> FStar.Tactics.Effect.Tac Prims.string