Normalizer: do not drop internal ascriptions #394
Annotations
8 errors and 10 warnings
|
Diff failed for files /tests/error-messages/_output/Monoid.fst.json_output and /tests/error-messages/Monoid.fst.json_output.expected:
--- _output/Monoid.fst.json_output 2025-02-18 17:16:13.153743721 +0000
+++ Monoid.fst.json_output.expected 2025-02-18 17:13:28.510220362 +0000
@@ -454,12 +454,10 @@
Monoid.intro_monoid Prims.bool false xor
let lift_monoid_option m =
(let mult x y =
- ((match x, y with
- | FStar.Pervasives.Native.Some x0, FStar.Pervasives.Native.Some y0 ->
- FStar.Pervasives.Native.Some (m.mult x0 y0)
- | _, _ -> FStar.Pervasives.Native.None)
- <:
- FStar.Pervasives.Native.option a)
+ (match x, y with
+ | FStar.Pervasives.Native.Some x0, FStar.Pervasives.Native.Some y0 ->
+ FStar.Pervasives.Native.Some (m.mult x0 y0)
+ | _, _ -> FStar.Pervasives.Native.None)
<:
FStar.Pervasives.Native.option a
in
|
|
Diff failed for files /tests/error-messages/_output/Monoid.fst.output and /tests/error-messages/Monoid.fst.output.expected:
--- _output/Monoid.fst.output 2025-02-18 17:16:14.134741261 +0000
+++ Monoid.fst.output.expected 2025-02-18 17:13:28.510220362 +0000
@@ -454,12 +454,10 @@
Monoid.intro_monoid Prims.bool false xor
let lift_monoid_option m =
(let mult x y =
- ((match x, y with
- | FStar.Pervasives.Native.Some x0, FStar.Pervasives.Native.Some y0 ->
- FStar.Pervasives.Native.Some (m.mult x0 y0)
- | _, _ -> FStar.Pervasives.Native.None)
- <:
- FStar.Pervasives.Native.option a)
+ (match x, y with
+ | FStar.Pervasives.Native.Some x0, FStar.Pervasives.Native.Some y0 ->
+ FStar.Pervasives.Native.Some (m.mult x0 y0)
+ | _, _ -> FStar.Pervasives.Native.None)
<:
FStar.Pervasives.Native.option a
in
|
|
Diff failed for files /tests/error-messages/_output/PatImps.fst.json_output and /tests/error-messages/PatImps.fst.json_output.expected:
--- _output/PatImps.fst.json_output 2025-02-18 17:16:24.334716498 +0000
+++ PatImps.fst.json_output.expected 2025-02-18 17:13:28.512220356 +0000
@@ -76,13 +76,9 @@
module PatImps
Declarations: [
let f1 x =
- (((match x with
- | [] -> 0
- | _ :: _ -> 1)
- <:
- Prims.int)
- <:
- Prims.int)
+ (match x with
+ | [] -> 0
+ | _ :: _ -> 1)
<:
Prims.int
noeq
@@ -92,12 +88,8 @@
let f2 x =
- (((let PatImps.A #i = x in
- i)
- <:
- Prims.int)
- <:
- Prims.int)
+ (let PatImps.A #i = x in
+ i)
<:
Prims.int
noeq
@@ -113,13 +105,9 @@
let f3 x =
- (((match x with
- | PatImps.B #i -> i
- | PatImps.C #i -> i)
- <:
- Prims.int)
- <:
- Prims.int)
+ (match x with
+ | PatImps.B #i -> i
+ | PatImps.C #i -> i)
<:
Prims.int
]
|
|
Diff failed for files /tests/error-messages/_output/PatImps.fst.output and /tests/error-messages/PatImps.fst.output.expected:
--- _output/PatImps.fst.output 2025-02-18 17:16:24.608715842 +0000
+++ PatImps.fst.output.expected 2025-02-18 17:13:28.512220356 +0000
@@ -76,13 +76,9 @@
module PatImps
Declarations: [
let f1 x =
- (((match x with
- | [] -> 0
- | _ :: _ -> 1)
- <:
- Prims.int)
- <:
- Prims.int)
+ (match x with
+ | [] -> 0
+ | _ :: _ -> 1)
<:
Prims.int
noeq
@@ -92,12 +88,8 @@
let f2 x =
- (((let PatImps.A #i = x in
- i)
- <:
- Prims.int)
- <:
- Prims.int)
+ (let PatImps.A #i = x in
+ i)
<:
Prims.int
noeq
@@ -113,13 +105,9 @@
let f3 x =
- (((match x with
- | PatImps.B #i -> i
- | PatImps.C #i -> i)
- <:
- Prims.int)
- <:
- Prims.int)
+ (match x with
+ | PatImps.B #i -> i
+ | PatImps.C #i -> i)
<:
Prims.int
]
|
|
Diff failed for files /tests/error-messages/_output/TuplePat.fst.json_output and /tests/error-messages/TuplePat.fst.json_output.expected:
--- _output/TuplePat.fst.json_output 2025-02-18 17:16:40.075674431 +0000
+++ TuplePat.fst.json_output.expected 2025-02-18 17:13:28.514220351 +0000
@@ -32,21 +32,17 @@
module TuplePat
Declarations: [
let mult x y =
- ((match x, y with
- | 0, 0 -> 0
- | x, y -> x * y)
- <:
- Prims.int)
+ (match x, y with
+ | 0, 0 -> 0
+ | x, y -> x * y)
<:
Prims.int
let mult2 x y =
- ((match x, y with
- | FStar.Pervasives.Native.Some x, FStar.Pervasives.Native.Some y -> x * y
- | FStar.Pervasives.Native.None , _ -> 0
- | _, FStar.Pervasives.Native.None -> 0
- | _ -> 123)
- <:
- Prims.int)
+ (match x, y with
+ | FStar.Pervasives.Native.Some x, FStar.Pervasives.Native.Some y -> x * y
+ | FStar.Pervasives.Native.None , _ -> 0
+ | _, FStar.Pervasives.Native.None -> 0
+ | _ -> 123)
<:
Prims.int
]
|
|
Diff failed for files /tests/error-messages/_output/TuplePat.fst.output and /tests/error-messages/TuplePat.fst.output.expected:
--- _output/TuplePat.fst.output 2025-02-18 17:16:40.298673817 +0000
+++ TuplePat.fst.output.expected 2025-02-18 17:13:28.514220351 +0000
@@ -32,21 +32,17 @@
module TuplePat
Declarations: [
let mult x y =
- ((match x, y with
- | 0, 0 -> 0
- | x, y -> x * y)
- <:
- Prims.int)
+ (match x, y with
+ | 0, 0 -> 0
+ | x, y -> x * y)
<:
Prims.int
let mult2 x y =
- ((match x, y with
- | FStar.Pervasives.Native.Some x, FStar.Pervasives.Native.Some y -> x * y
- | FStar.Pervasives.Native.None , _ -> 0
- | _, FStar.Pervasives.Native.None -> 0
- | _ -> 123)
- <:
- Prims.int)
+ (match x, y with
+ | FStar.Pervasives.Native.Some x, FStar.Pervasives.Native.Some y -> x * y
+ | FStar.Pervasives.Native.None , _ -> 0
+ | _, FStar.Pervasives.Native.None -> 0
+ | _ -> 123)
<:
Prims.int
]
|
|
Diff failed for files /tests/ide/emacs/_output/Fib.compute.ideout and /tests/ide/emacs/Fib.compute.ideout.expected:
--- _output/Fib.compute.ideout 2025-02-18 17:24:08.009937060 +0000
+++ Fib.compute.ideout.expected 2025-02-18 17:13:28.519220338 +0000
@@ -1,3 +1,3 @@
{"kind": "protocol-info", "rest": "[...]"}
{"kind": "response", "query-id": "1", "response": [], "status": "success"}
-{"kind": "response", "query-id": "2", "response": "(8 <: int) <: int", "status": "success"}
+{"kind": "response", "query-id": "2", "response": "8 <: int", "status": "success"}
|
|
|
|
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
|
|
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.
|
|
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.
|
|
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.
|
|
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.
|
|
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.
|
|
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.
|
|
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.
|
|
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.
|
|
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.
|
The logs for this run have expired and are no longer available.
Loading