Re: [isabelle] missing function in Word library?
Sascha Boehme wrote:
while studying the current (most recent) Word library, I didn't find a
function which extracts a part from a word. I started to implement a
function on my own, but I'm sure there must be a better version
(especially wrt. to doing proofs on it).
Here is my solution:
definition word_extract :: "'a::len0 word => int => int => 'b::len word"
where "word_extract w from to = (of_bl o rev o drop (nat from) o take
(nat to) o rev o to_bl) w"
If that is your current definition, John's version is probably what you want
(reasoning about mask and shift is easier than type conversions).
There is also the built-in "slice :: nat => 'a word => 'b word". The nat
says from where to slice, the target type length says how much to slice.
This archive was generated by a fusion of
Pipermail (Mailman edition) and