Tactics: introduce postprocess_type #266
Annotations
10 errors and 10 warnings
|
Run tests, without forcing a build:
X64.Vale.Decls.fst#L250
(19) * Error 19 at X64.Vale.Decls.fst(250,2-259,16):
- Assertion failed
|
|
Run tests, without forcing a build:
X64.Vale.Decls.fst#L241
(19) * Error 19 at X64.Vale.Decls.fst(250,2-259,16):
- Could not prove post-condition
- See also X64.Vale.Decls.fst(241,18-242,46)
|
|
Run tests, without forcing a build:
X64.Vale.Decls.fst#L239
(19) * Error 19 at X64.Vale.Decls.fst(250,2-259,16):
- Could not prove post-condition
- See also X64.Vale.Decls.fst(239,82-241,14)
|
|
Run tests, without forcing a build:
X64.Vale.Decls.fst#L238
(19) * Error 19 at X64.Vale.Decls.fst(250,2-259,16):
- Could not prove post-condition
- See also X64.Vale.Decls.fst(238,28-239,78)
|
|
Run tests, without forcing a build:
X64.Vale.Decls.fst#L238
(19) * Error 19 at X64.Vale.Decls.fst(250,2-259,16):
- Could not prove post-condition
- See also X64.Vale.Decls.fst(238,7-238,24)
|
|
Run tests, without forcing a build:
X64.Vale.Decls.fst#L237
(19) * Error 19 at X64.Vale.Decls.fst(250,2-259,16):
- Could not prove post-condition
- See also X64.Vale.Decls.fst(237,7-237,48)
|
|
Run tests, without forcing a build:
X64.Vale.Decls.fst#L250
(19) * Error 19 at X64.Vale.Decls.fst(250,2-259,16):
- Could not prove post-condition
|
|
Run tests, without forcing a build:
X64.Vale.Decls.fsti#L216
(19) * Error 19 at X64.Vale.Decls.fst(252,41-252,55):
- Assertion failed
- See also X64.Vale.Decls.fsti(216,25-216,54)
|
|
Run tests, without forcing a build:
X64.Vale.Decls.fsti#L216
(19) * Error 19 at X64.Vale.Decls.fst(252,41-252,55):
- Assertion failed
- See also X64.Vale.Decls.fsti(216,13-216,21)
|
|
Run tests, without forcing a build:
X64.Vale.Decls.fst#L108
(19) * Error 19 at X64.Vale.Decls.fst(253,2-253,20):
- Assertion failed
- See also X64.Vale.Decls.fst(108,4-108,27)
|
|
Run tests, without forcing a build:
Hello.fst#L5
(272) * Warning 272 at Hello.fst(5,0-5,34):
- Top-level let-bindings must be total; this term may have effects
|
|
Run tests, without forcing a build:
Part2.Free.fst#L132
(350) * Warning 350 at Part2.Free.fst(132,4-134,12):
- The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.
|
|
Run tests, without forcing a build:
Part2.Free.fst#L133
(350) * Warning 350 at Part2.Free.fst(133,4-134,12):
- The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.
|
|
Run tests, without forcing a build:
Part2.FreeFunExt.fst#L136
(350) * Warning 350 at Part2.FreeFunExt.fst(136,4-138,12):
- The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.
|
|
Run tests, without forcing a build:
Part2.FreeFunExt.fst#L137
(350) * Warning 350 at Part2.FreeFunExt.fst(137,4-138,12):
- The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.
|
|
Run tests, without forcing a build:
Part2.Par.fst#L40
(350) * Warning 350 at Part2.Par.fst(40,18-40,40):
- The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.
|
|
Run tests, without forcing a build:
Part2.Par.fst#L48
(350) * Warning 350 at Part2.Par.fst(48,18-48,40):
- The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.
|
|
Run tests, without forcing a build:
Part2.Par.fst#L105
(350) * Warning 350 at Part2.Par.fst(105,4-106,17):
- The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.
|
|
Run tests, without forcing a build:
Part2.ST.fst#L26
(350) * Warning 350 at Part2.ST.fst(26,2-28,10):
- The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.
|
|
Run tests, without forcing a build:
Part2.ST.fst#L27
(350) * Warning 350 at Part2.ST.fst(27,2-28,10):
- The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.
|
Loading