rems-project / linksem

Semantic model for aspects of ELF static linking and DWARF debug information
Other
43 stars 7 forks source link

Add hol targets for natural_nat_shifts_ #22

Open xrchz opened 6 years ago

xrchz commented 6 years ago

Addresses #20.

I am not sure whether this is the best approach: maybe a library function would be better instead of inline division and multiplication? As far as I know, there is no function already defined in HOL for natural numbers.