Characters


Basics | Alphanumerics | ASCII
1. Basics

   Introduces: character , character of _ , code _ .

   Includes:   Instant/Partial Order ( character for s , _ is _ , _ is less than _ ) .

    Needs:      Numbers/Naturals .
  • character = ž .
    
  • character of _ :: natural -> character (partial, injective) . 
    
  • code _ :: character -> natural (total, injective) .
(1)  character of code c:character = c .
 (2)  c:character is c':character = code c is code c' .
 (3)  c:character is less than c':character = code c is less than code c' .

   open .

Back to the beginning.

2. Alphanumerics
   Introduces:  digit , letter , lowercase _ , uppercase _ . 

  • character >= digit | letter  (disjoint) .
    
  • digit = `0'|`1'|`2'|`3'|`4'|`5'|`6'|`7'|`8'|`9'  (individual) .
    
  • letter = lowercase letter | uppercase letter (disjoint) . 
    
  • lowercase letter = `a'|...|`z' (individual) .
    
  • uppercase letter = `A'|...|`Z' (individual) .
    
  • lowercase _  :: character -> character (total) . 
    
  • uppercase _ :: character -> character (total) . 
    
Needs:	Tuples .  character <= component .

  (1) distinct (d:digit, l:lowercase letter, u:uppercase letter) = true .
  (2) strictly-increasing (`0', `1', ..., `9') = true ;
  (3) strictly-increasing (`a', `b', ..., `z') = true ;
  (4) strictly-increasing (`A', `B', ..., `Z') = true .
  (5) uppercase `a' = `A' ; lowercase `A' = `a' ; uppercase `z' = `Z' . lowercase `Z' = `z' .
  (6) lowercase lowercase l:letter = lowercase l ; 
          	uppercase uppercase l:letter = uppercase l .
  (7) c&letter = nothing => lowercase c:character = c ; uppercase c:character = c .

  open.

Back to the beginning.

3. ASCII

  Introduces:  graphic-character , control _ , control-character , format-effector .

  Needs:      Strings/Alphanumerics .
  • code _ :: character -> natural [max octal``177''] (total, injective) . 
    
  • character =  graphic-character | control-character .
    
  • graphic-character =
            ` '   |  `!'   |  `"'  | `#'  | `$'  | `%'   |  `&' | `''  | 
            `('   |  `)'   |  `*'  |  `+' | `,'  |  `--' |  `.' |  `/' |  
            digit |  `:'   |  `;'  | `<'  |  `=' |  `>'  | `?'  |  
            `@'   |  uppercase letter | `['  |  `\'   |  `]'   |  `^'  | `_'  |         
    	  `''   |  lowercase letter | `{'   |  `|'   |  `}'  | `~' (individual) .
    
  • control _ :: `@' |uppercase letter|`['|`\'|`]'|`^'|`_'|`?' ->
    	control-character (total, injective) . 
    
  • format-effector = control (`I'|`J'|`K'|`L'|`M') .
(1) c&(`@'|uppercase letter|`['|`\'|`]'|`^'|`_'|`?') = nothing =>
       		control c:character = nothing .
 (2) code control`M' = control`@' = octal``000'' ;	control`A' = octal``001'' ; ...
 	code ` ' = octal``040'' ; ...
 	code `~' = octal``176'' ; code control`?' = octal``177'' .

   closed .

Back to the beginning.

Index | Instant | Tuples | Truth-Values | Numbers | Characters | Lists | Strings | Syntax | Sets | Maps