[isabelle] missing function in Word library?
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"
I'm grateful for any hints how to improve this.
This archive was generated by a fusion of
Pipermail (Mailman edition) and