bug#6878: bool-vectors of length 0 signal error when aref/aset the 0th element

[Stefan Monnier <monnier@iro.umontreal.ca>]

>>> ,---- (info "(elisp)Bool-Vector Type")
>>> | "A "bool-vector" is a one-dimensional array of elements that must be `t'
>>> | or `nil'."
>> All elements of (make-bool-vector 0 t) are either t or nil.

> Prove it!

Easy! formally, he said:

  ∀ n ≥ 0 ∧ n < 0. (aref (make-bool-vector 0 t) n) ∈ { nil, t }

And since there is no such `n', this is trivially true.
More specifically, "n ≥ 0 ∧ n < 0" is a falsehood, and from false you
can conclude anything you wish.  Among other things you can just
a trivially prove:

  ∀ n ≥ 0 ∧ n < 0. the sky is green


-- Stefan