Skip to main content

Browse the archive

Revision cef6a8e821f55e71b791555d22b45bd3debc2596 authored by Jonathan Protzenko on 08 May 2020, 16:26:29 UTC, committed by GitHub on 08 May 2020, 16:26:29 UTC 
Merge pull request #298 from project-everest/vdum_ocaml_nits
 
OCaml API: Don't run unit tests which require unsupported features
2 parent s 760addb + 28f416c
Raw File
Vale.X64.Flags.fst.hints 
[
  "��W���\u0017m�Y�͚�t�",
  [
    [
      "Vale.X64.Flags.upd",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.X64.Flags.flag_val_t", "equation_Vale.X64.Flags.t",
        "equation_Vale.X64.Machine_s.flag",
        "function_token_typing_Vale.X64.Flags.flag_val_t", "int_inversion",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Map.lemma_InDomUpd1",
        "lemma_FStar.Set.lemma_equal_elim",
        "lemma_FStar.Set.lemma_equal_intro",
        "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_empty",
        "primitive_Prims.op_BarBar", "primitive_Prims.op_Negation",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_2ea34cbc8e73c89468af536d5146da5a",
        "refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64",
        "typing_FStar.Map.domain", "typing_FStar.Map.upd",
        "typing_FStar.Set.complement", "typing_FStar.Set.empty",
        "typing_Vale.X64.Machine_s.flag"
      ],
      0,
      "f81a5ad3c12f74e6bf82fb6f0cdba97f"
    ],
    [
      "Vale.X64.Flags.of_fun",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Vale.X64.Flags_interpretation_Tm_arrow_6d1d81ae558d658d7d34082785eb5144",
        "data_typing_intro_FStar.Pervasives.Native.None@tok",
        "equation_Prims.eqtype", "equation_Vale.X64.Flags.flag_val_t",
        "equation_Vale.X64.Machine_s.flag",
        "function_token_typing_Prims.bool",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.X64.Flags.flag_val_t",
        "haseqTm_refine_a29663a141e931174462ff96f2d1bbb5", "int_inversion",
        "int_typing", "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Map.lemma_InDomConstMap",
        "lemma_FStar.Map.lemma_SelUpd1", "lemma_FStar.Map.lemma_SelUpd2",
        "lemma_FStar.Map.lemma_UpdDomain",
        "lemma_FStar.Set.lemma_equal_elim",
        "lemma_FStar.Set.lemma_equal_intro",
        "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_empty",
        "lemma_FStar.Set.mem_union", "primitive_Prims.op_BarBar",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Negation", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64",
        "refinement_interpretation_Tm_refine_a29663a141e931174462ff96f2d1bbb5",
        "refinement_kinding_Tm_refine_a29663a141e931174462ff96f2d1bbb5",
        "typing_FStar.Map.const", "typing_FStar.Map.domain",
        "typing_FStar.Map.upd", "typing_FStar.Set.complement",
        "typing_FStar.Set.empty", "typing_FStar.Set.singleton",
        "typing_FStar.Set.union", "typing_Vale.X64.Machine_s.flag"
      ],
      0,
      "8c332660635067e63dd733f6516de158"
    ],
    [
      "Vale.X64.Flags.lemma_upd_eq",
      1,
      1,
      0,
      [
        "@query", "function_token_typing_Vale.X64.Flags.sel",
        "function_token_typing_Vale.X64.Flags.upd",
        "interpretation_Tm_abs_9fabf848a1a32f51b141d5916bad7662",
        "interpretation_Tm_abs_dee13f6801a03886b79150447bc19803"
      ],
      0,
      "65ba459e06c9d90641c015f5a85a958a"
    ],
    [
      "Vale.X64.Flags.lemma_upd_ne",
      1,
      1,
      0,
      [
        "@query", "function_token_typing_Vale.X64.Flags.sel",
        "function_token_typing_Vale.X64.Flags.upd",
        "interpretation_Tm_abs_9fabf848a1a32f51b141d5916bad7662",
        "interpretation_Tm_abs_dee13f6801a03886b79150447bc19803"
      ],
      0,
      "0d9b58a8dfebb535ca1f2f333823a58c"
    ],
    [
      "Vale.X64.Flags.lemma_equal_intro",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_Vale.X64.Flags.equal",
        "equation_Vale.X64.Flags.flag_val_t", "equation_Vale.X64.Flags.t",
        "equation_Vale.X64.Machine_s.flag",
        "function_token_typing_Vale.X64.Flags.flag_val_t",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Map.lemma_equal_elim",
        "lemma_FStar.Set.lemma_equal_elim",
        "refinement_interpretation_Tm_refine_2ea34cbc8e73c89468af536d5146da5a",
        "typing_FStar.Map.domain", "typing_FStar.Set.complement",
        "typing_FStar.Set.empty", "typing_Vale.X64.Machine_s.flag"
      ],
      0,
      "4e76aff233552761f5570485ba55269d"
    ],
    [
      "Vale.X64.Flags.lemma_equal_elim",
      1,
      1,
      0,
      [
        "@query", "eq2-interp", "equation_Vale.X64.Flags.equal",
        "equation_Vale.X64.Flags.t"
      ],
      0,
      "17a8cb83fde5dd48d46198774eb669a9"
    ]
  ]
]
back to top