6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithfrom Basic/Numbers get Int

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithspec PredefinedSign =

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith Int with Int |-> integer, Nat |-> nonNegativeInteger, Pos |-> positiveInteger

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith then

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith sort Thing

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith sort boolean < DATA

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith sort integer < DATA

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith op True,False:boolean

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith sort positveInteger < nonNegativeInteger;

77c7ff125b9cf3d212f719f5dd1cbe67b51cf8e9Jon A. Cruz sort nonNegativeInteger < integer;

77c7ff125b9cf3d212f719f5dd1cbe67b51cf8e9Jon A. Cruz sort nonPositiveInteger < integer;

77c7ff125b9cf3d212f719f5dd1cbe67b51cf8e9Jon A. Cruz sort negativeInteger < nonPositiveInteger;

77c7ff125b9cf3d212f719f5dd1cbe67b51cf8e9Jon A. Cruz sort nonPositiveInteger = {p : integer . p <= 0}

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith pred Nothing : Thing

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith forall x : nonNegativeInteger

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith . 0 @@ x = x %(no_preceeding_zeros)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith forall x : Thing . not (Nothing (x)) %(gn_Nothing_def)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith sorts Char; string < DATA

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith free type string ::= emptyString | __:@:__ (Char;string)

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith ops ' ' : Char; %(DL_printable_32)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '!' : Char; %(DL_printable_33)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '\"' : Char; %(DL_printable_34)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '#' : Char; %(DL_printable_35)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '$' : Char; %(DL_printable_36)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '%' : Char; %(DL_printable_37)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '&' : Char; %(DL_printable_38)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '\'' : Char; %(DL_printable_39)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '(' : Char; %(DL_printable_40)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith ')' : Char; %(DL_printable_41)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '*' : Char; %(DL_printable_42)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '+' : Char; %(DL_printable_43)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith ',' : Char; %(DL_printable_44)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '-' : Char; %(DL_printable_45)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '.' : Char; %(DL_printable_46)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '/' : Char; %(DL_printable_47)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '0' : Char; %(DL_printable_48)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '1' : Char; %(DL_printable_49)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '2' : Char; %(DL_printable_50)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '3' : Char; %(DL_printable_51)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '4' : Char; %(DL_printable_52)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '5' : Char; %(DL_printable_53)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '6' : Char; %(DL_printable_54)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '7' : Char; %(DL_printable_55)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '8' : Char; %(DL_printable_56)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '9' : Char; %(DL_printable_57)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith ':' : Char; %(DL_printable_58)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith ';' : Char; %(DL_printable_59)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '<' : Char; %(DL_printable_60)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '=' : Char; %(DL_printable_61)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '>' : Char; %(DL_printable_62)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '?' : Char; %(DL_printable_63)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '@' : Char; %(DL_printable_64)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'A' : Char; %(DL_printable_65)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'B' : Char; %(DL_printable_66)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'C' : Char; %(DL_printable_67)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'D' : Char; %(DL_printable_68)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'E' : Char; %(DL_printable_69)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'F' : Char; %(DL_printable_70)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'G' : Char; %(DL_printable_71)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'H' : Char; %(DL_printable_72)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'I' : Char; %(DL_printable_73)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'J' : Char; %(DL_printable_74)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'K' : Char; %(DL_printable_75)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'L' : Char; %(DL_printable_76)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'M' : Char; %(DL_printable_77)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'N' : Char; %(DL_printable_78)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'O' : Char; %(DL_printable_79)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'P' : Char; %(DL_printable_80)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'Q' : Char; %(DL_printable_81)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'R' : Char; %(DL_printable_82)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'S' : Char; %(DL_printable_83)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'T' : Char; %(DL_printable_84)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'U' : Char; %(DL_printable_85)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'V' : Char; %(DL_printable_86)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'W' : Char; %(DL_printable_87)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'X' : Char; %(DL_printable_88)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'Y' : Char; %(DL_printable_89)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'Z' : Char; %(DL_printable_90)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '[' : Char; %(DL_printable_91)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '\\' : Char; %(DL_printable_92)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith ']' : Char; %(DL_printable_93)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '^' : Char; %(DL_printable_94)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '_' : Char; %(DL_printable_95)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '`' : Char; %(DL_printable_96)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'a' : Char; %(DL_printable_97)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'b' : Char; %(DL_printable_98)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'c' : Char; %(DL_printable_99)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'd' : Char; %(DL_printable_100)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'e' : Char; %(DL_printable_101)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'f' : Char; %(DL_printable_102)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'g' : Char; %(DL_printable_103)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'h' : Char; %(DL_printable_104)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'i' : Char; %(DL_printable_105)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'j' : Char; %(DL_printable_106)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'k' : Char; %(DL_printable_107)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'l' : Char; %(DL_printable_108)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'm' : Char; %(DL_printable_109)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'n' : Char; %(DL_printable_110)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'o' : Char; %(DL_printable_111)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'p' : Char; %(DL_printable_112)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'q' : Char; %(DL_printable_113)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'r' : Char; %(DL_printable_114)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 's' : Char; %(DL_printable_115)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 't' : Char; %(DL_printable_116)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'u' : Char; %(DL_printable_117)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'v' : Char; %(DL_printable_118)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'w' : Char; %(DL_printable_119)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'x' : Char; %(DL_printable_120)%

