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 963 B image not shown  

Quelle  activation.out   Sprache: unbekannt

 
Untersuchungsergebnis.out Download desUnknown {[0] [0] [0]}zum Wurzelverzeichnis wechseln

File "./output/activation.v", line 5, characters 0-47:
The command has indeed failed with message:
More than one interpretation bound to this notation, confirm with the "all"
modifier.
File "./output/activation.v", line 12, characters 0-22:
The command has indeed failed with message:
No notation provided.
File "./output/activation.v", line 16, characters 0-24:
The command has indeed failed with message:
Found no matching notation to enable or disable.
[no-notation-to-enable-or-disable,syntax,default]
a
     : Type
File "./output/activation.v", line 26, characters 11-12:
The command has indeed failed with message:
The reference a was not found in the current environment.
Prop
     : Type
a
     : Type
a
     : Type
0
     : nat
x
     : bool
0
     : nat
File "./output/activation.v", line 47, characters 0-49:
The command has indeed failed with message:
Found no matching notation to enable or disable.
[no-notation-to-enable-or-disable,syntax,default]

[ zur Elbe Produktseite wechseln0.101Quellennavigators  ]