If there is a let foo = 42 in the fsti file, we currently have two entries in the dataset. For example:
val to_uint_t (m: nat) (a: int) : Tot (uint_t m)
let to_uint_t (m:nat) (a:int) : Tot (uint_t m) = a % pow2 m
One is in FStar.UInt.fsti.checked, one is in FStar.UInt.fst.checked.
If there is a
let foo = 42in thefstifile, we currently have two entries in the dataset. For example:One is in
FStar.UInt.fsti.checked, one is inFStar.UInt.fst.checked.