Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/output/   (Beweissystem des Inria Version 9.1.0©)  Datei vom 15.8.2025 mit Größe 835 B image not shown  

Quelle  Qf_stdlib.out   Sprache: unbekannt

 
File "./output/Qf_stdlib.v", line 16, characters 6-22:
Warning: Coq.Init.Nat.add has been replaced by Corelib.Init.Nat.add.
[deprecated-dirpath-Coq,deprecated-since-9.0,deprecated,default]
Quickfix:
Replace File "./output/Qf_stdlib.v", line 16, characters 6-22 with Corelib.Init.Nat.add
Nat.add : nat -> nat -> nat

Nat.add is not universe polymorphic
Arguments Nat.add (n m)%_nat_scope
Nat.add is transparent
Expands to: Constant Corelib.Init.Nat.add
Declared in library Corelib.Init.Nat, line 47, characters 9-12
File "./output/Qf_stdlib.v", line 17, characters 6-22:
Warning: Coq.Init.Nat.add has been replaced by Corelib.Init.Nat.add.
[deprecated-dirpath-Coq,deprecated-since-9.0,deprecated,default]
Quickfix:
Replace File "./output/Qf_stdlib.v", line 17, characters 6-22 with Corelib.Init.Nat.add
Nat.add
     : nat -> nat -> nat

[ Dauer der Verarbeitung: 0.13 Sekunden  (vorverarbeitet)  ]