/seL4-l4v-master/HOL4/examples/acl2/examples/M1/ |
H A D | hol_defaxiomsScript.sml | 331 (eqlable_listp (chr c) = nil) 383 (acl2_make_character_list (chr c) = nil) 753 [chr #"\n"; chr #" "; chr #"!"; chr #"\""; chr #"#"; 754 chr #"$"; chr #"%"; chr #" [all...] |
H A D | sexpScript.sml | 97 val _ = declare_names ("ACL2_CHARACTER", "chr"); 170 `(characterp(chr x) = t) /\ (characterp _ = nil)`; 574 `(char_code(chr c) = int (&(ORD c))) /\ 592 then chr(CHR (Num(reduced_nmr a))) 593 else chr(CHR 0)) 595 (code_char _ = chr(CHR 0))`; 681 (sexp_size (chr b) = 1) /\ 687 `(make_character_list(cons (chr c) y) = 688 (cons (chr c) (make_character_list y))) 698 (* "abc" |--> (cons (chr #" [all...] |
/seL4-l4v-master/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
H A D | hol_defaxiomsScript.sml | 330 (eqlable_listp (chr c) = nil) 382 (acl2_make_character_list (chr c) = nil) 752 [chr #"\n"; chr #" "; chr #"!"; chr #"\""; chr #"#"; 753 chr #"$"; chr #"%"; chr #" [all...] |
H A D | sexpScript.sml | 97 val _ = declare_names ("ACL2_CHARACTER", "chr"); 170 `(characterp(chr x) = t) /\ (characterp _ = nil)`; 574 `(char_code(chr c) = int (&(ORD c))) /\ 592 then chr(CHR (Num(reduced_nmr a))) 593 else chr(CHR 0)) 595 (code_char _ = chr(CHR 0))`; 681 (sexp_size (chr b) = 1) /\ 687 `(make_character_list(cons (chr c) y) = 688 (cons (chr c) (make_character_list y))) 698 (* "abc" |--> (cons (chr #" [all...] |
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | hol_defaxiomsScript.sml | 326 (eqlable_listp (chr c) = nil) 378 (acl2_make_character_list (chr c) = nil) 748 [chr #"\n"; chr #" "; chr #"!"; chr #"\""; chr #"#"; 749 chr #"$"; chr #"%"; chr #" [all...] |
H A D | sexpScript.sml | 97 val _ = declare_names ("ACL2_CHARACTER", "chr"); 170 `(characterp(chr x) = t) /\ (characterp _ = nil)`; 574 `(char_code(chr c) = int (&(ORD c))) /\ 592 then chr(CHR (Num(reduced_nmr a))) 593 else chr(CHR 0)) 595 (code_char _ = chr(CHR 0))`; 681 (sexp_size (chr b) = 1) /\ 687 `(make_character_list(cons (chr c) y) = 688 (cons (chr c) (make_character_list y))) 698 (* "abc" |--> (cons (chr #" [all...] |
H A D | make_sexp.ml | 75 val _ = declare_names ("ACL2_CHARACTER", "chr"); 144 `(characterp(chr x) = t) /\ (characterp _ = nil)`; 548 `(char_code(chr c) = int (&(ORD c))) /\ 566 then chr(CHR (Num(reduced_nmr a))) 567 else chr(CHR 0)) 569 (code_char _ = chr(CHR 0))`; 650 `(make_character_list(cons (chr c) y) = 651 (cons (chr c) (make_character_list y))) 659 (* "abc" |--> (cons (chr #"a") (cons (chr #" [all...] |
/seL4-l4v-master/HOL4/src/TeX/theory_tests/ |
H A D | bag248Script.sml | 11 val _ = Unicode.unicode_version {tmnm = "<:", u = UTF8.chr 0x22F2} 15 val _ = TeX_notation {hol = UTF8.chr 0x22F2, TeX = ("\\HOLTokenIn{}:",2)}
|
/seL4-l4v-master/HOL4/examples/RL_Environment/ |
H A D | RL_Socket.sml | 21 (fn i => Char.chr(Word8.toInt(Word8Vector.sub(datar,i))))) 28 if String.isSuffix (String.str(Char.chr 0)) datar 32 else if Char.contains datar (Char.chr 0) then
|
/seL4-l4v-master/HOL4/src/portableML/ |
H A D | UTF8.sig | 14 val chr : int -> string (* May raise Chr *) value 21 val explodei : string -> int list (* invert with String.concat o map chr *)
|
H A D | UTF8Set.sml | 27 listItems' (pfx ^ chr i) acc set 56 | SOME set => recurse best (curpfx ^ chr i) rest set
|
H A D | UTF8.sml | 10 fun chr i = function 12 else if i < 128 then str (Char.chr i) 18 String.implode [Char.chr byte1, Char.chr byte2] 29 String.implode (map Char.chr [byte1, byte2, byte3]) 42 String.implode (map Char.chr [byte1, byte2, byte3, byte4]) 234 fun safecp_to_char (CP i) = chr i 235 | safecp_to_char (RB b) = str (Char.chr b)
|
H A D | UnicodeChars.sml | 4 val U = UTF8.chr 166 if i < 128 then Char.isAlpha (Char.chr i) 178 if i < 128 then Char.isDigit (Char.chr i) 183 if i < 128 then Char.isPunct (Char.chr i)
|
/seL4-l4v-master/HOL4/src/1/theory_tests/ |
H A D | SGAUnicodeMergeA2Script.sml | 15 val funion_symbol = UTF8.chr 0x228C
|
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | File.h | 93 int putCharQ(int chr) { // Quick version with minimal overhead : don't call this in wrong mode! argument 100 return buf[pos++] = (uchar)chr; } 106 int putChar(int chr) { argument 108 return putCharQ(chr); }
|
/seL4-l4v-master/HOL4/polyml/modules/IntInfAsInt/ |
H A D | StringChar.sml | 26 val chr = chr o FixedInt.fromInt value 55 val chr : int -> char = Char.chr value
|
/seL4-l4v-master/HOL4/examples/formal-languages/regular/regular-play/test/ |
H A D | regexTest.sml | 32 fun toRegAlt 0 = Sym (chr 0) 33 | toRegAlt i = Alt (Sym (chr i), toRegAlt (i - 1)) 76 implode (map (fn x => chr ((Word8.toIntX x) + 128)) (readMax maxSize []))
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | String.sml | 142 fun chr i : char = function 148 val minChar = chr 0 and maxChar = chr maxOrd 150 fun succ c = if ord c = maxOrd then raise Chr else chr(ord c + 1) 151 and pred c = if ord c = 0 then raise Chr else chr(ord c - 1) 165 fun isAscii c = c <= chr 127 170 fun toLower c = if isUpper c then chr (ord c + 32) else c 171 fun toUpper c = if isLower c then chr (ord c - 32) else c 662 if res > maxOrd then NONE else SOME(chr res, str) 669 if i >= ~1 orelse res > maxOrd then NONE else SOME(chr re 1695 val chr : int -> char = Char.chr value [all...] |
H A D | SML90.sml | 45 val chr : int -> string value 82 fun chr i = str(Char.chr i) function
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | MLstring.sml | 18 else chr v 50 scan' (chr (cord - 64) :: acc) (i + 2)
|
H A D | CharSet.sml | 80 fun g(m, acc) = Char.chr(d * 8 + m) :: acc
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/lib/ |
H A D | L3.sml | 68 val chr = Char.chr o IntInf.toInt value
|
H A D | L3.sig | 8 val chr : IntInf.int -> char value
|
/seL4-l4v-master/HOL4/examples/acl2/tests/gold/ |
H A D | test1.sml | 4 implode(map chr (cons 65 (cons 67 (cons 76 (cons 50 nil)))));
|
H A D | test1a.sml | 4 implode(map chr (cons 65 (cons 67 (cons 76 (cons 50 nil)))));
|