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]