(290) * Warning 290 at /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst:284.16-284.18: - In the decreases clause for this function, the SMT solver may not be able to prove that the types of b1 (bound in Pulse.Syntax.Base.fst:284.16-284.18) and t1 (bound in Pulse.Syntax.Base.fst:173.21-173.23) are equal. - The type of the first term is: Pulse.Syntax.Base.branch - The type of the second term is: 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.fst:289.15-289.17: - In the decreases clause for this function, the SMT solver may not be able to prove that the types of q1 (bound in Pulse.Syntax.Base.fst:289.15-289.17) and t1 (bound in Pulse.Syntax.Base.fst:173.21-173.23) are equal. - The type of the first term is: Pulse.Syntax.Base.qualifier - The type of the second term is: 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.fst:123.21-123.23: - In the decreases clause for this function, the SMT solver may not be able to prove that the types of p1 (bound in Pulse.Syntax.Base.fst:123.21-123.23) and pb1 (bound in Pulse.Syntax.Base.fst:139.17-139.20) 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.

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

(328) * Warning 328 at /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Desugar.fst:882.5-882.17: - Global binding 'PulseSyntaxExtension.Desugar.desugar_decl' is recursive but not used in its body

(337) * Warning 337 at /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst:601.48-601.49: - 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 /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst:600.48-600.49: - 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 /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst:497.9-497.18: - Global binding 'PulseSyntaxExtension.Sugar.scan_decl' is recursive but not used in its body

(328) * Warning 328 at /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst:359.9-359.16: - Global binding 'PulseSyntaxExtension.Sugar.eq_decl' is recursive but not used in its body