let tm_while invariant condition condition_var body = Tm_While { invariant; condition; condition_var; body }
let tm_while invariant condition condition_var body =
Tm_While
({ invariant = invariant; condition = condition; condition_var = condition_var; body = body })
Pulse.Syntax.Builder.fst.checked
Pulse.Syntax.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked
Pulse.Syntax.Builder.fst
Pulse.Syntax.Base.term Pulse.Syntax.Base.st_term Pulse.Syntax.Base.ppname Pulse.Syntax.Base.Tm_While Pulse.Syntax.Base.Mkst_term'__Tm_While__payload Pulse.Syntax.Base.st_term'
module Pulse.Syntax.Builder
open Pulse.Syntax

let pat_var s = Pat_Var s
let pat_const c = Pat_Constant c
let pat_cons fv vs = Pat_Cons fv vs

let tm_return ctag insert_eq term = Tm_Return { ctag; insert_eq; term }
let tm_abs b q ascription body = Tm_Abs { b; q; ascription; body }
let tm_stapp head arg_qual arg = Tm_STApp { head; arg_qual; arg }
let tm_bind binder head body = Tm_Bind { binder; head; body }
let tm_totbind binder head body = Tm_TotBind { binder; head; body }
let tm_if b then_ else_ post = Tm_If { b; then_; else_; post }
let tm_match sc returns_ brs = Tm_Match {sc; returns_; brs}
let tm_elim_exists p = Tm_ElimExists { p }
val tm_while : invariant: Pulse.Syntax.Base.term ->
    condition: Pulse.Syntax.Base.st_term ->
    condition_var: Pulse.Syntax.Base.ppname ->
    body: Pulse.Syntax.Base.st_term
  -> Pulse.Syntax.Base.st_term'

    invariant: Pulse.Syntax.Base.term ->
    condition: Pulse.Syntax.Base.st_term ->
    condition_var: Pulse.Syntax.Base.ppname ->
    body: Pulse.Syntax.Base.st_term
  -> Pulse.Syntax.Base.st_term'