Definite error:
For every expanded signature Sigma, the instance of Fixed_Size_BitVectors ...
Should be:
For every expanded signature Sigma, the instance of FixedSizeBitVectors ...
I am confused by:
The semantic interpretation [[_]] of well-sorted BitVec-terms is
inductively defined as follows.
Variables
If v is a variable of sort (_ BitVec m) with 0 < m, then
[[v]] is some element of [[0, m-1) → {0, 1}], the set of total
functions from [0, m) to {0, 1}.
specifically:
[[0, m-1) → {0, 1}], the set of total functions from [0, m) to {0, 1}.
I am a confused why it is written [[0, m-1) → {0, 1}] and not {[0, m-1) → {0, 1}}
Is there some special meaning to the outer [ ]?
I am also confused by [0, m-1) which I think should be either [0, m) or [0, m-1]
From Caleb Donovick, Apr 22, 2023:
Definite error: For every expanded signature Sigma, the instance of Fixed_Size_BitVectors ... Should be: For every expanded signature Sigma, the instance of FixedSizeBitVectors ...
I am confused by: The semantic interpretation [[_]] of well-sorted BitVec-terms is inductively defined as follows.
Variables
If v is a variable of sort (_ BitVec m) with 0 < m, then [[v]] is some element of [[0, m-1) → {0, 1}], the set of total functions from [0, m) to {0, 1}.
specifically: [[0, m-1) → {0, 1}], the set of total functions from [0, m) to {0, 1}.
I am a confused why it is written [[0, m-1) → {0, 1}] and not {[0, m-1) → {0, 1}} Is there some special meaning to the outer [ ]? I am also confused by [0, m-1) which I think should be either [0, m) or [0, m-1]
Caleb