let tm_abs b q ascription body = Tm_Abs { b; q; ascription; body }
let tm_abs b q ascription body =
Tm_Abs ({ b = b; q = q; ascription = ascription; 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 FStar.Pervasives.Native.option Pulse.Syntax.Base.qualifier Pulse.Syntax.Base.comp Pulse.Syntax.Base.st_term Pulse.Syntax.Base.Tm_Abs Pulse.Syntax.Base.Mkst_term'__Tm_Abs__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
val tm_abs : b: Pulse.Syntax.Base.binder ->
    q: FStar.Pervasives.Native.option Pulse.Syntax.Base.qualifier ->
    ascription: Pulse.Syntax.Base.comp ->
    body: Pulse.Syntax.Base.st_term
  -> Pulse.Syntax.Base.st_term'

    b: Pulse.Syntax.Base.binder ->
    q: FStar.Pervasives.Native.option Pulse.Syntax.Base.qualifier ->
    ascription: Pulse.Syntax.Base.comp ->
    body: Pulse.Syntax.Base.st_term
  -> Pulse.Syntax.Base.st_term'