Basics |
Alphanumerics
1. Basics
Introduces: string , string of_ , characters_ , " " , _^_ .
Includes: Instant/Distinction ( string for s , _ is _ ) .
Needs: Tuples/Basics, Lists/Flat . character <= item .
- string = flat-list [character] .
- string of_ :: character* -> string (total, injective) .
- characters_ :: string -> character* (total, injective) .
- " " :: string .
- _^_ :: string, string -> string (total, associative, unit is " ").
- _is_ :: string, string -> truth-value (total) .
(1) "" = empty-list .
(2) string of c:character* = list of c .
(3) characters s:string = items s .
(4) (s1:string)^(s2:string) = concatenation (s1,
s2) .
* The notation "c" abbreviates
string of 'c'. Moreover, for
n>=2, the notation "c1...cn"
abbreviates "c1"^...^"cn".
2. Alphanumerics
Introduces: lowercase_ , uppercase_ , decimal_ , octal-digit , octal _ .
Needs: Tuples/Basics, Numbers/Naturals .
- lowercase_ :: string -> string (total) .
- uppercase_ :: string -> string (total) .
- decimal_ :: string of digit+ -> natural (total) .
- octal _ :: string of octal-digit+ -> natural (total).
- octal-digit = ` 0 ' | ` 1 ' | ` 2 ' | ` 3 ' | ` 4 ' | ` 5 ' | ` 6 ' | ` 7 '.
(1) lowercase " " = " " ; lowercase string of c:character = string of lowercase
c;
lowercase (s1:string ^ s2:string) = lowercase
s1 ^ lowercase s2 .
(2) uppercase "" = "" ; uppercase string of c:character = string of uppercase
c;
uppercase (s1:string ^ s2:string) = uppercase
s1 ^ uppercase s2 .
(3) decimal "0" = 0 ; decimal "1" = 1 ; decimal "2" = 2 ;
decimal "3" = 3 ; decimal "4" = 4 ; decimal "5" = 5 ;
decimal "6" = 6 ; decimal "7" = 7 ; decimal "8" = 8 ;
decimal "9" = 9 ;
decimal (s:string of digit+ ^ string of d:digit) =
sum (product (10, decimal s), decimal (string of d)) .
(4) octal (string of d:octal-digit) = decimal (string of d) ;
octal "8" = nothing ; octal "9" = nothing ;
octal (s:string of octal-digit+ ^ string of d:octal-digit)=
sum (product (8, octal s), octal (string of d)) .
|