From 34d5468be95e79adc6cd6158d3431a00341f107a Mon Sep 17 00:00:00 2001 From: Ramana Kumar Date: Fri, 25 May 2018 15:10:37 +0100 Subject: [PATCH] Add hol targets for natural_nat_shifts_ Addresses #20. --- src/dwarf.lem | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/dwarf.lem b/src/dwarf.lem index 4eba23c..9dcc750 100644 --- a/src/dwarf.lem +++ b/src/dwarf.lem @@ -699,9 +699,11 @@ let partialNaturalFromInteger (i:integer) : natural = val natural_nat_shift_left : natural -> nat -> natural declare ocaml target_rep function natural_nat_shift_left = `Nat_big_num.shift_left` +declare hol target_rep function natural_nat_shift_left n m = (naturalPow 2 m) * n val natural_nat_shift_right : natural -> nat -> natural declare ocaml target_rep function natural_nat_shift_right = `Nat_big_num.shift_right` +declare hol target_rep function natural_nat_shift_right n m = n / (naturalPow 2 m)