equal
deleted
inserted
replaced
18 We want the bitwise operations to bind slightly weaker |
18 We want the bitwise operations to bind slightly weaker |
19 than \<open>+\<close> and \<open>-\<close>, but \<open>~~\<close> to |
19 than \<open>+\<close> and \<open>-\<close>, but \<open>~~\<close> to |
20 bind slightly stronger than \<open>*\<close>. |
20 bind slightly stronger than \<open>*\<close>. |
21 \<close> |
21 \<close> |
22 |
22 |
23 text \<open>Testing and shifting operations.\<close> |
|
24 |
|
25 class bits = bit + |
23 class bits = bit + |
26 fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool" (infixl "!!" 100) |
24 fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool" (infixl "!!" 100) |
27 and lsb :: "'a \<Rightarrow> bool" |
25 and lsb :: "'a \<Rightarrow> bool" |
28 and msb :: "'a \<Rightarrow> bool" |
26 and msb :: "'a \<Rightarrow> bool" |
29 and set_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a" |
27 and set_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a" |