equal
deleted
inserted
replaced
8 imports Code_Abstract_Nat |
8 imports Code_Abstract_Nat |
9 begin |
9 begin |
10 |
10 |
11 text \<open> |
11 text \<open> |
12 When generating code for functions on natural numbers, the |
12 When generating code for functions on natural numbers, the |
13 canonical representation using @{term "0::nat"} and |
13 canonical representation using \<^term>\<open>0::nat\<close> and |
14 @{term Suc} is unsuitable for computations involving large |
14 \<^term>\<open>Suc\<close> is unsuitable for computations involving large |
15 numbers. This theory refines the representation of |
15 numbers. This theory refines the representation of |
16 natural numbers for code generation to use binary |
16 natural numbers for code generation to use binary |
17 numerals, which do not grow linear in size but logarithmic. |
17 numerals, which do not grow linear in size but logarithmic. |
18 \<close> |
18 \<close> |
19 |
19 |