let tm_stapp head arg_qual arg = Tm_STApp { head; arg_qual; arg }
let tm_stapp head arg_qual arg =
Tm_STApp ({ head = head; arg_qual = arg_qual; arg = arg })
Pulse.Syntax.Builder.fst.checked
Pulse.Syntax.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked
Pulse.Syntax.Builder.fst
Pulse.Syntax.Base.term FStar.Pervasives.Native.option Pulse.Syntax.Base.qualifier Pulse.Syntax.Base.Tm_STApp Pulse.Syntax.Base.Mkst_term'__Tm_STApp__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 }
val tm_stapp : head: Pulse.Syntax.Base.term ->
    arg_qual: FStar.Pervasives.Native.option Pulse.Syntax.Base.qualifier ->
    arg: Pulse.Syntax.Base.term
  -> Pulse.Syntax.Base.st_term'

    head: Pulse.Syntax.Base.term ->
    arg_qual: FStar.Pervasives.Native.option Pulse.Syntax.Base.qualifier ->
    arg: Pulse.Syntax.Base.term
  -> Pulse.Syntax.Base.st_term'