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]
[ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
]
