Erase functions to fun #164
Annotations
10 warnings
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/FStar.Set.fst#L25
(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Set.fst(25,4-25,9):
- Values of type `equal` will be erased during extraction, but its interface
hides this fact.
- Add the `erasable` attribute to the `val equal` declaration for this symbol
in the interface
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/FStar.Ghost.fst#L24
(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Ghost.fst(24,4-24,8):
- Values of type `hide` will be erased during extraction, but its interface
hides this fact.
- Add the `erasable` attribute to the `val hide` declaration for this symbol
in the interface
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/FStar.Pervasives.fst#L38
(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Pervasives.fst(38,4-38,11):
- Values of type `ambient` will be erased during extraction, but its interface
hides this fact.
- Add the `erasable` attribute to the `val ambient` declaration for this
symbol in the interface
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/FStar.Pervasives.fst#L138
(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Pervasives.fst(138,4-138,13):
- Values of type `inversion` will be erased during extraction, but its
interface hides this fact.
- Add the `erasable` attribute to the `val inversion` declaration for this
symbol in the interface
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/FStar.Monotonic.Heap.fst#L31
(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Monotonic.Heap.fst(31,4-31,9):
- Values of type `equal` will be erased during extraction, but its interface
hides this fact.
- Add the `erasable` attribute to the `val equal` declaration for this symbol
in the interface
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/FStar.Monotonic.Heap.fst#L56
(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Monotonic.Heap.fst(56,4-56,12):
- Values of type `contains` will be erased during extraction, but its
interface hides this fact.
- Add the `erasable` attribute to the `val contains` declaration for this
symbol in the interface
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/FStar.Monotonic.Heap.fst#L62
(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Monotonic.Heap.fst(62,4-62,18):
- Values of type `addr_unused_in` will be erased during extraction, but its
interface hides this fact.
- Add the `erasable` attribute to the `val addr_unused_in` declaration for
this symbol in the interface
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/FStar.Monotonic.Heap.fst#L66
(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Monotonic.Heap.fst(66,4-66,13):
- Values of type `unused_in` will be erased during extraction, but its
interface hides this fact.
- Add the `erasable` attribute to the `val unused_in` declaration for this
symbol in the interface
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/FStar.Monotonic.Heap.fst#L275
(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Monotonic.Heap.fst(275,4-275,18):
- Values of type `aref_unused_in` will be erased during extraction, but its
interface hides this fact.
- Add the `erasable` attribute to the `val aref_unused_in` declaration for
this symbol in the interface
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/FStar.Monotonic.Heap.fst#L280
(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Monotonic.Heap.fst(280,4-280,16):
- Values of type `aref_live_at` will be erased during extraction, but its
interface hides this fact.
- Add the `erasable` attribute to the `val aref_live_at` declaration for this
symbol in the interface
|
Loading