Also adjust the level of $n, see the discussion in #5.
We also move all of the level specifications to ReservedNotations.v.
This allows early detection of notation conflicts, as any file importing
bbv.ReservedNotations will observe all notation conflicts that can arise
from importing any file of bbv.
samuelgruetter
commented
6 years ago
Also adjust the level of $n, see the discussion in #5.
We also move all of the level specifications to ReservedNotations.v. This allows early detection of notation conflicts, as any file importing bbv.ReservedNotations will observe all notation conflicts that can arise from importing any file of bbv.
Closes #5