INNER CODE UNIT · JavaScript

mkFStar

FStarLang/karamel · krmllib/js/loader.js:197

let mkFStar = () => dummyModule(
  [ "FStar_UInt128_constant_time_carry_ok", "FStar_PropositionalExtensionality_axiom" ],
  [ "FStar_Monotonic_Heap_lemma_mref_injectivity" ]);

let mkLowStar = (mem) => ({
  LowStar_Monotonic_Buffer_is_null: (addr) => (addr == 0)
});

let mkSteelReference = (mem) => ({
  Steel_Reference_is_null: (addr) => (addr == 0)
});

let mkPrims = (mem) => ({
  Prims_op_Addition: (x, y) => { return x + y; }
});

let mkC = (mem) => ({
  srand: () => { throw new Error("todo: srand") },

View source record →