375a47157c1740a5fdd9ad733c347a53381531abAlex Valavanis 'y' : Char; %(DL_printable_121)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith 'z' : Char; %(DL_printable_122)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '{' : Char; %(DL_printable_123)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '|' : Char; %(DL_printable_124)%

375a47157c1740a5fdd9ad733c347a53381531abAlex Valavanis '}' : Char; %(DL_printable_125)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith '~' : Char; %(DL_printable_126)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith %% Iso-Latin-1 character number 160 is displayed as space,

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith %% but internally is different from character 32 (space)

375a47157c1740a5fdd9ad733c347a53381531abAlex Valavanis '�' : Char; %(DL_printable_160)%

'�' : Char; %(DL_printable_161)%

'�' : Char; %(DL_printable_162)%

'�' : Char; %(DL_printable_163)%

'�' : Char; %(DL_printable_164)%

'�' : Char; %(DL_printable_165)%

'�' : Char; %(DL_printable_166)%

'�' : Char; %(DL_printable_167)%

'�' : Char; %(DL_printable_168)%

'�' : Char; %(DL_printable_169)%

'�' : Char; %(DL_printable_170)%

'�' : Char; %(DL_printable_171)%

'�' : Char; %(DL_printable_172)%

'�' : Char; %(DL_printable_173)%

'�' : Char; %(DL_printable_174)%

'�' : Char; %(DL_printable_175)%

'�' : Char; %(DL_printable_176)%

'�' : Char; %(DL_printable_177)%

'�' : Char; %(DL_printable_178)%

'�' : Char; %(DL_printable_179)%

'�' : Char; %(DL_printable_180)%

'�' : Char; %(DL_printable_181)%

'�' : Char; %(DL_printable_182)%

'�' : Char; %(DL_printable_183)%

'�' : Char; %(DL_printable_184)%

'�' : Char; %(DL_printable_185)%

'�' : Char; %(DL_printable_186)%

'�' : Char; %(DL_printable_187)%

'�' : Char; %(DL_printable_188)%

'�' : Char; %(DL_printable_189)%

'�' : Char; %(DL_printable_190)%

'�' : Char; %(DL_printable_191)%

'�' : Char; %(DL_printable_192)%

'�' : Char; %(DL_printable_193)%

'�' : Char; %(DL_printable_194)%

'�' : Char; %(DL_printable_195)%

'�' : Char; %(DL_printable_196)%

'�' : Char; %(DL_printable_197)%

'�' : Char; %(DL_printable_198)%

'�' : Char; %(DL_printable_199)%

'�' : Char; %(DL_printable_200)%

'�' : Char; %(DL_printable_201)%

'�' : Char; %(DL_printable_202)%

'�' : Char; %(DL_printable_203)%

'�' : Char; %(DL_printable_204)%

'�' : Char; %(DL_printable_205)%

'�' : Char; %(DL_printable_206)%

'�' : Char; %(DL_printable_207)%

'�' : Char; %(DL_printable_208)%

'�' : Char; %(DL_printable_209)%

'�' : Char; %(DL_printable_210)%

'�' : Char; %(DL_printable_211)%

'�' : Char; %(DL_printable_212)%

'�' : Char; %(DL_printable_213)%

'�' : Char; %(DL_printable_214)%

'�' : Char; %(DL_printable_215)%

'�' : Char; %(DL_printable_216)%

'�' : Char; %(DL_printable_217)%

'�' : Char; %(DL_printable_218)%

'�' : Char; %(DL_printable_219)%

'�' : Char; %(DL_printable_220)%

'�' : Char; %(DL_printable_221)%

'�' : Char; %(DL_printable_222)%

'�' : Char; %(DL_printable_223)%

'�' : Char; %(DL_printable_224)%

'�' : Char; %(DL_printable_225)%

'�' : Char; %(DL_printable_226)%

'�' : Char; %(DL_printable_227)%

'�' : Char; %(DL_printable_228)%

'�' : Char; %(DL_printable_229)%

'�' : Char; %(DL_printable_230)%

'�' : Char; %(DL_printable_231)%

'�' : Char; %(DL_printable_232)%

'�' : Char; %(DL_printable_233)%

'�' : Char; %(DL_printable_234)%

'�' : Char; %(DL_printable_235)%

'�' : Char; %(DL_printable_236)%

'�' : Char; %(DL_printable_237)%

'�' : Char; %(DL_printable_238)%

'�' : Char; %(DL_printable_239)%

'�' : Char; %(DL_printable_240)%

'�' : Char; %(DL_printable_241)%

'�' : Char; %(DL_printable_242)%

'�' : Char; %(DL_printable_243)%

'�' : Char; %(DL_printable_244)%

'�' : Char; %(DL_printable_245)%

'�' : Char; %(DL_printable_246)%

'�' : Char; %(DL_printable_247)%

'�' : Char; %(DL_printable_248)%

'�' : Char; %(DL_printable_249)%

'�' : Char; %(DL_printable_250)%

'�' : Char; %(DL_printable_251)%

'�' : Char; %(DL_printable_252)%

'�' : Char; %(DL_printable_253)%

'�' : Char; %(DL_printable_254)%

'�' : Char; %(DL_printable_255)%

end