ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

(328) * Warning 328 at src/syntax_extension/PulseSyntaxExtension.Sugar.fst(366,8-366,15): - Global binding 'PulseSyntaxExtension.Sugar.eq_decl' is recursive but not used in its body

(328) * Warning 328 at src/syntax_extension/PulseSyntaxExtension.Sugar.fst(512,8-512,17): - Global binding 'PulseSyntaxExtension.Sugar.scan_decl' is recursive but not used in its body

(337) * Warning 337 at src/syntax_extension/PulseSyntaxExtension.Sugar.fst(621,47-621,48): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at src/syntax_extension/PulseSyntaxExtension.Sugar.fst(622,47-622,48): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at src/checker/Pulse.Common.fst(84,11-84,12): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(328) * Warning 328 at src/syntax_extension/PulseSyntaxExtension.Desugar.fst(781,4-781,16): - Global binding 'PulseSyntaxExtension.Desugar.desugar_decl' is recursive but not used in its body

(290) * Warning 290 at /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fsti(373,16-373,18): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of t1 (bound in /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fsti(373,16-373,18)) and b1 (bound in src/checker/Pulse.Syntax.Base.fst(295,15-295,17)) are equal. - The type of the first term is: Pulse.Syntax.Base.st_term - The type of the second term is: Pulse.Syntax.Base.pattern & Pulse.Syntax.Base.st_term - If the proof fails, try annotating these with the same type.

(290) * Warning 290 at /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fsti(373,16-373,18): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of t1 (bound in /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fsti(373,16-373,18)) and q1 (bound in src/checker/Pulse.Syntax.Base.fst(301,14-301,16)) are equal. - The type of the first term is: Pulse.Syntax.Base.st_term - The type of the second term is: Pulse.Syntax.Base.qualifier - If the proof fails, try annotating these with the same type.

(290) * Warning 290 at src/checker/Pulse.Syntax.Base.fst(125,20-125,22): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of p1 (bound in src/checker/Pulse.Syntax.Base.fst(125,20-125,22)) and pb1 (bound in src/checker/Pulse.Syntax.Base.fst(141,16-141,19)) are equal. - The type of the first term is: Pulse.Syntax.Base.pattern - The type of the second term is: Pulse.Syntax.Base.pattern & Prims.bool - If the proof fails, try annotating these with the same type.