equal
deleted
inserted
replaced
57 "array_sum = |
57 "array_sum = |
58 WHILE Less (!(N 0)) (Plus (!(N 1)) (N 1)) |
58 WHILE Less (!(N 0)) (Plus (!(N 1)) (N 1)) |
59 DO ( N 2 ::= Plus (!(N 2)) (!(!(N 0))); |
59 DO ( N 2 ::= Plus (!(N 2)) (!(!(N 0))); |
60 N 0 ::= Plus (!(N 0)) (N 1) )" |
60 N 0 ::= Plus (!(N 0)) (N 1) )" |
61 |
61 |
62 text \<open>To show the first n variables in a @{typ "nat \<Rightarrow> nat"} state:\<close> |
62 text \<open>To show the first n variables in a \<^typ>\<open>nat \<Rightarrow> nat\<close> state:\<close> |
63 definition |
63 definition |
64 "list t n = map t [0 ..< n]" |
64 "list t n = map t [0 ..< n]" |
65 |
65 |
66 values "{list t n |t n. (array_sum, nth[3,4,0,3,7],5) \<Rightarrow> (t,n)}" |
66 values "{list t n |t n. (array_sum, nth[3,4,0,3,7],5) \<Rightarrow> (t,n)}" |
67 |
67 |