feat(lean): add negated condition to while loop spec #1863
Merged
Annotations
10 warnings
|
dummy#L0
(321) * Warning 321:
- Did not expect module FStar.Pervasives to be already checked.
- Found it in an unexpected location:
/nix/store/lk8466gkmpa7m9602xrc34s41q7phfzk-ocaml5.3.0-fstar-7b347386330d0e5a331a220535b6f15288903234/lib/fstar/ulib.checked/FStar.Pervasives.fst.checked
instead of /tmp/nix-shell.vy9tRk/tmp.hXG1ZC8eHP/FStar.Pervasives.fst.checked
|
|
dummy#L0
(321) * Warning 321:
- Did not expect module FStar.Pervasives.Native to be already checked.
- Found it in an unexpected location:
/nix/store/lk8466gkmpa7m9602xrc34s41q7phfzk-ocaml5.3.0-fstar-7b347386330d0e5a331a220535b6f15288903234/lib/fstar/ulib.checked/FStar.Pervasives.Native.fst.checked
instead of
/tmp/nix-shell.vy9tRk/tmp.hXG1ZC8eHP/FStar.Pervasives.Native.fst.checked
|
|
dummy#L0
(321) * Warning 321:
- Did not expect module FStar.Pervasives to be already checked.
- Found it in an unexpected location:
/nix/store/lk8466gkmpa7m9602xrc34s41q7phfzk-ocaml5.3.0-fstar-7b347386330d0e5a331a220535b6f15288903234/lib/fstar/ulib.checked/FStar.Pervasives.fsti.checked
instead of
/tmp/nix-shell.vy9tRk/tmp.hXG1ZC8eHP/FStar.Pervasives.fsti.checked
|
|
dummy#L0
(321) * Warning 321:
- Did not expect module FStar.NormSteps to be already checked.
- Found it in an unexpected location:
/nix/store/lk8466gkmpa7m9602xrc34s41q7phfzk-ocaml5.3.0-fstar-7b347386330d0e5a331a220535b6f15288903234/lib/fstar/ulib.checked/FStar.NormSteps.fst.checked
instead of /tmp/nix-shell.vy9tRk/tmp.hXG1ZC8eHP/FStar.NormSteps.fst.checked
|
|
dummy#L0
(321) * Warning 321:
- Did not expect module FStar.NormSteps to be already checked.
- Found it in an unexpected location:
/nix/store/lk8466gkmpa7m9602xrc34s41q7phfzk-ocaml5.3.0-fstar-7b347386330d0e5a331a220535b6f15288903234/lib/fstar/ulib.checked/FStar.NormSteps.fsti.checked
instead of /tmp/nix-shell.vy9tRk/tmp.hXG1ZC8eHP/FStar.NormSteps.fsti.checked
|
|
dummy#L0
(321) * Warning 321:
- Did not expect module FStar.Attributes to be already checked.
- Found it in an unexpected location:
/nix/store/lk8466gkmpa7m9602xrc34s41q7phfzk-ocaml5.3.0-fstar-7b347386330d0e5a331a220535b6f15288903234/lib/fstar/ulib.checked/FStar.Attributes.fsti.checked
instead of
/tmp/nix-shell.vy9tRk/tmp.hXG1ZC8eHP/FStar.Attributes.fsti.checked
|
|
dummy#L0
(321) * Warning 321:
- Did not expect module FStar.Prelude to be already checked.
- Found it in an unexpected location:
/nix/store/lk8466gkmpa7m9602xrc34s41q7phfzk-ocaml5.3.0-fstar-7b347386330d0e5a331a220535b6f15288903234/lib/fstar/ulib.checked/FStar.Prelude.fsti.checked
instead of /tmp/nix-shell.vy9tRk/tmp.hXG1ZC8eHP/FStar.Prelude.fsti.checked
|
|
dummy#L0
(321) * Warning 321:
- Did not expect module Prims to be already checked.
- Found it in an unexpected location:
/nix/store/lk8466gkmpa7m9602xrc34s41q7phfzk-ocaml5.3.0-fstar-7b347386330d0e5a331a220535b6f15288903234/lib/fstar/ulib.checked/Prims.fst.checked
instead of /tmp/nix-shell.vy9tRk/tmp.hXG1ZC8eHP/Prims.fst.checked
|
|
dummy#L0
(321) * Warning 321:
- Did not expect module FStar.Mul to be already checked.
- Found it in an unexpected location:
/nix/store/lk8466gkmpa7m9602xrc34s41q7phfzk-ocaml5.3.0-fstar-7b347386330d0e5a331a220535b6f15288903234/lib/fstar/ulib.checked/FStar.Mul.fst.checked
instead of /tmp/nix-shell.vy9tRk/tmp.hXG1ZC8eHP/FStar.Mul.fst.checked
|
|
dummy#L0
(321) * Warning 321:
- Did not expect module FStar.Math.Lemmas to be already checked.
- Found it in an unexpected location:
/nix/store/lk8466gkmpa7m9602xrc34s41q7phfzk-ocaml5.3.0-fstar-7b347386330d0e5a331a220535b6f15288903234/lib/fstar/ulib.checked/FStar.Math.Lemmas.fsti.checked
instead of
/tmp/nix-shell.vy9tRk/tmp.hXG1ZC8eHP/FStar.Math.Lemmas.fsti.checked
|
The logs for this run have expired and are no longer available.
Loading