let tm_return ctag insert_eq term = Tm_Return { ctag; insert_eq; term }
let tm_return ctag insert_eq term =
Tm_Return ({ ctag = ctag; insert_eq = insert_eq; term = term })
Pulse.Syntax.Builder.fst.checked
Pulse.Syntax.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked
Pulse.Syntax.Builder.fst
Pulse.Syntax.Base.ctag Prims.bool Pulse.Syntax.Base.term Pulse.Syntax.Base.Tm_Return Pulse.Syntax.Base.Mkst_term'__Tm_Return__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_return : ctag: Pulse.Syntax.Base.ctag -> insert_eq: Prims.bool -> term: Pulse.Syntax.Base.term
  -> Pulse.Syntax.Base.st_term'
ctag: Pulse.Syntax.Base.ctag -> insert_eq: Prims.bool -> term: Pulse.Syntax.Base.term
  -> Pulse.Syntax.Base.st_term'