Range: reformat show instance, allows clicking in VScode to work #373
Annotations
10 warnings
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/FStar.TSet.fst#L28
(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.TSet.fst:28.4-28.7:
- Values of type `set` cannot be erased during extraction, but the
`must_erase_for_extraction` attribute claims that it can.
- Please remove the attribute.
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fsti:435.8-435.51:
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fst:293.8-293.25:
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
- See also /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fsti:435.8-435.51
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fsti:435.8-435.51:
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
dummy#L1
(242) * Warning 242 at ulib/FStar.WellFounded.fst:122.0-131.33:
- Definitions of inner let-rec aux and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: ulib/FStar.WellFounded.fst:86.12-86.15
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
dummy#L1
(242) * Warning 242 at ulib/FStar.WellFounded.fst:122.0-131.33:
- Definitions of inner let-rec aux and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: ulib/FStar.WellFounded.fst:126.12-126.15
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
ulib/FStar.GhostSet.fst#L23
(318) * Warning 318 at ulib/FStar.GhostSet.fst:23.4-23.7:
- Values of type `set` cannot be erased during extraction, but the
`must_erase_for_extraction` attribute claims that it can.
- Please remove the attribute.
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
ulib/experimental/FStar.MST.fst#L222
(330) * Warning 330 at ulib/experimental/FStar.MST.fst:222.43-222.55:
- Polymonadic binds ((DIV, MSTATE) |> MSTATE) in this case) is an experimental
feature;it is subject to some redesign in the future. Please keep us
informed (on github etc.) about how you are using it
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
ulib/experimental/FStar.MST.fst#L247
(352) * Warning 352 at ulib/experimental/FStar.MST.fst:247.42-247.60:
- Combinator FStar.MSTTotal.MSTATETOT ~> FStar.MST.MSTATE is not a
substitutive indexed effect combinator, it is better to make it one if
possible for better performance and ease of use
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
ulib/FStar.GSet.fst#L23
(318) * Warning 318 at ulib/FStar.GSet.fst:23.4-23.7:
- Values of type `set` cannot be erased during extraction, but the
`must_erase_for_extraction` attribute claims that it can.
- Please remove the attribute.
|
Loading