val mk_fst (u1 u2: R.universe) (a1 a2 e: R.term) : R.term
let mk_fst (u1 u2:R.universe) (a1 a2 e:R.term) : R.term =
  let open R in
  let t = pack_ln (Tv_UInst (pack_fv fst_lid) [u1; u2]) in
  let t = pack_ln (Tv_App t (a1, Q_Implicit)) in
  let t = pack_ln (Tv_App t (a2, Q_Implicit)) in
  pack_ln (Tv_App t (e, Q_Explicit))
val mk_fst (u1 u2: R.universe) (a1 a2 e: R.term) : R.term
let mk_fst (u1 u2: R.universe) (a1 a2 e: R.term) : R.term =
let open R in
let t = pack_ln (Tv_UInst (pack_fv fst_lid) [u1; u2]) in
let t = pack_ln (Tv_App t (a1, Q_Implicit)) in
let t = pack_ln (Tv_App t (a2, Q_Implicit)) in
pack_ln (Tv_App t (e, Q_Explicit))
Pulse.Reflection.Util.fst.checked
Pulse.RuntimeUtils.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Ghost.fsti.checked
Pulse.Reflection.Util.fst
FStar.Reflection.Types.universe FStar.Reflection.Types.term FStar.Reflection.V2.Builtins.pack_ln FStar.Reflection.V2.Data.Tv_App FStar.Pervasives.Native.Mktuple2 FStar.Reflection.V2.Data.aqualv FStar.Reflection.V2.Data.Q_Explicit FStar.Reflection.V2.Data.Q_Implicit FStar.Reflection.V2.Data.Tv_UInst FStar.Reflection.V2.Builtins.pack_fv Pulse.Reflection.Util.fst_lid Prims.Cons Prims.Nil
module Pulse.Reflection.Util

module R = FStar.Reflection.V2
module T = FStar.Tactics.V2
module RT = FStar.Reflection.Typing
module RU = Pulse.RuntimeUtils
open FStar.List.Tot

let pulse_lib_core = ["Pulse"; "Lib"; "Core"]
let mk_pulse_lib_core_lid s = pulse_lib_core@[s]

let tun = R.pack_ln R.Tv_Unknown
let unit_lid = R.unit_lid
let bool_lid = R.bool_lid
let int_lid  = R.int_lid
let erased_lid = ["FStar"; "Ghost"; "erased"]
let hide_lid = ["FStar"; "Ghost"; "hide"]
let reveal_lid = ["FStar"; "Ghost"; "reveal"]
let vprop_lid = mk_pulse_lib_core_lid "vprop"
let vprop_fv = R.pack_fv vprop_lid
let vprop_tm = R.pack_ln (R.Tv_FVar vprop_fv)
let unit_fv = R.pack_fv unit_lid
let unit_tm = R.pack_ln (R.Tv_FVar unit_fv)
let bool_fv = R.pack_fv bool_lid
let bool_tm = R.pack_ln (R.Tv_FVar bool_fv)
let nat_lid = ["Prims"; "nat"]
let nat_fv = R.pack_fv nat_lid
let nat_tm = R.pack_ln (R.Tv_FVar nat_fv)
let szt_lid = ["FStar"; "SizeT"; "t"]
let szt_fv = R.pack_fv szt_lid
let szt_tm = R.pack_ln (R.Tv_FVar szt_fv)
let szv_lid = ["FStar"; "SizeT"; "v"]
let szv_fv = R.pack_fv szv_lid
let szv_tm = R.pack_ln (R.Tv_FVar szv_fv)
let seq_lid = ["FStar"; "Seq"; "Base"; "seq"]
let seq_create_lid = ["FStar"; "Seq"; "Base"; "create"]


let tuple2_lid = ["FStar"; "Pervasives"; "Native"; "tuple2"]
let fst_lid = ["FStar"; "Pervasives"; "Native"; "fst"]
let snd_lid = ["FStar"; "Pervasives"; "Native"; "snd"]

let mk_tuple2 (u1 u2:R.universe) (a1 a2:R.term) : R.term =
  let open R in
  let t = pack_ln (Tv_UInst (pack_fv tuple2_lid) [u1; u2]) in
  let t = pack_ln (Tv_App t (a1, Q_Explicit)) in
  pack_ln (Tv_App t (a2, Q_Explicit))
val mk_fst (u1 u2: R.universe) (a1 a2 e: R.term) : R.term

    u1: FStar.Reflection.Types.universe ->
    u2: FStar.Reflection.Types.universe ->
    a1: FStar.Reflection.Types.term ->
    a2: FStar.Reflection.Types.term ->
    e: FStar.Reflection.Types.term
  -> FStar.Reflection.Types.term