val proposition_to_string : proposition -> Tac string
let proposition_to_string p = term_to_string p
val proposition_to_string : proposition -> Tac string
let proposition_to_string p =
term_to_string p
FStar.InteractiveHelpers.Propositions.fst.checked
prims.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.fst.checked FStar.InteractiveHelpers.ExploreTerm.fst.checked FStar.InteractiveHelpers.Base.fst.checked
FStar.InteractiveHelpers.Propositions.fst
FStar.InteractiveHelpers.Propositions.proposition FStar.Tactics.V1.Builtins.term_to_string Prims.string
module FStar.InteractiveHelpers.Propositions

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

let term_eq = FStar.Tactics.term_eq_old

/// Propositions and assertions.
/// Assertions are propositions to be inserted in the F* code: we differentiate
/// between pre and post assertions, which are to be inserted before a point in
/// the code. For instance, if we analyze an effectful term in F*:
/// [> assert(y <> 0); // pre assertion
/// [> let z = x / y in // term of interest
/// [> assert(...); // post assertion

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

/// Analyze a term to retrieve its effectful information

type proposition = term
val proposition_to_string : proposition -> Tac string
p: FStar.InteractiveHelpers.Propositions.proposition -> FStar.Tactics.Effect.Tac Prims.string