natural_nat_shift

[xrchz]

In dwarf.lem there are some "missing pervasives" called natural_nat_shift_left and natural_nat_shift_right with no definition but with OCaml bindings. Are these equivalent to multiplication and division by a power of 2? If so, could they be defined that way, at least for the HOL backend?

[PeterSewell]

On 25 May 2018 at 13:03, Ramana Kumar ***@***.***> wrote: In dwarf.lem there are some "missing pervasives" called natural_nat_shift_left and natural_nat_shift_right with no definition but with OCaml bindings. Are these equivalent to multiplication and division by a power of 2?

Looking just at dwarf.lem, I think they're just that but with the mixed natural / nat types - in HOL would just be multiplication and division by 2, y.

…

If so, could they be defined that way, at least for the HOL backend? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#20>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AErM5vi0iCWk9hWoFERU2q3p9prd5YsWks5t1_MKgaJpZM4UN2-U> .