let nat_tm = R.pack_ln (R.Tv_FVar nat_fv)
let nat_tm =
R.pack_ln (R.Tv_FVar nat_fv)
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.V2.Builtins.pack_ln FStar.Reflection.V2.Data.Tv_FVar Pulse.Reflection.Util.nat_fv
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"]
val nat_tm : FStar.Reflection.Types.term
FStar.Reflection.Types.term