[
  "�\f3�)dXs��\u001aM�6zF",
  [
    [
      "Lib.Meta.int_of_hex",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.Meta.hex_digit",
        "equation_Lib.Meta.is_hex_digit",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_edb0c372e7bf797bdba364efa56489b6"
      ],
      0,
      "d848c0b69bdac97fa342bbefaecd1c01"
    ],
    [
      "Lib.Meta.as_uint8s",
      1,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.for_all.fuel_instrumented",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_FStar.List.Tot.Base.for_all.fuel_instrumented",
        "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "FStar.Char_pretyping_dc6ef56115bc91878da75a1e0625bb73",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_84543425b818e2d10a976186b8e8c250",
        "Lib.Meta_interpretation_Tm_arrow_fc1554671c39653ed371206100dcafd3",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_7a3bde9139992c29f781a4ea3ad13323_0",
        "binder_x_febb71ea7321b0772979ace745cc37ac_1", "bool_inversion",
        "constructor_distinct_BoxBool",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Prims.Cons", "constructor_distinct_Tm_unit",
        "data_typing_intro_Prims.Cons@tok", "disc_equation_Prims.Cons",
        "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Prims.LexTop@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Meta.byte_of_hex", "equation_Lib.Meta.hex_digit",
        "equation_Lib.Meta.int_of_hex", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "equation_with_fuel_FStar.List.Tot.Base.for_all.fuel_instrumented",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Lib.Meta.is_hex_digit",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Prims.Cons_tl", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7aac12c24449a22c34d98a0ea8ed4a32",
        "refinement_interpretation_Tm_refine_b338ec010a48764c17c429acaf5dcd17",
        "refinement_interpretation_Tm_refine_edb0c372e7bf797bdba364efa56489b6",
        "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "token_correspondence_Lib.Meta.is_hex_digit",
        "typing_FStar.Char.char", "typing_FStar.List.Tot.Base.length",
        "typing_FStar.List.Tot.Base.rev", "typing_Lib.Meta.int_of_hex",
        "typing_Lib.Meta.is_hex_digit",
        "typing_Prims.__proj__Cons__item__tl", "well-founded-ordering-on-nat"
      ],
      0,
      "51e882d6f16baa648dd719734d2748a7"
    ],
    [
      "Lib.Meta.from_hex",
      1,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit",
        "data_typing_intro_Prims.Nil@tok", "equation_FStar.String.char",
        "equation_FStar.String.strlen", "equation_Lib.IntTypes.uint8",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Modulus", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
        "refinement_interpretation_Tm_refine_2b2ea413658c5044b7d9307ce2d5d7af",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_9534f2540b2b63f27bcbd9837be1dc1b",
        "refinement_interpretation_Tm_refine_95bb7de2948a613291f9a441b0fcca14",
        "string_inversion", "typing_FStar.Char.char",
        "typing_FStar.String.list_of_string", "typing_FStar.String.strlen"
      ],
      0,
      "07c823809e66883684272a0e16900fb9"
    ]
  ]
]