(352) * Warning 352 at /__w/steel/steel/steel/lib/steel/Steel.ST.Effect.AtomicAndGhost.fsti(185,16-185,20): - Combinator (Steel.ST.Effect.AtomicAndGhost.STAGCommon , Steel.ST.Effect.AtomicAndGhost.STAGCommon) |> Steel.ST.Effect.AtomicAndGhost.STAGCommon is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(352) * Warning 352 at /__w/steel/steel/steel/lib/steel/Steel.ST.Effect.fsti(169,24-169,36): - Combinator ite_Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(352) * Warning 352 at /__w/steel/steel/steel/lib/steel/Steel.ST.Effect.fsti(168,19-168,26): - Combinator Steel.ST.Effect.STBase <: Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(352) * Warning 352 at /__w/steel/steel/steel/lib/steel/Steel.ST.Effect.fsti(167,16-167,20): - Combinator (Steel.ST.Effect.STBase , Steel.ST.Effect.STBase) |> Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(352) * Warning 352 at /__w/steel/steel/steel/lib/steel/Steel.ST.Effect.fsti(169,24-169,36): - Combinator ite_Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(352) * Warning 352 at /__w/steel/steel/steel/lib/steel/Steel.ST.Effect.fsti(168,19-168,26): - Combinator Steel.ST.Effect.STBase <: Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(352) * Warning 352 at /__w/steel/steel/steel/lib/steel/Steel.ST.Effect.fsti(167,16-167,20): - Combinator (Steel.ST.Effect.STBase , Steel.ST.Effect.STBase) |> Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(340) * Warning 340 at /__w/steel/steel/steel/lib/steel/Steel.Effect.Common.fsti(461,24-461,37): - Unfolding name which is marked as a plugin: frame_vc_norm

(337) * Warning 337 at /__w/steel/steel/steel/lib/steel/Steel.Effect.Common.fsti(2066,65-2066,66): - 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/steel/steel/steel/src/extraction/ExtractSteel.Krml.fst(33,41-33,42): - 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 '@'.

(288) * Warning 288 at FStar.Krml.Endianness.fst(58,34-58,41): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at FStar.Krml.Endianness.fst(58,11-58,18): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at FStar.Krml.Endianness.fst(57,56-57,63): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at FStar.Krml.Endianness.fst(57,4-57,28): - FStar.Krml.Endianness.lemma_euclidean_division is deprecated - FStar.Endianness.lemma_euclidean_division - See also FStar.Krml.Endianness.fst(36,4-36,28)

(288) * Warning 288 at FStar.Krml.Endianness.fst(56,11-56,18): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at FStar.Krml.Endianness.fst(55,11-55,18): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at FStar.Krml.Endianness.fst(47,8-47,32): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at FStar.Krml.Endianness.fst(45,13-45,20): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at FStar.Krml.Endianness.fst(45,13-45,20): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(328) * Warning 328 at Spec.Loops.fst(47,8-47,19): - Global binding 'Spec.Loops.repeat_base' is recursive but not used in its body

(328) * Warning 328 at /__w/steel/steel/FStar/src/parser/FStarC.Parser.ToDocument.fst(1989,4-1989,12): - Global binding 'FStarC.Parser.ToDocument.p_tmNoEq' is recursive but not used in its body

(328) * Warning 328 at /__w/steel/steel/FStar/src/parser/FStarC.Parser.ToDocument.fst(1725,4-1725,21): - Global binding 'FStarC.Parser.ToDocument.p_maybeFocusArrow' is recursive but not used in its body

(328) * Warning 328 at /__w/steel/steel/FStar/src/parser/FStarC.Parser.ToDocument.fst(1093,4-1093,24): - Global binding 'FStarC.Parser.ToDocument.p_disjunctivePattern' is recursive but not used in its body

(328) * Warning 328 at /__w/steel/steel/FStar/src/parser/FStarC.Parser.ToDocument.fst(754,4-754,13): - Global binding 'FStarC.Parser.ToDocument.p_justSig' is recursive but not used in its body

(328) * Warning 328 at /__w/steel/steel/FStar/src/parser/FStarC.Parser.ToDocument.fst(733,8-733,14): - Global binding 'FStarC.Parser.ToDocument.p_decl' is recursive but not used in its body

(337) * Warning 337 at /__w/steel/steel/FStar/src/basic/FStarC.Plugins.fst(88,16-88,17): - 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/steel/steel/FStar/src/basic/FStarC.Plugins.fst(87,16-87,17): - 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/steel/steel/FStar/src/basic/FStarC.Plugins.fst(86,16-86,17): - 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/steel/steel/FStar/src/basic/FStarC.Plugins.fst(85,16-85,17): - 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 '@'.