val cast_info_to_string : cast_info -> Tac string
let cast_info_to_string info =
  "Mkcast_info (" ^ term_to_string info.term ^ ") (" ^
  option_to_string type_info_to_string info.p_ty ^ ") (" ^
  option_to_string type_info_to_string info.exp_ty ^ ")"
val cast_info_to_string : cast_info -> Tac string
let cast_info_to_string info =
"Mkcast_info (" ^
term_to_string info.term ^
") (" ^
option_to_string type_info_to_string info.p_ty ^
") (" ^ option_to_string type_info_to_string info.exp_ty ^ ")"
FStar.InteractiveHelpers.Effectful.fst.checked
prims.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.InteractiveHelpers.Propositions.fst.checked FStar.InteractiveHelpers.ExploreTerm.fst.checked FStar.InteractiveHelpers.Base.fst.checked FStar.HyperStack.fst.checked
FStar.InteractiveHelpers.Effectful.fst
FStar.InteractiveHelpers.Effectful.cast_info Prims.op_Hat Prims.string FStar.InteractiveHelpers.Base.option_to_string FStar.InteractiveHelpers.ExploreTerm.type_info FStar.InteractiveHelpers.ExploreTerm.type_info_to_string FStar.InteractiveHelpers.Effectful.__proj__Mkcast_info__item__exp_ty FStar.InteractiveHelpers.Effectful.__proj__Mkcast_info__item__p_ty FStar.Tactics.V1.Builtins.term_to_string FStar.InteractiveHelpers.Effectful.__proj__Mkcast_info__item__term
module FStar.InteractiveHelpers.Effectful

module HS = FStar.HyperStack

open FStar.List
open FStar.Tactics
open FStar.Mul
open FStar.InteractiveHelpers.Base
open FStar.InteractiveHelpers.ExploreTerm
open FStar.InteractiveHelpers.Propositions

let term_eq = FStar.Tactics.term_eq_old

/// Effectful term analysis: retrieve information about an effectful term, including
/// its return type, its arguments, its correctly instantiated pre/postcondition, etc.

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


(*** Effectful term analysis *)
/// Cast information
noeq type cast_info = {
  term : term;
  p_ty : option type_info; // The type of the term
  exp_ty : option type_info; // The type of the expected parameter
}

let mk_cast_info t p_ty exp_ty : cast_info =
  Mkcast_info t p_ty exp_ty

val cast_info_to_string : cast_info -> Tac string
val cast_info_to_string : cast_info -> Tac string
info: FStar.InteractiveHelpers.Effectful.cast_info -> FStar.Tactics.Effect.Tac Prims.string