let tm_bind binder head body = Tm_Bind { binder; head; body }
let tm_bind binder head body =
Tm_Bind ({ binder = binder; head = head; 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.binder Pulse.Syntax.Base.st_term Pulse.Syntax.Base.Tm_Bind Pulse.Syntax.Base.Mkst_term'__Tm_Bind__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 }
val tm_bind : binder: Pulse.Syntax.Base.binder ->
    head: Pulse.Syntax.Base.st_term ->
    body: Pulse.Syntax.Base.st_term
  -> Pulse.Syntax.Base.st_term'

    binder: Pulse.Syntax.Base.binder ->
    head: Pulse.Syntax.Base.st_term ->
    body: Pulse.Syntax.Base.st_term
  -> Pulse.Syntax.Base.st_term'