let simpl_norm_steps = [primops; simplify; iota]
let simpl_norm_steps =
[primops; simplify; iota]
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
Prims.Cons FStar.Pervasives.norm_step FStar.Pervasives.primops FStar.Pervasives.simplify FStar.Pervasives.iota Prims.Nil
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
let proposition_to_string p = term_to_string p

/// Propositions split between pre and post assertions
noeq type assertions = {
  pres : list proposition;
  posts : list proposition;
}

let mk_assertions pres posts : assertions =
  Mkassertions pres posts

(*** Simplification *)
/// Whenever we generate assertions, we simplify them to make them cleaner,
/// prettier and remove the trivial ones. The normalization steps we apply
val simpl_norm_steps : Prims.list FStar.Pervasives.norm_step
Prims.list FStar.Pervasives.norm_step