Some error nits #169
Annotations
11 warnings
|
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
Produce all artifacts:
FStar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /__w/FStar/FStar/FStar/ulib/FStar.UInt.fsti:435.9-435.52:
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
|
Produce all artifacts:
FStar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /__w/FStar/FStar/FStar/ulib/FStar.UInt.fst:293.9-293.26:
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
- See also /__w/FStar/FStar/FStar/ulib/FStar.UInt.fsti:435.9-435.52
|
|
Produce all artifacts:
FStar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /__w/FStar/FStar/FStar/ulib/FStar.UInt.fsti:435.9-435.52:
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
|
Produce all artifacts:
FStar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti#L446
(288) * Warning 288 at /__w/FStar/FStar/FStar/ulib/FStar.Reflection.V2.Arith.fst:116.21-116.32:
- FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated
- Use Reflection.term_eq instead
- See also /__w/FStar/FStar/FStar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti:446.1-446.43
|
|
Produce all artifacts:
FStar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /__w/FStar/FStar/FStar/ulib/FStar.UInt.fsti:435.9-435.52:
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
|
Produce all artifacts:
FStar/src/data/FStarC.RBSet.fst#L105
(337) * Warning 337 at /__w/FStar/FStar/FStar/src/data/FStarC.RBSet.fst:105.31-105.32:
- 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 '@'.
|
|
Produce all artifacts:
FStar/src/data/FStarC.RBSet.fst#L105
(337) * Warning 337 at /__w/FStar/FStar/FStar/src/data/FStarC.RBSet.fst:105.37-105.38:
- 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 '@'.
|
|
Produce all artifacts:
FStar/src/basic/FStarC.Plugins.fst#L86
(337) * Warning 337 at /__w/FStar/FStar/FStar/src/basic/FStarC.Plugins.fst:86.17-86.18:
- 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 '@'.
|
|
Produce all artifacts:
FStar/src/basic/FStarC.Plugins.fst#L87
(337) * Warning 337 at /__w/FStar/FStar/FStar/src/basic/FStarC.Plugins.fst:87.17-87.18:
- 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 '@'.
|
|
Produce all artifacts:
FStar/src/basic/FStarC.Plugins.fst#L88
(337) * Warning 337 at /__w/FStar/FStar/FStar/src/basic/FStarC.Plugins.fst:88.17-88.18:
- 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 '@'.
|
Loading