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

Previous Next

Full log

View this message in rfc822 format

From: Stefan Monnier <monnier <at> iro.umontreal.ca>
To: MON KEY <monkey <at> sandpframing.com>
Cc: 6878 <at> debbugs.gnu.org
Subject: bug#6878: bool-vectors of length 0 signal error when aref/aset the 0th element
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

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.