Disable cross-effect subtyping of arrows #155
Annotations
10 errors and 11 warnings
|
Run tests, without forcing a build:
Pure.fst#L91
(189) * Error 189 at Pure.fst(91,13-93,55):
- Expected expression of type post Prims.int
got expression _
of type Prims.pure_post Prims.int
|
|
Run tests, without forcing a build:
dummy#L1
(189) * Error 189 at Ex04e.fst(23,0-25,49):
- Expected expression of type f: (_: (*?u72*) _ -> Prims.bool) -> Type
got expression fun _ -> (*?u72*) _
of type f: (_: (*?u72*) _ -> Prims.bool) -> Prims.GTot Type
|
|
Run tests, without forcing a build:
Bug1536.fst#L18
(12) * Error 12 at Bug1536.fst(18,18-18,42):
- Expected type Prims.pure_wp (FStar.Pervasives.either a Prims.exn)
but f__w _
has type _: (_: FStar.Pervasives.either a Prims.exn -> Type0) -> Type0
|
|
Run tests, without forcing a build:
Bug709.fst#L18
(12) * Error 12 at Bug709.fst(18,34-29,27):
- Expected type Prims.pure_wp (a & s)
but f__w _
has type _: (_: a & s -> Type0) -> Type0
- See also Bug709.fst(18,34-27,10)
|
|
Run tests, without forcing a build:
dummy#L1
(189) * Error 189 at Bug1449.fst(20,0-23,29):
- Expected expression of type a: Prims.string -> Type
got expression fun _ -> Prims.string
of type a: Prims.string -> Prims.GTot Prims.eqtype
|
|
Run tests, without forcing a build:
Vec.fst#L150
(66) * Error 66 at Vec.fst(150,83-150,107):
- Failed to resolve implicit argument ?15
of type Type0
introduced for
flex-flex quasi: lhs=Instantiating implicit argument rhs=Instantiating
implicit argument
|
|
Run tests, without forcing a build:
Bug713.fst#L18
(12) * Error 12 at Bug713.fst(18,8-24,20):
- Expected type Prims.pure_wp Prims.int
but _ _
has type _: (_: Prims.int -> Type0) -> Type0
- See also Bug713.fst(18,8-23,11)
|
|
Run tests, without forcing a build:
dummy#L1
(189) * Error 189 at Part1.Lemmas.fst(188,0-191,55):
- Expected expression of type f: (_: (*?u72*) _ -> Prims.bool) -> Type
got expression fun _ -> (*?u72*) _
of type f: (_: (*?u72*) _ -> Prims.bool) -> Prims.GTot Type
|
|
Run tests, without forcing a build:
Bug2169b.fst#L9
(54) * Error 54 at Bug2169b.fst(10,24-10,25):
- _: a -> Type0 is not a subtype of the expected type _: a{Prims.l_True} -> Prims.GTot Type0
- See also Bug2169b.fst(9,46-9,47)
|
|
Run tests, without forcing a build:
Bug1066.fst#L9
(12) * Error 12 at Bug1066.fst(9,56-9,69):
- Expected type Type but b _ has type Type
|
|
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
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