Coallesce duplicate lemmas about pow2, move into Math.Lemmas, add 128… #3910
Annotations
10 errors and 10 warnings
|
FStar.UInt128.fst#L956
(19) * Error 19 at /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(956,15-981,3):
- Subtyping check failed
- Expected type b: Prims.nat{b < Prims.pow2 32}
got type FStar.UInt.uint_t FStar.UInt32.n
- Also see: /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(963,31-963,40)
- Other related locations: /__w/FStar/FStar/FStar/ulib/Prims.fst(682,18-682,24)
|
|
FStar.UInt128.fst#L956
(19) * Error 19 at /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(956,15-981,3):
- Subtyping check failed
- Expected type b: Prims.nat{b < Prims.pow2 32}
got type FStar.UInt.uint_t FStar.UInt32.n
- Also see: /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(963,31-963,40)
- Other related locations: /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(951,52-951,63)
|
|
FStar.UInt128.fst#L956
(19) * Error 19 at /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(956,15-981,3):
- Assertion failed
- Also see: /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(965,17-965,20)
- Other related locations: /__w/FStar/FStar/FStar/ulib/FStar.UInt64.fsti(147,12-147,32)
|
|
FStar.UInt128.fst#L956
(19) * Error 19 at /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(956,15-981,3):
- Assertion failed
- Also see: /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(966,16-966,19)
- Other related locations: /__w/FStar/FStar/FStar/ulib/FStar.UInt64.fsti(91,12-91,32)
|
|
FStar.UInt128.fst#L956
(19) * Error 19 at /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(956,15-981,3):
- Assertion failed
- Also see: /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(971,18-971,29)
- Other related locations: /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(934,12-934,32)
|
|
FStar.UInt128.fst#L956
(19) * Error 19 at /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(956,15-981,3):
- Assertion failed
- Also see: /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(972,23-972,34)
- Other related locations: /__w/FStar/FStar/FStar/ulib/FStar.UInt64.fsti(211,12-211,28)
|
|
FStar.UInt128.fst#L956
(19) * Error 19 at /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(956,15-981,3):
- Assertion failed
- Also see: /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(975,2-975,8)
- Other related locations: /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(975,9-975,42)
|
|
FStar.UInt128.fst#L956
(19) * Error 19 at /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(956,15-981,3):
- Subtyping check failed
- Expected type Prims.nonzero got type Prims.pos
- Also see: /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(978,34-978,41)
- Other related locations: /__w/FStar/FStar/FStar/ulib/Prims.fst(688,22-688,28)
|
|
FStar.UInt128.fst#L956
(19) * Error 19 at /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(956,15-981,3):
- Assertion failed
- Also see: /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(978,2-978,8)
- Other related locations: /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(978,9-978,52)
|
|
FStar.UInt128.fst#L956
(19) * Error 19 at /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(956,15-981,3):
- Assertion failed
- Also see: /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(980,2-980,8)
- Other related locations: /__w/FStar/FStar/FStar/ulib/FStar.UInt128.fst(980,9-980,64)
|
|
FStarC.Parser.ToDocument.fst#L1734
(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(1734,4-1734,21):
- Global binding
'FStarC.Parser.ToDocument.p_maybeFocusArrow'
is recursive but not used in its body
|
|
FStarC.Parser.ToDocument.fst#L1093
(328) * Warning 328 at /__w/FStar/FStar/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
|
|
FStarC.Parser.ToDocument.fst#L754
(328) * Warning 328 at /__w/FStar/FStar/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
|
|
FStarC.Parser.ToDocument.fst#L733
(328) * Warning 328 at /__w/FStar/FStar/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
|
|
FStarC.Parser.AST.fst#L778
(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.AST.fst(778,8-778,22):
- Global binding
'FStarC.Parser.AST.decl_to_string'
is recursive but not used in its body
|
|
FStarC.Plugins.fst#L88
(337) * Warning 337 at /__w/FStar/FStar/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 '@'.
|
|
FStarC.Plugins.fst#L87
(337) * Warning 337 at /__w/FStar/FStar/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 '@'.
|
|
FStarC.Plugins.fst#L86
(337) * Warning 337 at /__w/FStar/FStar/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 '@'.
|
|
FStarC.Plugins.fst#L85
(337) * Warning 337 at /__w/FStar/FStar/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 '@'.
|
|
FStar.UInt.fsti#L435
(271) * Warning 271 at /__w/FStar/FStar/FStar/stage0/out/lib/fstar/ulib/FStar.UInt.fsti(435,8-435,51):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
The logs for this run have expired and are no longer available.
Loading