Erase functions to fun #164
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.Pervasives.fst#L38
(318) * Warning 318 at /__w/FStar/FStar/FStar/ulib/FStar.Pervasives.fst(38,4-38,11):
- Values of type `ambient` will be erased during extraction, but its interface
hides this fact.
- Add the `erasable` attribute to the `val ambient` declaration for this
symbol in the interface
|
|
Produce all artifacts:
FStar/ulib/FStar.Pervasives.fst#L138
(318) * Warning 318 at /__w/FStar/FStar/FStar/ulib/FStar.Pervasives.fst(138,4-138,13):
- Values of type `inversion` will be erased during extraction, but its
interface hides this fact.
- Add the `erasable` attribute to the `val inversion` declaration for this
symbol in the interface
|
|
Produce all artifacts:
FStar/ulib/FStar.Set.fst#L25
(318) * Warning 318 at /__w/FStar/FStar/FStar/ulib/FStar.Set.fst(25,4-25,9):
- Values of type `equal` will be erased during extraction, but its interface
hides this fact.
- Add the `erasable` attribute to the `val equal` declaration for this symbol
in the interface
|
|
Produce all artifacts:
FStar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /__w/FStar/FStar/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
|
|
Produce all artifacts:
FStar/ulib/FStar.Seq.Properties.fst#L436
(318) * Warning 318 at /__w/FStar/FStar/FStar/ulib/FStar.Seq.Properties.fst(436,4-436,12):
- Values of type `contains` will be erased during extraction, but its
interface hides this fact.
- Add the `erasable` attribute to the `val contains` declaration for this
symbol in the interface
|
|
Produce all artifacts:
FStar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /__w/FStar/FStar/FStar/ulib/FStar.UInt.fst(293,8-293,25):
- 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,8-435,51)
|
|
Produce all artifacts:
FStar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /__w/FStar/FStar/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
|
|
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,20-116,31):
- 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,0-446,42)
|
|
Produce all artifacts:
FStar/ulib/FStar.Pervasives.fst#L38
(318) * Warning 318 at /__w/FStar/FStar/FStar/ulib/FStar.Pervasives.fst(38,4-38,11):
- Values of type `ambient` will be erased during extraction, but its interface
hides this fact.
- Add the `erasable` attribute to the `val ambient` declaration for this
symbol in the interface
|
|
Produce all artifacts:
FStar/ulib/FStar.Pervasives.fst#L138
(318) * Warning 318 at /__w/FStar/FStar/FStar/ulib/FStar.Pervasives.fst(138,4-138,13):
- Values of type `inversion` will be erased during extraction, but its
interface hides this fact.
- Add the `erasable` attribute to the `val inversion` declaration for this
symbol in the interface
|
Loading