diff options
Diffstat (limited to 'backends/hol4/primitivesTheory.sig')
| -rw-r--r-- | backends/hol4/primitivesTheory.sig | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig index 583f66bd..bac7fd4f 100644 --- a/backends/hol4/primitivesTheory.sig +++ b/backends/hol4/primitivesTheory.sig @@ -249,11 +249,11 @@ sig [isize_bounds] Axiom [oracles: ] [axioms: isize_bounds] [] - ⊢ isize_min ≤ i16_min ∧ isize_max ≥ i16_max + ⊢ isize_min ≤ i16_min ∧ i16_max ≤ isize_max [usize_bounds] Axiom - [oracles: ] [axioms: usize_bounds] [] ⊢ usize_max ≥ u16_max + [oracles: ] [axioms: usize_bounds] [] ⊢ u16_max ≤ usize_max [isize_to_int_bounds] Axiom |