Stream: Coq users

Topic: ✔ Simple notation for `Vector.t bool`

view this post on Zulip Julin S (Dec 26 2021 at 06:12):

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?

view this post on Zulip Julin S (Dec 26 2021 at 17:07):

Oh sorry, the first zero in the notation was the reason for the error. Making 'O' (capital o) made it okay.

view this post on Zulip Notification Bot (Dec 26 2021 at 17:07):

Ju-sh has marked this topic as resolved.

Last updated: Apr 16 2024 at 16:01 UTC