equal
deleted
inserted
replaced
56 "constn 0 = z" | |
56 "constn 0 = z" | |
57 "constn (Suc n) = Cn 1 s [constn n]" |
57 "constn (Suc n) = Cn 1 s [constn n]" |
58 |
58 |
59 |
59 |
60 text {* |
60 text {* |
61 Signal function, which returns 1 when the input argument is greater than @{text "0"}. |
61 Sign function, which returns 1 when the input argument is greater than @{text "0"}. |
62 *} |
62 *} |
63 definition rec_sg :: "recf" |
63 definition rec_sg :: "recf" |
64 where |
64 where |
65 "rec_sg = Cn 1 rec_minus [constn 1, |
65 "rec_sg = Cn 1 rec_minus [constn 1, |
66 Cn 1 rec_minus [constn 1, id 1 0]]" |
66 Cn 1 rec_minus [constn 1, id 1 0]]" |