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

From: Stefan Monnier <[email-masked]>
Date: Thu, 19 Aug 2010 17:51:51 +0200

>>> ,---- (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