I was trying to make a notation for Vector.t bool
so that I can use 0b1
instead of [true]%vector
and 0b0
instead of [false]%vector
.
So I did
Require Import Vector.
Import VectorNotations.
Notation "'0b0'" := [false]%vector : vector.
but upon doing
Check 0b0.
It gave error saying
The reference b0 was not found in the current environment.
How can this be fixed?
Oh sorry, the first zero in the notation was the reason for the error. Making 'O' (capital o) made it okay.
Ju-sh has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC