Irvin
Irvin
Note the main motivation of this pr was stuff like v2w (x:xs) not being simplified
The theorem i was attempting to prove was ``` Definition bits_to_word_def: (bits_to_word [] = 0w) /\ (bits_to_word (T::xs) = (bits_to_word xs
I would agree that having `v2w v = n2w (v2n v)` might be a better situation. A normalized word is actually going to end up being `n2w n` anyway where...
I don't think I have time to figure out the simp rules so leaving it as just theorems added.
Note some more work on enat in HOL4 at examples/computability/kolmog/extNatScript.sml.
For implementation I'm considering 1. Add primrec combinators as a primitive operation. 2. Add a pass which detects primrec functions and rewrites them to use the combinators. 3. Implement a...
I don't think the algorithm would work out of the box and need to be changed.
I should be able to do this in since I'm going to be touching nearby code for https://github.com/CakeML/cakeml/issues/355#issuecomment-2678603638
I think if this is done in a more general way by adding a type unsafe way to modify a mutable block to an immutable block we will be able...
#1143 also will have to be done using a way to turn a mutable array into a vector