diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_values.v | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index ab557ff4..335ebf26 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -73,7 +73,13 @@ Definition nn := nat. (*val pow : Z -> Z -> Z*) Definition pow m n := m ^ n. -Definition pow2 n := pow 2 n. +Program Definition pow2 n : {z : Z & ArithFact (2 ^ n <= z <= 2 ^ n)} := existT _ (pow 2 n) _. +Next Obligation. +constructor. +unfold pow. +auto using Z.le_refl. +Qed. + (* Definition inline lt := (<) Definition inline gt := (>) |