Ceres
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1310 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (887 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (80 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (77 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (36 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (58 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (110 entries) |
Global Index
A
ab:22 [binder, in Ceres.CeresSerialize]ab:28 [binder, in Ceres.CeresSerialize]
after_atom_string_cons [lemma, in Ceres.CeresParserRoundtrip]
after_atom_string_nil_inv [lemma, in Ceres.CeresParserRoundtrip]
after_atom_cons [constructor, in Ceres.CeresParserRoundtrip]
after_atom_nil [constructor, in Ceres.CeresParserRoundtrip]
after_atom_string [inductive, in Ceres.CeresParserRoundtrip]
after_atom_string_snoc [lemma, in Ceres.CeresParserRoundtripProof]
all_con:45 [binder, in Ceres.CeresDeserialize]
all_con:39 [binder, in Ceres.CeresDeserialize]
app_cons_assoc [lemma, in Ceres.CeresUtils]
AsciiTest [section, in Ceres.CeresString]
ascii_compare [definition, in Ceres.CeresString]
Atom [abbreviation, in Ceres.CeresS]
atom [inductive, in Ceres.CeresS]
atom_token_Str [constructor, in Ceres.CeresParserRoundtrip]
atom_token_Num [constructor, in Ceres.CeresParserRoundtrip]
atom_token_Raw [constructor, in Ceres.CeresParserRoundtrip]
atom_token [inductive, in Ceres.CeresParserRoundtrip]
atom_string [definition, in Ceres.CeresParserRoundtrip]
Atom_ [constructor, in Ceres.CeresS]
atom_token_atom [lemma, in Ceres.CeresParserRoundtripProof]
a_eqb:41 [binder, in Ceres.CeresS]
a':120 [binder, in Ceres.CeresRoundtrip]
A:1 [binder, in Ceres.CeresSerialize]
A:1 [binder, in Ceres.CeresUtils]
A:1 [binder, in Ceres.CeresString]
A:1 [binder, in Ceres.CeresS]
A:1 [binder, in Ceres.CeresFormat]
A:1 [binder, in Ceres.CeresRoundtrip]
A:10 [binder, in Ceres.CeresSerialize]
A:10 [binder, in Ceres.CeresRoundtrip]
a:104 [binder, in Ceres.CeresRoundtrip]
a:107 [binder, in Ceres.CeresDeserialize]
A:108 [binder, in Ceres.CeresRoundtrip]
A:11 [binder, in Ceres.CeresDeserialize]
a:11 [binder, in Ceres.CeresUtils]
a:11 [binder, in Ceres.CeresFormat]
A:111 [binder, in Ceres.CeresDeserialize]
a:114 [binder, in Ceres.CeresRoundtrip]
A:12 [binder, in Ceres.CeresS]
a:123 [binder, in Ceres.CeresDeserialize]
A:123 [binder, in Ceres.CeresRoundtrip]
A:127 [binder, in Ceres.CeresRoundtrip]
A:128 [binder, in Ceres.CeresDeserialize]
A:13 [binder, in Ceres.CeresDeserialize]
A:132 [binder, in Ceres.CeresDeserialize]
A:135 [binder, in Ceres.CeresRoundtrip]
A:138 [binder, in Ceres.CeresDeserialize]
A:14 [binder, in Ceres.CeresSerialize]
A:143 [binder, in Ceres.CeresRoundtrip]
A:146 [binder, in Ceres.CeresDeserialize]
a:152 [binder, in Ceres.CeresRoundtrip]
A:153 [binder, in Ceres.CeresRoundtrip]
A:156 [binder, in Ceres.CeresDeserialize]
A:157 [binder, in Ceres.CeresRoundtrip]
A:16 [binder, in Ceres.CeresDeserialize]
A:16 [binder, in Ceres.CeresRoundtrip]
a:161 [binder, in Ceres.CeresRoundtrip]
A:165 [binder, in Ceres.CeresRoundtrip]
A:168 [binder, in Ceres.CeresDeserialize]
A:17 [binder, in Ceres.CeresUtils]
a:17 [binder, in Ceres.CeresString]
A:177 [binder, in Ceres.CeresDeserialize]
A:18 [binder, in Ceres.CeresSerialize]
A:18 [binder, in Ceres.CeresS]
a:185 [binder, in Ceres.CeresDeserialize]
A:186 [binder, in Ceres.CeresDeserialize]
A:19 [binder, in Ceres.CeresDeserialize]
a:190 [binder, in Ceres.CeresDeserialize]
A:191 [binder, in Ceres.CeresDeserialize]
A:194 [binder, in Ceres.CeresDeserialize]
A:201 [binder, in Ceres.CeresDeserialize]
A:203 [binder, in Ceres.CeresDeserialize]
A:207 [binder, in Ceres.CeresDeserialize]
a:21 [binder, in Ceres.CeresString]
a:214 [binder, in Ceres.CeresDeserialize]
A:22 [binder, in Ceres.CeresDeserialize]
A:22 [binder, in Ceres.CeresRoundtrip]
A:226 [binder, in Ceres.CeresDeserialize]
A:23 [binder, in Ceres.CeresUtils]
A:234 [binder, in Ceres.CeresDeserialize]
A:24 [binder, in Ceres.CeresSerialize]
a:25 [binder, in Ceres.CeresString]
a:25 [binder, in Ceres.CeresS]
a:26 [binder, in Ceres.CeresRoundtrip]
A:27 [binder, in Ceres.CeresString]
a:27 [binder, in Ceres.CeresS]
A:28 [binder, in Ceres.CeresRoundtrip]
A:29 [binder, in Ceres.CeresDeserialize]
a:29 [binder, in Ceres.CeresString]
a:29 [binder, in Ceres.CeresS]
a:3 [binder, in Tutorial]
a:31 [binder, in Ceres.CeresSerialize]
A:31 [binder, in Ceres.CeresDeserialize]
A:31 [binder, in Ceres.CeresS]
A:33 [binder, in Ceres.CeresSerialize]
a:33 [binder, in Ceres.CeresString]
a:33 [binder, in Ceres.CeresRoundtrip]
a:35 [binder, in Ceres.CeresString]
A:35 [binder, in Ceres.CeresRoundtrip]
a:37 [binder, in Ceres.CeresString]
a:39 [binder, in Ceres.CeresString]
A:39 [binder, in Ceres.CeresS]
A:39 [binder, in Ceres.CeresRoundtrip]
A:4 [binder, in Ceres.CeresSerialize]
a:4 [binder, in Ceres.CeresS]
a:4 [binder, in Ceres.CeresRoundtrip]
A:43 [binder, in Ceres.CeresRoundtrip]
A:48 [binder, in Ceres.CeresDeserialize]
a:49 [binder, in Ceres.CeresRoundtrip]
A:5 [binder, in Ceres.CeresRoundtrip]
A:50 [binder, in Ceres.CeresParserRoundtrip]
A:51 [binder, in Ceres.CeresS]
A:53 [binder, in Ceres.CeresRoundtrip]
a:54 [binder, in Ceres.CeresS]
a:57 [binder, in Ceres.CeresRoundtrip]
A:59 [binder, in Ceres.CeresDeserialize]
a:6 [binder, in Ceres.CeresSerialize]
A:6 [binder, in Ceres.CeresS]
A:64 [binder, in Ceres.CeresRoundtrip]
a:67 [binder, in Ceres.CeresParserRoundtrip]
A:68 [binder, in Ceres.CeresS]
a:69 [binder, in Ceres.CeresDeserialize]
A:69 [binder, in Ceres.CeresRoundtrip]
A:7 [binder, in Ceres.CeresSerialize]
A:7 [binder, in Ceres.CeresDeserialize]
A:7 [binder, in Ceres.CeresUtils]
a:70 [binder, in Ceres.CeresS]
A:71 [binder, in Ceres.CeresParserRoundtrip]
A:73 [binder, in Ceres.CeresDeserialize]
A:73 [binder, in Ceres.CeresS]
a:75 [binder, in Ceres.CeresRoundtrip]
a:77 [binder, in Ceres.CeresDeserialize]
A:78 [binder, in Ceres.CeresDeserialize]
A:79 [binder, in Ceres.CeresRoundtrip]
A:8 [binder, in Ceres.CeresDeserialize]
A:8 [binder, in Ceres.CeresFormat]
A:83 [binder, in Ceres.CeresRoundtrip]
a:84 [binder, in Ceres.CeresDeserialize]
A:86 [binder, in Ceres.CeresDeserialize]
a:9 [binder, in Ceres.CeresRoundtrip]
A:91 [binder, in Ceres.CeresRoundtrip]
a:94 [binder, in Ceres.CeresDeserialize]
A:97 [binder, in Ceres.CeresDeserialize]
B
Bool [constructor, in Tutorial]B':3 [binder, in Ceres.CeresUtils]
b:108 [binder, in Ceres.CeresDeserialize]
B:109 [binder, in Ceres.CeresRoundtrip]
B:112 [binder, in Ceres.CeresDeserialize]
b:112 [binder, in Ceres.CeresString]
b:124 [binder, in Ceres.CeresDeserialize]
B:128 [binder, in Ceres.CeresRoundtrip]
b:13 [binder, in Ceres.CeresSerialize]
B:13 [binder, in Ceres.CeresS]
B:133 [binder, in Ceres.CeresDeserialize]
B:136 [binder, in Ceres.CeresRoundtrip]
B:139 [binder, in Ceres.CeresDeserialize]
b:14 [binder, in Ceres.CeresUtils]
B:147 [binder, in Ceres.CeresDeserialize]
B:157 [binder, in Ceres.CeresDeserialize]
B:178 [binder, in Ceres.CeresDeserialize]
B:18 [binder, in Ceres.CeresUtils]
b:18 [binder, in Ceres.CeresString]
B:19 [binder, in Ceres.CeresSerialize]
B:2 [binder, in Ceres.CeresUtils]
B:204 [binder, in Ceres.CeresDeserialize]
B:208 [binder, in Ceres.CeresDeserialize]
b:215 [binder, in Ceres.CeresDeserialize]
b:22 [binder, in Ceres.CeresString]
B:25 [binder, in Ceres.CeresSerialize]
b:26 [binder, in Ceres.CeresString]
b:30 [binder, in Ceres.CeresString]
B:32 [binder, in Ceres.CeresS]
b:34 [binder, in Ceres.CeresString]
b:36 [binder, in Ceres.CeresString]
b:38 [binder, in Ceres.CeresString]
b:40 [binder, in Ceres.CeresString]
B:40 [binder, in Ceres.CeresS]
B:51 [binder, in Ceres.CeresParserRoundtrip]
B:54 [binder, in Ceres.CeresRoundtrip]
b:55 [binder, in Ceres.CeresS]
B:60 [binder, in Ceres.CeresDeserialize]
b:60 [binder, in Ceres.CeresRoundtrip]
B:7 [binder, in Ceres.CeresS]
B:72 [binder, in Ceres.CeresParserRoundtrip]
B:79 [binder, in Ceres.CeresDeserialize]
B:8 [binder, in Ceres.CeresUtils]
B:84 [binder, in Ceres.CeresRoundtrip]
b:85 [binder, in Ceres.CeresDeserialize]
B:87 [binder, in Ceres.CeresDeserialize]
B:92 [binder, in Ceres.CeresRoundtrip]
b:95 [binder, in Ceres.CeresDeserialize]
B:98 [binder, in Ceres.CeresDeserialize]
C
Ceres [library]CeresDeserialize [library]
CeresFormat [library]
CeresParser [library]
CeresParserInternal [library]
CeresParserRoundtrip [library]
CeresParserRoundtripProof [library]
CeresParserUtils [library]
CeresRoundtrip [library]
CeresS [library]
CeresSerialize [library]
CeresString [library]
CeresUtils [library]
comma_sep [definition, in Ceres.CeresString]
Comment [constructor, in Ceres.CeresParserInternal]
comment [inductive, in Ceres.CeresParserRoundtrip]
comment_mk [constructor, in Ceres.CeresParserRoundtrip]
compb [definition, in Ceres.CeresString]
compcomp [definition, in Ceres.CeresString]
Complete [definition, in Ceres.CeresRoundtrip]
CompleteClass [record, in Ceres.CeresRoundtrip]
CompleteClass [inductive, in Ceres.CeresRoundtrip]
CompleteClass_ascii [instance, in Ceres.CeresRoundtrip]
CompleteClass_string [instance, in Ceres.CeresRoundtrip]
CompleteClass_list [instance, in Ceres.CeresRoundtrip]
CompleteClass_prod [instance, in Ceres.CeresRoundtrip]
CompleteClass_sum [instance, in Ceres.CeresRoundtrip]
CompleteClass_option [instance, in Ceres.CeresRoundtrip]
CompleteClass_bool [instance, in Ceres.CeresRoundtrip]
CompleteClass_Integral [instance, in Ceres.CeresRoundtrip]
CompleteIntegral [record, in Ceres.CeresRoundtrip]
CompleteIntegral [inductive, in Ceres.CeresRoundtrip]
complete_class_list [lemma, in Ceres.CeresRoundtrip]
Complete_nat [instance, in Ceres.CeresRoundtrip]
Complete_N [instance, in Ceres.CeresRoundtrip]
Complete_Z [instance, in Ceres.CeresRoundtrip]
complete_integral [projection, in Ceres.CeresRoundtrip]
complete_integral [constructor, in Ceres.CeresRoundtrip]
complete_class [projection, in Ceres.CeresRoundtrip]
complete_class [constructor, in Ceres.CeresRoundtrip]
c':69 [binder, in Ceres.CeresString]
c':72 [binder, in Ceres.CeresString]
c0:31 [binder, in Ceres.CeresString]
c0:33 [binder, in Ceres.CeresDeserialize]
c0:71 [binder, in Ceres.CeresRoundtrip]
c0:99 [binder, in Ceres.CeresString]
c1:32 [binder, in Ceres.CeresString]
c1:34 [binder, in Ceres.CeresDeserialize]
c1:72 [binder, in Ceres.CeresRoundtrip]
c1:98 [binder, in Ceres.CeresString]
c2:97 [binder, in Ceres.CeresString]
c:109 [binder, in Ceres.CeresDeserialize]
C:113 [binder, in Ceres.CeresDeserialize]
c:116 [binder, in Ceres.CeresString]
c:12 [binder, in Ceres.CeresParserRoundtrip]
c:12 [binder, in Ceres.CeresParserRoundtripProof]
c:125 [binder, in Ceres.CeresDeserialize]
C:140 [binder, in Ceres.CeresDeserialize]
C:148 [binder, in Ceres.CeresDeserialize]
C:158 [binder, in Ceres.CeresDeserialize]
c:17 [binder, in Ceres.CeresParserRoundtrip]
c:183 [binder, in Ceres.CeresParserRoundtripProof]
c:189 [binder, in Ceres.CeresParserRoundtripProof]
C:19 [binder, in Ceres.CeresUtils]
c:193 [binder, in Ceres.CeresParserRoundtripProof]
c:194 [binder, in Ceres.CeresParserRoundtripProof]
c:2 [binder, in Ceres.CeresParserRoundtripProof]
c:200 [binder, in Ceres.CeresParserRoundtripProof]
c:210 [binder, in Ceres.CeresParserRoundtripProof]
c:221 [binder, in Ceres.CeresParserRoundtripProof]
c:27 [binder, in Ceres.CeresParserInternal]
c:35 [binder, in Ceres.CeresDeserialize]
c:39 [binder, in Ceres.CeresParserRoundtrip]
c:42 [binder, in Ceres.CeresParserInternal]
c:43 [binder, in Ceres.CeresDeserialize]
c:44 [binder, in Ceres.CeresParserInternal]
c:44 [binder, in Ceres.CeresParserRoundtrip]
c:48 [binder, in Ceres.CeresParserRoundtrip]
c:49 [binder, in Ceres.CeresParserInternal]
c:50 [binder, in Ceres.CeresRoundtrip]
c:51 [binder, in Ceres.CeresRoundtrip]
c:52 [binder, in Ceres.CeresString]
C:55 [binder, in Ceres.CeresRoundtrip]
c:6 [binder, in Ceres.CeresParserUtils]
c:63 [binder, in Ceres.CeresParserRoundtripProof]
c:65 [binder, in Ceres.CeresString]
c:65 [binder, in Ceres.CeresParserRoundtripProof]
c:68 [binder, in Ceres.CeresString]
c:71 [binder, in Ceres.CeresString]
c:76 [binder, in Ceres.CeresString]
c:76 [binder, in Ceres.CeresParserRoundtripProof]
c:77 [binder, in Ceres.CeresString]
c:79 [binder, in Ceres.CeresString]
c:80 [binder, in Ceres.CeresString]
c:81 [binder, in Ceres.CeresString]
c:81 [binder, in Ceres.CeresParserRoundtripProof]
c:82 [binder, in Ceres.CeresString]
C:88 [binder, in Ceres.CeresDeserialize]
C:9 [binder, in Ceres.CeresUtils]
c:91 [binder, in Ceres.CeresParserRoundtripProof]
c:95 [binder, in Ceres.CeresString]
c:96 [binder, in Ceres.CeresDeserialize]
C:99 [binder, in Ceres.CeresDeserialize]
D
DeBindField [section, in Ceres.CeresRoundtrip]Decidable_eq_string [instance, in Ceres.CeresString]
Decidable_eq_ascii [instance, in Ceres.CeresString]
Decidable_eq_sexp [instance, in Ceres.CeresS]
Decidable_eq_atom [instance, in Ceres.CeresS]
DeRetField [section, in Ceres.CeresRoundtrip]
Deser [module, in Ceres.CeresDeserialize]
DeserError [constructor, in Ceres.CeresDeserialize]
Deserialize [record, in Ceres.CeresDeserialize]
Deserialize [inductive, in Ceres.CeresDeserialize]
Deserialize_sexp [instance, in Ceres.CeresDeserialize]
Deserialize_list [instance, in Ceres.CeresDeserialize]
Deserialize_ascii [instance, in Ceres.CeresDeserialize]
Deserialize_string [instance, in Ceres.CeresDeserialize]
Deserialize_unit [instance, in Ceres.CeresDeserialize]
Deserialize_Empty_set [instance, in Ceres.CeresDeserialize]
Deserialize_prod [instance, in Ceres.CeresDeserialize]
Deserialize_sum [instance, in Ceres.CeresDeserialize]
Deserialize_option [instance, in Ceres.CeresDeserialize]
Deserialize_bool [instance, in Ceres.CeresDeserialize]
Deserialize_SemiIntegral [instance, in Ceres.CeresDeserialize]
Deserialize_t [instance, in Tutorial]
Deser.as_fun [definition, in Ceres.CeresDeserialize]
Deser.bind_field [definition, in Ceres.CeresDeserialize]
Deser.con_ [definition, in Ceres.CeresDeserialize]
Deser.con0 [definition, in Ceres.CeresDeserialize]
Deser.con1 [definition, in Ceres.CeresDeserialize]
Deser.con1_ [definition, in Ceres.CeresDeserialize]
Deser.con2 [definition, in Ceres.CeresDeserialize]
Deser.con2_ [definition, in Ceres.CeresDeserialize]
Deser.con3 [definition, in Ceres.CeresDeserialize]
Deser.con3_ [definition, in Ceres.CeresDeserialize]
Deser.con4 [definition, in Ceres.CeresDeserialize]
Deser.con4_ [definition, in Ceres.CeresDeserialize]
Deser.con5 [definition, in Ceres.CeresDeserialize]
Deser.con5_ [definition, in Ceres.CeresDeserialize]
Deser.DeserFromSexpList [record, in Ceres.CeresDeserialize]
Deser.DeserFromSexpList [inductive, in Ceres.CeresDeserialize]
Deser.DeserFromSexpList_S [instance, in Ceres.CeresDeserialize]
Deser.DeserFromSexpList_0 [instance, in Ceres.CeresDeserialize]
Deser.fields [definition, in Ceres.CeresDeserialize]
Deser.match_con [definition, in Ceres.CeresDeserialize]
Deser.Notations [module, in Ceres.CeresDeserialize]
_ >>= _ (deser_scope) [notation, in Ceres.CeresDeserialize]
Deser.ret [definition, in Ceres.CeresDeserialize]
Deser._from_sexp_list [projection, in Ceres.CeresDeserialize]
Deser._from_sexp_list [constructor, in Ceres.CeresDeserialize]
Deser._con [definition, in Ceres.CeresDeserialize]
de:3 [binder, in Ceres.CeresRoundtrip]
de:7 [binder, in Ceres.CeresRoundtrip]
digit_of_ascii [definition, in Ceres.CeresString]
doa:100 [binder, in Ceres.CeresString]
DString [module, in Ceres.CeresString]
dstring_A:2 [binder, in Ceres.CeresFormat]
dstring_of_sexp [definition, in Ceres.CeresFormat]
DString.app_string [definition, in Ceres.CeresString]
DString.of_ascii [definition, in Ceres.CeresString]
DString.of_string [definition, in Ceres.CeresString]
DString.t [definition, in Ceres.CeresString]
D:100 [binder, in Ceres.CeresDeserialize]
d:105 [binder, in Ceres.CeresParserRoundtripProof]
d:110 [binder, in Ceres.CeresDeserialize]
d:112 [binder, in Ceres.CeresParserRoundtripProof]
D:114 [binder, in Ceres.CeresDeserialize]
d:126 [binder, in Ceres.CeresDeserialize]
d:127 [binder, in Ceres.CeresParserRoundtripProof]
d:138 [binder, in Ceres.CeresParserRoundtripProof]
D:149 [binder, in Ceres.CeresDeserialize]
d:151 [binder, in Ceres.CeresParserRoundtripProof]
D:159 [binder, in Ceres.CeresDeserialize]
d:159 [binder, in Ceres.CeresParserRoundtripProof]
d:17 [binder, in Ceres.CeresParserInternal]
d:174 [binder, in Ceres.CeresParserRoundtripProof]
d:223 [binder, in Ceres.CeresParserRoundtripProof]
d:33 [binder, in Ceres.CeresParserInternal]
E
Ei:214 [binder, in Ceres.CeresParserRoundtripProof]EmptyInput [constructor, in Ceres.CeresParserUtils]
eof [definition, in Ceres.CeresParserInternal]
eof_sound [lemma, in Ceres.CeresParserRoundtripProof]
eqb_eq_string [lemma, in Ceres.CeresString]
eqb_string [definition, in Ceres.CeresString]
eqb_eq_ascii' [lemma, in Ceres.CeresString]
eqb_eq_ascii [lemma, in Ceres.CeresString]
eqb_eq [definition, in Ceres.CeresString]
eqb_ascii [definition, in Ceres.CeresString]
eqb_eq_bool' [lemma, in Ceres.CeresString]
eqb_eq_bool [lemma, in Ceres.CeresString]
eqb_eq_sexp [definition, in Ceres.CeresS]
eqb_A:74 [binder, in Ceres.CeresS]
eqb_eq_sexp_ [lemma, in Ceres.CeresS]
eqb_eq_atom [lemma, in Ceres.CeresS]
eqb_eq_list [lemma, in Ceres.CeresS]
eqb_sexp [definition, in Ceres.CeresS]
eqb_atom [definition, in Ceres.CeresS]
eqb_sexp_ [definition, in Ceres.CeresS]
eqb_list [definition, in Ceres.CeresS]
eqb:10 [binder, in Ceres.CeresUtils]
eqb:28 [binder, in Ceres.CeresString]
eqb:52 [binder, in Ceres.CeresS]
eqb:56 [binder, in Ceres.CeresRoundtrip]
error [inductive, in Ceres.CeresDeserialize]
error [inductive, in Ceres.CeresParserUtils]
err:106 [binder, in Ceres.CeresRoundtrip]
err:117 [binder, in Ceres.CeresRoundtrip]
err:37 [binder, in Ceres.CeresDeserialize]
escape [inductive, in Ceres.CeresParserInternal]
escaped_s':92 [binder, in Ceres.CeresString]
escape_string [definition, in Ceres.CeresString]
escape_string_regular [lemma, in Ceres.CeresParserRoundtripProof]
escape_string_dquote [lemma, in Ceres.CeresParserRoundtripProof]
escape_string_backslash [lemma, in Ceres.CeresParserRoundtripProof]
escape_string_newline [lemma, in Ceres.CeresParserRoundtripProof]
escape_to_string [definition, in Ceres.CeresParserRoundtripProof]
EscBackslash [constructor, in Ceres.CeresParserInternal]
EscNone [constructor, in Ceres.CeresParserInternal]
es':122 [binder, in Ceres.CeresRoundtrip]
es1:5 [binder, in Ceres.CeresParserRoundtripProof]
es2:6 [binder, in Ceres.CeresParserRoundtripProof]
es:107 [binder, in Ceres.CeresRoundtrip]
es:115 [binder, in Ceres.CeresRoundtrip]
es:145 [binder, in Ceres.CeresParserRoundtripProof]
es:147 [binder, in Ceres.CeresRoundtrip]
es:164 [binder, in Ceres.CeresParserRoundtripProof]
es:228 [binder, in Ceres.CeresParserRoundtripProof]
es:234 [binder, in Ceres.CeresParserRoundtripProof]
es:240 [binder, in Ceres.CeresParserRoundtripProof]
es:38 [binder, in Ceres.CeresDeserialize]
es:52 [binder, in Ceres.CeresRoundtrip]
es:56 [binder, in Ceres.CeresDeserialize]
es:67 [binder, in Ceres.CeresDeserialize]
es:69 [binder, in Ceres.CeresParserRoundtrip]
es:77 [binder, in Ceres.CeresParserRoundtrip]
es:78 [binder, in Ceres.CeresParserRoundtrip]
es:78 [binder, in Ceres.CeresRoundtrip]
Example [section, in Ceres.CeresS]
Example.example_2 [variable, in Ceres.CeresS]
Example.example_1 [variable, in Ceres.CeresS]
example1 [definition, in Tutorial]
example2 [definition, in Tutorial]
Exp [constructor, in Ceres.CeresParserInternal]
e':121 [binder, in Ceres.CeresRoundtrip]
e':30 [binder, in Ceres.CeresParserInternal]
e:101 [binder, in Ceres.CeresParserRoundtripProof]
E:115 [binder, in Ceres.CeresDeserialize]
e:127 [binder, in Ceres.CeresDeserialize]
E:160 [binder, in Ceres.CeresDeserialize]
e:19 [binder, in Ceres.CeresParserInternal]
e:197 [binder, in Ceres.CeresDeserialize]
e:201 [binder, in Ceres.CeresParserRoundtripProof]
e:212 [binder, in Ceres.CeresDeserialize]
e:218 [binder, in Ceres.CeresDeserialize]
e:221 [binder, in Ceres.CeresDeserialize]
e:224 [binder, in Ceres.CeresDeserialize]
e:237 [binder, in Ceres.CeresDeserialize]
e:25 [binder, in Ceres.CeresParserInternal]
e:27 [binder, in Ceres.CeresDeserialize]
e:3 [binder, in Ceres.CeresParserRoundtripProof]
e:4 [binder, in Ceres.CeresParserUtils]
e:41 [binder, in Ceres.CeresParserRoundtripProof]
e:48 [binder, in Ceres.CeresRoundtrip]
e:60 [binder, in Ceres.CeresParserRoundtripProof]
e:7 [binder, in Tutorial]
e:71 [binder, in Ceres.CeresParserRoundtripProof]
e:74 [binder, in Ceres.CeresRoundtrip]
e:8 [binder, in Ceres.CeresRoundtrip]
F
forall_Forall [lemma, in Ceres.CeresS]FromSexp [definition, in Ceres.CeresDeserialize]
FromSexpList [definition, in Ceres.CeresDeserialize]
FromSexpListN [record, in Ceres.CeresDeserialize]
from_Z [projection, in Ceres.CeresDeserialize]
from_Z [constructor, in Ceres.CeresDeserialize]
from_string [definition, in Ceres.CeresDeserialize]
from_sexp [definition, in Ceres.CeresDeserialize]
fs:148 [binder, in Ceres.CeresRoundtrip]
f:102 [binder, in Ceres.CeresDeserialize]
f:113 [binder, in Ceres.CeresRoundtrip]
f:117 [binder, in Ceres.CeresDeserialize]
f:13 [binder, in Ceres.CeresUtils]
f:130 [binder, in Ceres.CeresDeserialize]
f:135 [binder, in Ceres.CeresDeserialize]
f:14 [binder, in Ceres.CeresS]
f:142 [binder, in Ceres.CeresDeserialize]
f:151 [binder, in Ceres.CeresDeserialize]
f:162 [binder, in Ceres.CeresDeserialize]
f:184 [binder, in Ceres.CeresDeserialize]
f:21 [binder, in Ceres.CeresUtils]
f:25 [binder, in Ceres.CeresDeserialize]
f:30 [binder, in Ceres.CeresDeserialize]
f:33 [binder, in Ceres.CeresS]
f:4 [binder, in Ceres.CeresUtils]
f:46 [binder, in Ceres.CeresRoundtrip]
f:56 [binder, in Ceres.CeresString]
f:59 [binder, in Ceres.CeresRoundtrip]
f:64 [binder, in Ceres.CeresDeserialize]
f:75 [binder, in Ceres.CeresDeserialize]
f:8 [binder, in Ceres.CeresS]
f:81 [binder, in Ceres.CeresDeserialize]
f:90 [binder, in Ceres.CeresDeserialize]
G
get_one [definition, in Ceres.CeresParserInternal]get_done [definition, in Ceres.CeresParserInternal]
get_Raw [definition, in Ceres.CeresS]
get_Str [definition, in Ceres.CeresS]
get_Num [definition, in Ceres.CeresS]
g:24 [binder, in Ceres.CeresDeserialize]
g:45 [binder, in Ceres.CeresRoundtrip]
H
Hdone:147 [binder, in Ceres.CeresParserRoundtripProof]Hdone:169 [binder, in Ceres.CeresParserRoundtripProof]
Hdu:131 [binder, in Ceres.CeresParserRoundtripProof]
Heqb_eq:75 [binder, in Ceres.CeresS]
Heqb:56 [binder, in Ceres.CeresS]
Hes:150 [binder, in Ceres.CeresParserRoundtripProof]
Hes:172 [binder, in Ceres.CeresParserRoundtripProof]
Hi:157 [binder, in Ceres.CeresParserRoundtripProof]
Hi:206 [binder, in Ceres.CeresParserRoundtripProof]
Hi:213 [binder, in Ceres.CeresParserRoundtripProof]
Hmore:133 [binder, in Ceres.CeresParserRoundtripProof]
Hstackend:149 [binder, in Ceres.CeresParserRoundtripProof]
Hstackend:171 [binder, in Ceres.CeresParserRoundtripProof]
Hstack:148 [binder, in Ceres.CeresParserRoundtripProof]
Hstack:170 [binder, in Ceres.CeresParserRoundtripProof]
Hs0:146 [binder, in Ceres.CeresParserRoundtripProof]
Hs0:168 [binder, in Ceres.CeresParserRoundtripProof]
Hs:216 [binder, in Ceres.CeresParserRoundtripProof]
H0:12 [binder, in Ceres.CeresRoundtrip]
H0:136 [binder, in Ceres.CeresParserRoundtripProof]
H0:137 [binder, in Ceres.CeresDeserialize]
H0:144 [binder, in Ceres.CeresDeserialize]
H0:153 [binder, in Ceres.CeresDeserialize]
H0:164 [binder, in Ceres.CeresDeserialize]
H0:18 [binder, in Ceres.CeresRoundtrip]
H0:183 [binder, in Ceres.CeresDeserialize]
H0:206 [binder, in Ceres.CeresDeserialize]
H0:21 [binder, in Ceres.CeresSerialize]
H0:210 [binder, in Ceres.CeresDeserialize]
H0:24 [binder, in Ceres.CeresRoundtrip]
H0:27 [binder, in Ceres.CeresSerialize]
H0:30 [binder, in Ceres.CeresRoundtrip]
H1:126 [binder, in Ceres.CeresRoundtrip]
H1:131 [binder, in Ceres.CeresRoundtrip]
H1:139 [binder, in Ceres.CeresRoundtrip]
H1:145 [binder, in Ceres.CeresDeserialize]
H1:146 [binder, in Ceres.CeresRoundtrip]
H1:154 [binder, in Ceres.CeresDeserialize]
H1:156 [binder, in Ceres.CeresRoundtrip]
H1:160 [binder, in Ceres.CeresRoundtrip]
H1:165 [binder, in Ceres.CeresDeserialize]
H1:168 [binder, in Ceres.CeresRoundtrip]
H1:38 [binder, in Ceres.CeresRoundtrip]
H1:42 [binder, in Ceres.CeresRoundtrip]
H1:82 [binder, in Ceres.CeresRoundtrip]
H1:87 [binder, in Ceres.CeresRoundtrip]
H1:95 [binder, in Ceres.CeresRoundtrip]
H2:155 [binder, in Ceres.CeresDeserialize]
H2:166 [binder, in Ceres.CeresDeserialize]
H3:167 [binder, in Ceres.CeresDeserialize]
H4:134 [binder, in Ceres.CeresRoundtrip]
H4:142 [binder, in Ceres.CeresRoundtrip]
H4:90 [binder, in Ceres.CeresRoundtrip]
H4:98 [binder, in Ceres.CeresRoundtrip]
H:11 [binder, in Ceres.CeresSerialize]
H:11 [binder, in Ceres.CeresRoundtrip]
H:12 [binder, in Ceres.CeresDeserialize]
H:131 [binder, in Ceres.CeresDeserialize]
H:135 [binder, in Ceres.CeresParserRoundtripProof]
H:136 [binder, in Ceres.CeresDeserialize]
H:14 [binder, in Ceres.CeresDeserialize]
H:143 [binder, in Ceres.CeresDeserialize]
H:15 [binder, in Ceres.CeresSerialize]
H:152 [binder, in Ceres.CeresDeserialize]
H:158 [binder, in Ceres.CeresParserRoundtripProof]
H:163 [binder, in Ceres.CeresDeserialize]
H:17 [binder, in Ceres.CeresRoundtrip]
H:182 [binder, in Ceres.CeresDeserialize]
H:189 [binder, in Ceres.CeresDeserialize]
H:195 [binder, in Ceres.CeresDeserialize]
H:20 [binder, in Ceres.CeresSerialize]
H:202 [binder, in Ceres.CeresDeserialize]
H:205 [binder, in Ceres.CeresDeserialize]
H:207 [binder, in Ceres.CeresParserRoundtripProof]
H:209 [binder, in Ceres.CeresDeserialize]
H:227 [binder, in Ceres.CeresParserRoundtripProof]
H:23 [binder, in Ceres.CeresRoundtrip]
H:233 [binder, in Ceres.CeresParserRoundtripProof]
H:235 [binder, in Ceres.CeresDeserialize]
H:26 [binder, in Ceres.CeresSerialize]
H:29 [binder, in Ceres.CeresRoundtrip]
H:34 [binder, in Ceres.CeresSerialize]
H:5 [binder, in Ceres.CeresSerialize]
I
If [constructor, in Tutorial]initial_state [definition, in Ceres.CeresParserInternal]
Integral [record, in Ceres.CeresSerialize]
Integral [inductive, in Ceres.CeresSerialize]
Integral_Z [instance, in Ceres.CeresSerialize]
Integral_N [instance, in Ceres.CeresSerialize]
Integral_nat [instance, in Ceres.CeresSerialize]
InvalidChar [constructor, in Ceres.CeresParserUtils]
InvalidStringChar [constructor, in Ceres.CeresParserUtils]
is_atom_char [definition, in Ceres.CeresParserUtils]
is_alphanum [definition, in Ceres.CeresString]
is_lower [definition, in Ceres.CeresString]
is_upper [definition, in Ceres.CeresString]
is_digit [definition, in Ceres.CeresString]
is_whitespace [definition, in Ceres.CeresString]
is_printable [definition, in Ceres.CeresString]
is_atom_app [lemma, in Ceres.CeresParserRoundtripProof]
is_atom_singleton [lemma, in Ceres.CeresParserRoundtripProof]
i':137 [binder, in Ceres.CeresParserRoundtripProof]
i':173 [binder, in Ceres.CeresParserRoundtripProof]
i':179 [binder, in Ceres.CeresParserRoundtripProof]
i':190 [binder, in Ceres.CeresParserRoundtripProof]
i':208 [binder, in Ceres.CeresParserRoundtripProof]
i':217 [binder, in Ceres.CeresParserRoundtripProof]
i':222 [binder, in Ceres.CeresParserRoundtripProof]
i':50 [binder, in Ceres.CeresParserInternal]
i:119 [binder, in Ceres.CeresParserRoundtripProof]
i:14 [binder, in Ceres.CeresParserInternal]
i:185 [binder, in Ceres.CeresParserRoundtripProof]
i:197 [binder, in Ceres.CeresParserRoundtripProof]
i:209 [binder, in Ceres.CeresParserRoundtripProof]
i:218 [binder, in Ceres.CeresParserRoundtripProof]
i:22 [binder, in Ceres.CeresParserInternal]
i:230 [binder, in Ceres.CeresParserRoundtripProof]
i:236 [binder, in Ceres.CeresParserRoundtripProof]
i:40 [binder, in Ceres.CeresParserInternal]
i:43 [binder, in Ceres.CeresParserInternal]
i:47 [binder, in Ceres.CeresParserInternal]
i:55 [binder, in Ceres.CeresParserInternal]
i:57 [binder, in Ceres.CeresParserInternal]
i:58 [binder, in Ceres.CeresParserInternal]
i:59 [binder, in Ceres.CeresParserInternal]
i:60 [binder, in Ceres.CeresParserInternal]
L
leb_ascii [definition, in Ceres.CeresString]List [constructor, in Ceres.CeresS]
list_sexp_tokens [abbreviation, in Ceres.CeresParserRoundtrip]
list_tokens_cons [constructor, in Ceres.CeresParserRoundtrip]
list_tokens_nil [constructor, in Ceres.CeresParserRoundtrip]
list_tokens [inductive, in Ceres.CeresParserRoundtrip]
list_sexp_tokens_app [lemma, in Ceres.CeresParserRoundtripProof]
list_sexp_tokens_singleton [lemma, in Ceres.CeresParserRoundtripProof]
List_Exists_impl [lemma, in Ceres.CeresRoundtrip]
loc [definition, in Ceres.CeresDeserialize]
loc [definition, in Ceres.CeresParserUtils]
l:105 [binder, in Ceres.CeresRoundtrip]
l:116 [binder, in Ceres.CeresRoundtrip]
l:14 [binder, in Ceres.CeresRoundtrip]
l:151 [binder, in Ceres.CeresRoundtrip]
l:164 [binder, in Ceres.CeresRoundtrip]
l:196 [binder, in Ceres.CeresDeserialize]
l:20 [binder, in Ceres.CeresRoundtrip]
l:211 [binder, in Ceres.CeresDeserialize]
l:216 [binder, in Ceres.CeresDeserialize]
l:217 [binder, in Ceres.CeresDeserialize]
l:220 [binder, in Ceres.CeresDeserialize]
l:223 [binder, in Ceres.CeresDeserialize]
l:230 [binder, in Ceres.CeresDeserialize]
l:236 [binder, in Ceres.CeresDeserialize]
l:26 [binder, in Ceres.CeresDeserialize]
l:36 [binder, in Ceres.CeresDeserialize]
l:44 [binder, in Ceres.CeresDeserialize]
l:47 [binder, in Ceres.CeresRoundtrip]
l:54 [binder, in Ceres.CeresDeserialize]
l:6 [binder, in Tutorial]
l:65 [binder, in Ceres.CeresDeserialize]
l:73 [binder, in Ceres.CeresRoundtrip]
M
map_sum [definition, in Ceres.CeresUtils]map_sexp_ [definition, in Ceres.CeresS]
message [inductive, in Ceres.CeresDeserialize]
MkUnconsFields [constructor, in Ceres.CeresRoundtrip]
MkUnnilFields [constructor, in Ceres.CeresRoundtrip]
mk_error:66 [binder, in Ceres.CeresDeserialize]
mk_error:55 [binder, in Ceres.CeresDeserialize]
more_ok_cons [lemma, in Ceres.CeresParserRoundtrip]
more_ok_nil_inv [lemma, in Ceres.CeresParserRoundtrip]
more_ok_true [constructor, in Ceres.CeresParserRoundtrip]
more_ok_false [constructor, in Ceres.CeresParserRoundtrip]
more_ok [inductive, in Ceres.CeresParserRoundtrip]
more_ok_atom [lemma, in Ceres.CeresParserRoundtripProof]
more_ok_atom_inv [lemma, in Ceres.CeresParserRoundtripProof]
more_ok_str_token [lemma, in Ceres.CeresParserRoundtripProof]
more':115 [binder, in Ceres.CeresParserRoundtripProof]
more:104 [binder, in Ceres.CeresParserRoundtripProof]
more:114 [binder, in Ceres.CeresParserRoundtripProof]
more:122 [binder, in Ceres.CeresParserRoundtripProof]
more:125 [binder, in Ceres.CeresParserRoundtripProof]
more:130 [binder, in Ceres.CeresParserRoundtripProof]
more:14 [binder, in Ceres.CeresParserRoundtrip]
more:144 [binder, in Ceres.CeresParserRoundtripProof]
more:15 [binder, in Ceres.CeresParserRoundtrip]
more:15 [binder, in Ceres.CeresParserRoundtripProof]
more:153 [binder, in Ceres.CeresParserRoundtripProof]
more:16 [binder, in Ceres.CeresParserRoundtrip]
more:16 [binder, in Ceres.CeresParserRoundtripProof]
more:162 [binder, in Ceres.CeresParserRoundtripProof]
more:177 [binder, in Ceres.CeresParserRoundtripProof]
more:180 [binder, in Ceres.CeresParserRoundtripProof]
more:186 [binder, in Ceres.CeresParserRoundtripProof]
more:19 [binder, in Ceres.CeresParserRoundtripProof]
more:191 [binder, in Ceres.CeresParserRoundtripProof]
more:202 [binder, in Ceres.CeresParserRoundtripProof]
more:21 [binder, in Ceres.CeresParserRoundtrip]
more:211 [binder, in Ceres.CeresParserRoundtripProof]
more:225 [binder, in Ceres.CeresParserRoundtripProof]
more:25 [binder, in Ceres.CeresParserRoundtripProof]
more:28 [binder, in Ceres.CeresParserRoundtripProof]
more:32 [binder, in Ceres.CeresParserRoundtripProof]
more:46 [binder, in Ceres.CeresParserRoundtrip]
more:47 [binder, in Ceres.CeresParserRoundtrip]
more:69 [binder, in Ceres.CeresParserRoundtripProof]
MsgApp [constructor, in Ceres.CeresDeserialize]
MsgSexp [constructor, in Ceres.CeresDeserialize]
MsgStr [constructor, in Ceres.CeresDeserialize]
msg:4 [binder, in Ceres.CeresDeserialize]
msg:41 [binder, in Ceres.CeresDeserialize]
msg:47 [binder, in Ceres.CeresDeserialize]
msg:58 [binder, in Ceres.CeresDeserialize]
msg:70 [binder, in Ceres.CeresDeserialize]
m:112 [binder, in Ceres.CeresRoundtrip]
m:17 [binder, in Ceres.CeresDeserialize]
m:171 [binder, in Ceres.CeresDeserialize]
m:175 [binder, in Ceres.CeresDeserialize]
m:181 [binder, in Ceres.CeresDeserialize]
m:188 [binder, in Ceres.CeresDeserialize]
m:63 [binder, in Ceres.CeresDeserialize]
N
neqb_neq_ascii [lemma, in Ceres.CeresString]newline [abbreviation, in Ceres.CeresString]
new_sexp [definition, in Ceres.CeresParserInternal]
new_sexp_Str_sound [lemma, in Ceres.CeresParserRoundtripProof]
new_sexp_List_sound [lemma, in Ceres.CeresParserRoundtripProof]
new_sexp_Atom_sound [lemma, in Ceres.CeresParserRoundtripProof]
next [definition, in Ceres.CeresParserInternal]
next_comment [definition, in Ceres.CeresParserInternal]
next_str [definition, in Ceres.CeresParserInternal]
next_sound [lemma, in Ceres.CeresParserRoundtripProof]
next_comment_sound [lemma, in Ceres.CeresParserRoundtripProof]
next_str_sound [lemma, in Ceres.CeresParserRoundtripProof]
next_sound' [lemma, in Ceres.CeresParserRoundtripProof]
next' [definition, in Ceres.CeresParserInternal]
NoToken [constructor, in Ceres.CeresParserInternal]
not_string_elem_singleton [lemma, in Ceres.CeresString]
not_string_elem_head [lemma, in Ceres.CeresString]
not_string_elem_app [lemma, in Ceres.CeresString]
no_newline [definition, in Ceres.CeresParserRoundtripProof]
Num [constructor, in Ceres.CeresS]
Number [constructor, in Tutorial]
n0:85 [binder, in Ceres.CeresString]
n1:86 [binder, in Ceres.CeresString]
n2:87 [binder, in Ceres.CeresString]
n:101 [binder, in Ceres.CeresRoundtrip]
n:109 [binder, in Ceres.CeresString]
n:110 [binder, in Ceres.CeresString]
n:111 [binder, in Ceres.CeresString]
n:111 [binder, in Ceres.CeresRoundtrip]
n:150 [binder, in Ceres.CeresRoundtrip]
n:163 [binder, in Ceres.CeresRoundtrip]
n:170 [binder, in Ceres.CeresDeserialize]
n:18 [binder, in Ceres.CeresDeserialize]
n:180 [binder, in Ceres.CeresDeserialize]
n:199 [binder, in Ceres.CeresDeserialize]
n:200 [binder, in Ceres.CeresDeserialize]
n:22 [binder, in Ceres.CeresS]
n:229 [binder, in Ceres.CeresDeserialize]
n:49 [binder, in Ceres.CeresDeserialize]
n:53 [binder, in Ceres.CeresDeserialize]
n:62 [binder, in Ceres.CeresDeserialize]
n:83 [binder, in Ceres.CeresString]
n:84 [binder, in Ceres.CeresString]
n:93 [binder, in Ceres.CeresString]
n:96 [binder, in Ceres.CeresString]
O
oa:16 [binder, in Ceres.CeresSerialize]on_right [definition, in Ceres.CeresParserRoundtrip]
Open [constructor, in Ceres.CeresParserInternal]
P
ParseError [constructor, in Ceres.CeresDeserialize]parser_state [definition, in Ceres.CeresParserInternal]
parser_cur_token [projection, in Ceres.CeresParserInternal]
parser_stack [projection, in Ceres.CeresParserInternal]
parser_done [projection, in Ceres.CeresParserInternal]
parser_state_ [record, in Ceres.CeresParserInternal]
parser_state_empty [lemma, in Ceres.CeresParserRoundtripProof]
parser_state_string_mk [constructor, in Ceres.CeresParserRoundtripProof]
parser_state_string [inductive, in Ceres.CeresParserRoundtripProof]
parser_state_string_map [lemma, in Ceres.CeresParserRoundtripProof]
parser_state_string_mk_ [constructor, in Ceres.CeresParserRoundtripProof]
parser_state_string_ [inductive, in Ceres.CeresParserRoundtripProof]
parse_sexps_ [definition, in Ceres.CeresParserInternal]
PARSE_SEXPS_SOUND [definition, in Ceres.CeresParserRoundtrip]
parse_sexp [definition, in Ceres.CeresParser]
parse_sexps [definition, in Ceres.CeresParser]
parse_sexps_sound [lemma, in Ceres.CeresParserRoundtripProof]
partial_token [inductive, in Ceres.CeresParserInternal]
partial_token_string_Comment [constructor, in Ceres.CeresParserRoundtripProof]
partial_token_string_StrToken [constructor, in Ceres.CeresParserRoundtripProof]
partial_token_string_SimpleToken [constructor, in Ceres.CeresParserRoundtripProof]
partial_token_string_NoToken [constructor, in Ceres.CeresParserRoundtripProof]
partial_token_string [inductive, in Ceres.CeresParserRoundtripProof]
pa:103 [binder, in Ceres.CeresDeserialize]
pa:110 [binder, in Ceres.CeresRoundtrip]
pa:118 [binder, in Ceres.CeresDeserialize]
pa:227 [binder, in Ceres.CeresDeserialize]
pa:61 [binder, in Ceres.CeresDeserialize]
pa:76 [binder, in Ceres.CeresDeserialize]
pa:82 [binder, in Ceres.CeresDeserialize]
pa:91 [binder, in Ceres.CeresDeserialize]
pb:104 [binder, in Ceres.CeresDeserialize]
pb:119 [binder, in Ceres.CeresDeserialize]
pb:83 [binder, in Ceres.CeresDeserialize]
pb:92 [binder, in Ceres.CeresDeserialize]
pc:105 [binder, in Ceres.CeresDeserialize]
pc:120 [binder, in Ceres.CeresDeserialize]
pc:93 [binder, in Ceres.CeresDeserialize]
pd:106 [binder, in Ceres.CeresDeserialize]
pd:121 [binder, in Ceres.CeresDeserialize]
pe:122 [binder, in Ceres.CeresDeserialize]
Plus [constructor, in Tutorial]
pretty_error [definition, in Ceres.CeresParserUtils]
pretty_loc [definition, in Ceres.CeresParserUtils]
p0:23 [binder, in Ceres.CeresParserInternal]
p1:199 [binder, in Ceres.CeresParserRoundtripProof]
p:1 [binder, in Ceres.CeresParserUtils]
p:160 [binder, in Ceres.CeresParserRoundtripProof]
p:175 [binder, in Ceres.CeresParserRoundtripProof]
p:188 [binder, in Ceres.CeresParserRoundtripProof]
p:198 [binder, in Ceres.CeresParserRoundtripProof]
p:220 [binder, in Ceres.CeresParserRoundtripProof]
p:231 [binder, in Ceres.CeresParserRoundtripProof]
p:237 [binder, in Ceres.CeresParserRoundtripProof]
p:26 [binder, in Ceres.CeresParserInternal]
p:34 [binder, in Ceres.CeresParserInternal]
p:38 [binder, in Ceres.CeresParserRoundtripProof]
p:41 [binder, in Ceres.CeresParserInternal]
p:47 [binder, in Ceres.CeresParserRoundtripProof]
p:48 [binder, in Ceres.CeresParserInternal]
p:50 [binder, in Ceres.CeresDeserialize]
p:56 [binder, in Ceres.CeresParserInternal]
p:56 [binder, in Ceres.CeresParserRoundtripProof]
p:61 [binder, in Ceres.CeresParserInternal]
P:61 [binder, in Ceres.CeresRoundtrip]
p:62 [binder, in Ceres.CeresRoundtrip]
p:63 [binder, in Ceres.CeresRoundtrip]
P:65 [binder, in Ceres.CeresS]
P:65 [binder, in Ceres.CeresRoundtrip]
P:69 [binder, in Ceres.CeresS]
P:74 [binder, in Ceres.CeresParserRoundtrip]
p:76 [binder, in Ceres.CeresRoundtrip]
p:77 [binder, in Ceres.CeresRoundtrip]
p:96 [binder, in Ceres.CeresParserRoundtripProof]
p:99 [binder, in Ceres.CeresParserRoundtripProof]
Q
Q:66 [binder, in Ceres.CeresRoundtrip]R
Raw [constructor, in Ceres.CeresS]raw_or_num [definition, in Ceres.CeresParserInternal]
reflect_eq_false [constructor, in Ceres.CeresString]
reflect_eq_true [constructor, in Ceres.CeresString]
reflect_eq [inductive, in Ceres.CeresString]
ret:31 [binder, in Ceres.CeresParserInternal]
r:100 [binder, in Ceres.CeresRoundtrip]
R:101 [binder, in Ceres.CeresDeserialize]
R:116 [binder, in Ceres.CeresDeserialize]
R:129 [binder, in Ceres.CeresDeserialize]
R:134 [binder, in Ceres.CeresDeserialize]
R:141 [binder, in Ceres.CeresDeserialize]
R:150 [binder, in Ceres.CeresDeserialize]
R:161 [binder, in Ceres.CeresDeserialize]
R:169 [binder, in Ceres.CeresDeserialize]
R:174 [binder, in Ceres.CeresDeserialize]
r:176 [binder, in Ceres.CeresDeserialize]
R:179 [binder, in Ceres.CeresDeserialize]
R:187 [binder, in Ceres.CeresDeserialize]
r:35 [binder, in Ceres.CeresParserInternal]
R:51 [binder, in Ceres.CeresDeserialize]
r:51 [binder, in Ceres.CeresParserInternal]
r:52 [binder, in Ceres.CeresDeserialize]
r:60 [binder, in Ceres.CeresString]
R:71 [binder, in Ceres.CeresDeserialize]
r:72 [binder, in Ceres.CeresDeserialize]
R:74 [binder, in Ceres.CeresDeserialize]
R:80 [binder, in Ceres.CeresDeserialize]
R:89 [binder, in Ceres.CeresDeserialize]
R:99 [binder, in Ceres.CeresRoundtrip]
S
SemiIntegral [record, in Ceres.CeresDeserialize]SemiIntegral [inductive, in Ceres.CeresDeserialize]
SemiIntegral_nat [instance, in Ceres.CeresDeserialize]
SemiIntegral_N [instance, in Ceres.CeresDeserialize]
SemiIntegral_Z [instance, in Ceres.CeresDeserialize]
Serialize [record, in Ceres.CeresSerialize]
Serialize [inductive, in Ceres.CeresSerialize]
Serialize_sexp [instance, in Ceres.CeresSerialize]
Serialize_list [instance, in Ceres.CeresSerialize]
Serialize_string [instance, in Ceres.CeresSerialize]
Serialize_ascii [instance, in Ceres.CeresSerialize]
Serialize_unit [instance, in Ceres.CeresSerialize]
Serialize_Empty_set [instance, in Ceres.CeresSerialize]
Serialize_product [instance, in Ceres.CeresSerialize]
Serialize_sum [instance, in Ceres.CeresSerialize]
Serialize_option [instance, in Ceres.CeresSerialize]
Serialize_bool [instance, in Ceres.CeresSerialize]
Serialize_Integral [instance, in Ceres.CeresSerialize]
Serialize_t [instance, in Tutorial]
ser:2 [binder, in Ceres.CeresRoundtrip]
ser:6 [binder, in Ceres.CeresRoundtrip]
set_cur_token [definition, in Ceres.CeresParserInternal]
sexp [abbreviation, in Ceres.CeresS]
sexp_tokens_List [constructor, in Ceres.CeresParserRoundtrip]
sexp_tokens_Atom [constructor, in Ceres.CeresParserRoundtrip]
sexp_tokens [inductive, in Ceres.CeresParserRoundtrip]
sexp__ind [lemma, in Ceres.CeresS]
sexp_of_atoms [definition, in Ceres.CeresS]
sexp_ [inductive, in Ceres.CeresS]
SimpleToken [constructor, in Ceres.CeresParserInternal]
Sound [definition, in Ceres.CeresRoundtrip]
SoundClass [record, in Ceres.CeresRoundtrip]
SoundClass [inductive, in Ceres.CeresRoundtrip]
SoundClass_ascii [instance, in Ceres.CeresRoundtrip]
SoundClass_string [instance, in Ceres.CeresRoundtrip]
SoundClass_list [instance, in Ceres.CeresRoundtrip]
SoundClass_prod [instance, in Ceres.CeresRoundtrip]
SoundClass_sum [instance, in Ceres.CeresRoundtrip]
SoundClass_option [instance, in Ceres.CeresRoundtrip]
SoundClass_bool [instance, in Ceres.CeresRoundtrip]
SoundClass_Integral [instance, in Ceres.CeresRoundtrip]
SoundIntegral [record, in Ceres.CeresRoundtrip]
SoundIntegral [inductive, in Ceres.CeresRoundtrip]
sound_class_list [lemma, in Ceres.CeresRoundtrip]
sound_bind_field [lemma, in Ceres.CeresRoundtrip]
sound_ret_field [lemma, in Ceres.CeresRoundtrip]
sound_match_con [lemma, in Ceres.CeresRoundtrip]
sound__con [lemma, in Ceres.CeresRoundtrip]
Sound_nat [instance, in Ceres.CeresRoundtrip]
Sound_N [instance, in Ceres.CeresRoundtrip]
Sound_Z [instance, in Ceres.CeresRoundtrip]
sound_integral [projection, in Ceres.CeresRoundtrip]
sound_integral [constructor, in Ceres.CeresRoundtrip]
sound_class [projection, in Ceres.CeresRoundtrip]
sound_class [constructor, in Ceres.CeresRoundtrip]
stack_end_inv [lemma, in Ceres.CeresParserRoundtripProof]
stack_end_cons_Open [lemma, in Ceres.CeresParserRoundtripProof]
stack_end_cons [lemma, in Ceres.CeresParserRoundtripProof]
stack_end_nonempty [constructor, in Ceres.CeresParserRoundtripProof]
stack_end_nil [constructor, in Ceres.CeresParserRoundtripProof]
stack_end [inductive, in Ceres.CeresParserRoundtripProof]
stack_end_last_cons [constructor, in Ceres.CeresParserRoundtripProof]
stack_end_last_last [constructor, in Ceres.CeresParserRoundtripProof]
stack_end_last [inductive, in Ceres.CeresParserRoundtripProof]
stack_tokens_sexp [constructor, in Ceres.CeresParserRoundtripProof]
stack_tokens_open [constructor, in Ceres.CeresParserRoundtripProof]
stack_tokens_nil [constructor, in Ceres.CeresParserRoundtripProof]
stack_tokens [inductive, in Ceres.CeresParserRoundtripProof]
Str [constructor, in Ceres.CeresS]
string_string [definition, in Ceres.CeresParserRoundtrip]
string_of_bool [definition, in Ceres.CeresString]
string_of_N [definition, in Ceres.CeresString]
string_of_Z [definition, in Ceres.CeresString]
string_of_nat [definition, in Ceres.CeresString]
string_app_nil_r [lemma, in Ceres.CeresString]
string_reverse [definition, in Ceres.CeresString]
string_forall [definition, in Ceres.CeresString]
string_elem [definition, in Ceres.CeresString]
string_reverse_cons' [lemma, in Ceres.CeresParserRoundtripProof]
string_reverse_cons [lemma, in Ceres.CeresParserRoundtripProof]
string_app_assoc [lemma, in Ceres.CeresParserRoundtripProof]
string_of_sexp [definition, in Ceres.CeresFormat]
string_of_atom [definition, in Ceres.CeresFormat]
string_A:9 [binder, in Ceres.CeresFormat]
string_of_sexp_ [definition, in Ceres.CeresFormat]
StrToken [constructor, in Ceres.CeresParserInternal]
str_token_string_regular [lemma, in Ceres.CeresParserRoundtripProof]
str_token_string_escape [lemma, in Ceres.CeresParserRoundtripProof]
str_token_string_dquote [lemma, in Ceres.CeresParserRoundtripProof]
str_token_string_backslash [lemma, in Ceres.CeresParserRoundtripProof]
str_token_string_newline [lemma, in Ceres.CeresParserRoundtripProof]
str_token_string_new [lemma, in Ceres.CeresParserRoundtripProof]
str_token_string_EscNone [constructor, in Ceres.CeresParserRoundtripProof]
str_token_string_EscBackslash [constructor, in Ceres.CeresParserRoundtripProof]
str_token_string [inductive, in Ceres.CeresParserRoundtripProof]
subst_sexp_ [definition, in Ceres.CeresS]
symbol [inductive, in Ceres.CeresParserInternal]
s_str:34 [binder, in Ceres.CeresParserRoundtripProof]
s_com:30 [binder, in Ceres.CeresParserRoundtripProof]
s':102 [binder, in Ceres.CeresParserRoundtripProof]
s':115 [binder, in Ceres.CeresString]
s':132 [binder, in Ceres.CeresParserRoundtripProof]
s':14 [binder, in Ceres.CeresParserRoundtripProof]
s':156 [binder, in Ceres.CeresParserRoundtripProof]
s':196 [binder, in Ceres.CeresParserRoundtripProof]
s':205 [binder, in Ceres.CeresParserRoundtripProof]
s':98 [binder, in Ceres.CeresParserRoundtripProof]
s0':117 [binder, in Ceres.CeresParserRoundtripProof]
s0:107 [binder, in Ceres.CeresParserRoundtripProof]
s0:116 [binder, in Ceres.CeresParserRoundtripProof]
s0:123 [binder, in Ceres.CeresParserRoundtripProof]
s0:129 [binder, in Ceres.CeresParserRoundtripProof]
s0:140 [binder, in Ceres.CeresParserRoundtripProof]
s0:154 [binder, in Ceres.CeresParserRoundtripProof]
s0:161 [binder, in Ceres.CeresParserRoundtripProof]
s0:176 [binder, in Ceres.CeresParserRoundtripProof]
s0:187 [binder, in Ceres.CeresParserRoundtripProof]
s0:19 [binder, in Ceres.CeresParserRoundtrip]
s0:203 [binder, in Ceres.CeresParserRoundtripProof]
s0:212 [binder, in Ceres.CeresParserRoundtripProof]
s0:226 [binder, in Ceres.CeresParserRoundtripProof]
s0:238 [binder, in Ceres.CeresParserRoundtripProof]
s0:32 [binder, in Ceres.CeresParserRoundtrip]
s0:6 [binder, in Ceres.CeresFormat]
s0:78 [binder, in Ceres.CeresParserRoundtripProof]
s0:9 [binder, in Ceres.CeresParserRoundtripProof]
s1':134 [binder, in Ceres.CeresParserRoundtripProof]
s1:10 [binder, in Ceres.CeresParserRoundtripProof]
s1:124 [binder, in Ceres.CeresParserRoundtripProof]
s1:20 [binder, in Ceres.CeresParserRoundtrip]
s1:215 [binder, in Ceres.CeresParserRoundtripProof]
s1:24 [binder, in Ceres.CeresParserRoundtripProof]
s1:29 [binder, in Ceres.CeresParserRoundtrip]
s1:33 [binder, in Ceres.CeresParserRoundtrip]
s1:41 [binder, in Ceres.CeresString]
s1:42 [binder, in Ceres.CeresS]
s1:46 [binder, in Ceres.CeresString]
s1:48 [binder, in Ceres.CeresString]
s1:50 [binder, in Ceres.CeresString]
s1:66 [binder, in Ceres.CeresString]
s1:76 [binder, in Ceres.CeresS]
s1:78 [binder, in Ceres.CeresS]
s1:79 [binder, in Ceres.CeresParserRoundtripProof]
s1:80 [binder, in Ceres.CeresS]
s2:11 [binder, in Ceres.CeresParserRoundtripProof]
s2:42 [binder, in Ceres.CeresString]
s2:43 [binder, in Ceres.CeresS]
s2:47 [binder, in Ceres.CeresString]
s2:49 [binder, in Ceres.CeresString]
s2:51 [binder, in Ceres.CeresString]
s2:67 [binder, in Ceres.CeresString]
s2:77 [binder, in Ceres.CeresS]
s2:79 [binder, in Ceres.CeresS]
s2:80 [binder, in Ceres.CeresParserRoundtripProof]
s2:81 [binder, in Ceres.CeresS]
s:1 [binder, in Ceres.CeresParser]
s:1 [binder, in Ceres.CeresParserRoundtripProof]
s:101 [binder, in Ceres.CeresString]
s:103 [binder, in Ceres.CeresParserRoundtripProof]
s:107 [binder, in Ceres.CeresString]
s:114 [binder, in Ceres.CeresString]
s:117 [binder, in Ceres.CeresString]
s:118 [binder, in Ceres.CeresString]
s:126 [binder, in Ceres.CeresParserRoundtripProof]
s:13 [binder, in Ceres.CeresParserRoundtrip]
s:13 [binder, in Ceres.CeresParserRoundtripProof]
s:15 [binder, in Ceres.CeresDeserialize]
s:18 [binder, in Ceres.CeresParserInternal]
s:18 [binder, in Ceres.CeresParserRoundtrip]
s:18 [binder, in Ceres.CeresParserRoundtripProof]
s:182 [binder, in Ceres.CeresParserRoundtripProof]
s:192 [binder, in Ceres.CeresParserRoundtripProof]
s:195 [binder, in Ceres.CeresParserRoundtripProof]
s:2 [binder, in Ceres.CeresParser]
s:21 [binder, in Ceres.CeresParserRoundtripProof]
s:219 [binder, in Ceres.CeresParserRoundtripProof]
s:23 [binder, in Ceres.CeresS]
s:23 [binder, in Ceres.CeresParserRoundtripProof]
s:232 [binder, in Ceres.CeresParserRoundtripProof]
s:239 [binder, in Ceres.CeresParserRoundtripProof]
s:24 [binder, in Ceres.CeresS]
s:25 [binder, in Ceres.CeresParserRoundtrip]
s:26 [binder, in Ceres.CeresParserRoundtripProof]
s:27 [binder, in Ceres.CeresParserRoundtrip]
s:29 [binder, in Ceres.CeresParserRoundtripProof]
s:3 [binder, in Ceres.CeresParserRoundtrip]
s:30 [binder, in Ceres.CeresParserRoundtrip]
s:32 [binder, in Ceres.CeresSerialize]
s:33 [binder, in Ceres.CeresParserRoundtripProof]
s:34 [binder, in Ceres.CeresParserRoundtrip]
s:36 [binder, in Ceres.CeresParserInternal]
s:37 [binder, in Ceres.CeresParserRoundtrip]
s:4 [binder, in Ceres.CeresParserRoundtrip]
s:40 [binder, in Ceres.CeresParserRoundtrip]
s:43 [binder, in Ceres.CeresParserRoundtrip]
s:45 [binder, in Ceres.CeresParserInternal]
s:45 [binder, in Ceres.CeresParserRoundtrip]
s:46 [binder, in Ceres.CeresParserInternal]
s:49 [binder, in Ceres.CeresParserRoundtrip]
s:5 [binder, in Ceres.CeresParserRoundtrip]
s:52 [binder, in Ceres.CeresParserInternal]
s:53 [binder, in Ceres.CeresString]
s:57 [binder, in Ceres.CeresString]
s:61 [binder, in Ceres.CeresParserRoundtrip]
s:61 [binder, in Ceres.CeresString]
s:62 [binder, in Ceres.CeresParserInternal]
s:62 [binder, in Ceres.CeresParserRoundtrip]
s:62 [binder, in Ceres.CeresParserRoundtripProof]
s:64 [binder, in Ceres.CeresParserRoundtrip]
s:64 [binder, in Ceres.CeresString]
s:64 [binder, in Ceres.CeresParserRoundtripProof]
s:70 [binder, in Ceres.CeresString]
s:72 [binder, in Ceres.CeresS]
s:72 [binder, in Ceres.CeresParserRoundtripProof]
s:73 [binder, in Ceres.CeresParserRoundtripProof]
s:74 [binder, in Ceres.CeresParserRoundtripProof]
s:75 [binder, in Ceres.CeresParserRoundtripProof]
s:76 [binder, in Ceres.CeresParserRoundtrip]
s:77 [binder, in Ceres.CeresParserRoundtripProof]
s:8 [binder, in Ceres.CeresParserRoundtrip]
s:82 [binder, in Ceres.CeresParserRoundtripProof]
s:84 [binder, in Ceres.CeresParserRoundtripProof]
s:86 [binder, in Ceres.CeresParserRoundtripProof]
s:88 [binder, in Ceres.CeresParserRoundtripProof]
s:89 [binder, in Ceres.CeresString]
s:9 [binder, in Ceres.CeresParserRoundtrip]
s:90 [binder, in Ceres.CeresParserRoundtripProof]
s:93 [binder, in Ceres.CeresParserRoundtripProof]
s:94 [binder, in Ceres.CeresString]
s:97 [binder, in Ceres.CeresParserRoundtripProof]
T
t [inductive, in Tutorial]tks:52 [binder, in Ceres.CeresParserRoundtrip]
Token [module, in Ceres.CeresParserRoundtrip]
token_string_comment [constructor, in Ceres.CeresParserRoundtrip]
token_string_spaces [constructor, in Ceres.CeresParserRoundtrip]
token_string_string [constructor, in Ceres.CeresParserRoundtrip]
token_string_atom [constructor, in Ceres.CeresParserRoundtrip]
token_string_close [constructor, in Ceres.CeresParserRoundtrip]
token_string_open [constructor, in Ceres.CeresParserRoundtrip]
token_string_nil [constructor, in Ceres.CeresParserRoundtrip]
token_string [inductive, in Ceres.CeresParserRoundtrip]
token_string_spaces_app [lemma, in Ceres.CeresParserRoundtripProof]
token_string_string_snoc [lemma, in Ceres.CeresParserRoundtripProof]
token_string_comment_snoc [lemma, in Ceres.CeresParserRoundtripProof]
token_string_newline_snoc [lemma, in Ceres.CeresParserRoundtripProof]
token_string_atom_snoc [lemma, in Ceres.CeresParserRoundtripProof]
token_string_close_snoc [lemma, in Ceres.CeresParserRoundtripProof]
token_string_open_snoc [lemma, in Ceres.CeresParserRoundtripProof]
Token.Atom [constructor, in Ceres.CeresParserRoundtrip]
Token.Close [constructor, in Ceres.CeresParserRoundtrip]
Token.Open [constructor, in Ceres.CeresParserRoundtrip]
Token.Str [constructor, in Ceres.CeresParserRoundtrip]
Token.t [inductive, in Ceres.CeresParserRoundtrip]
tok':29 [binder, in Ceres.CeresParserInternal]
tok:100 [binder, in Ceres.CeresParserRoundtripProof]
tok:155 [binder, in Ceres.CeresParserRoundtripProof]
tok:204 [binder, in Ceres.CeresParserRoundtripProof]
tok:24 [binder, in Ceres.CeresParserInternal]
tok:66 [binder, in Ceres.CeresParserRoundtripProof]
tok:70 [binder, in Ceres.CeresParserRoundtripProof]
tok:83 [binder, in Ceres.CeresParserRoundtripProof]
tok:85 [binder, in Ceres.CeresParserRoundtripProof]
tok:87 [binder, in Ceres.CeresParserRoundtripProof]
tok:89 [binder, in Ceres.CeresParserRoundtripProof]
tok:92 [binder, in Ceres.CeresParserRoundtripProof]
to_Z [projection, in Ceres.CeresSerialize]
to_Z [constructor, in Ceres.CeresSerialize]
to_string [definition, in Ceres.CeresSerialize]
to_sexp [projection, in Ceres.CeresSerialize]
to_sexp [constructor, in Ceres.CeresSerialize]
ts00:110 [binder, in Ceres.CeresParserRoundtripProof]
ts00:141 [binder, in Ceres.CeresParserRoundtripProof]
ts00:165 [binder, in Ceres.CeresParserRoundtripProof]
ts01:111 [binder, in Ceres.CeresParserRoundtripProof]
ts01:142 [binder, in Ceres.CeresParserRoundtripProof]
ts01:166 [binder, in Ceres.CeresParserRoundtripProof]
ts02:143 [binder, in Ceres.CeresParserRoundtripProof]
ts02:167 [binder, in Ceres.CeresParserRoundtripProof]
ts0:44 [binder, in Ceres.CeresParserRoundtripProof]
ts1:7 [binder, in Ceres.CeresParserRoundtripProof]
ts2:8 [binder, in Ceres.CeresParserRoundtripProof]
ts:118 [binder, in Ceres.CeresParserRoundtripProof]
ts:17 [binder, in Ceres.CeresParserRoundtripProof]
ts:181 [binder, in Ceres.CeresParserRoundtripProof]
ts:20 [binder, in Ceres.CeresParserRoundtripProof]
ts:22 [binder, in Ceres.CeresParserRoundtripProof]
ts:229 [binder, in Ceres.CeresParserRoundtripProof]
ts:235 [binder, in Ceres.CeresParserRoundtripProof]
ts:24 [binder, in Ceres.CeresParserRoundtrip]
ts:241 [binder, in Ceres.CeresParserRoundtripProof]
ts:26 [binder, in Ceres.CeresParserRoundtrip]
ts:27 [binder, in Ceres.CeresParserRoundtripProof]
ts:28 [binder, in Ceres.CeresParserRoundtrip]
ts:31 [binder, in Ceres.CeresParserRoundtrip]
ts:31 [binder, in Ceres.CeresParserRoundtripProof]
ts:35 [binder, in Ceres.CeresParserRoundtrip]
ts:35 [binder, in Ceres.CeresParserRoundtripProof]
ts:38 [binder, in Ceres.CeresParserRoundtrip]
ts:4 [binder, in Ceres.CeresParserRoundtripProof]
ts:40 [binder, in Ceres.CeresParserRoundtripProof]
ts:43 [binder, in Ceres.CeresParserRoundtripProof]
ts:70 [binder, in Ceres.CeresParserRoundtrip]
ts:79 [binder, in Ceres.CeresParserRoundtrip]
Tutorial [library]
tyname:23 [binder, in Ceres.CeresDeserialize]
tyname:3 [binder, in Ceres.CeresDeserialize]
tyname:32 [binder, in Ceres.CeresDeserialize]
tyname:44 [binder, in Ceres.CeresRoundtrip]
tyname:70 [binder, in Ceres.CeresRoundtrip]
type_error [definition, in Ceres.CeresDeserialize]
T:12 [binder, in Ceres.CeresParserInternal]
T:16 [binder, in Ceres.CeresParserInternal]
T:184 [binder, in Ceres.CeresParserRoundtripProof]
t:20 [binder, in Ceres.CeresParserInternal]
T:39 [binder, in Ceres.CeresParserInternal]
t:68 [binder, in Ceres.CeresParserRoundtrip]
T:7 [binder, in Ceres.CeresParserInternal]
U
UnconsFields [inductive, in Ceres.CeresRoundtrip]unescape_string [definition, in Ceres.CeresString]
UnknownEscape [constructor, in Ceres.CeresParserUtils]
UnmatchedClose [constructor, in Ceres.CeresParserUtils]
UnmatchedOpen [constructor, in Ceres.CeresParserUtils]
UnnilFields [inductive, in Ceres.CeresRoundtrip]
UnterminatedString [constructor, in Ceres.CeresParserUtils]
us:39 [binder, in Ceres.CeresParserRoundtripProof]
us:42 [binder, in Ceres.CeresParserRoundtripProof]
us:49 [binder, in Ceres.CeresParserRoundtripProof]
us:52 [binder, in Ceres.CeresParserRoundtripProof]
us:55 [binder, in Ceres.CeresParserRoundtripProof]
us:57 [binder, in Ceres.CeresParserRoundtripProof]
us:59 [binder, in Ceres.CeresParserRoundtripProof]
u:106 [binder, in Ceres.CeresParserRoundtripProof]
u:113 [binder, in Ceres.CeresParserRoundtripProof]
u:128 [binder, in Ceres.CeresParserRoundtripProof]
U:13 [binder, in Ceres.CeresParserInternal]
u:139 [binder, in Ceres.CeresParserRoundtripProof]
u:15 [binder, in Ceres.CeresParserInternal]
u:152 [binder, in Ceres.CeresParserRoundtripProof]
u:163 [binder, in Ceres.CeresParserRoundtripProof]
u:178 [binder, in Ceres.CeresParserRoundtripProof]
u:224 [binder, in Ceres.CeresParserRoundtripProof]
u:48 [binder, in Ceres.CeresParserRoundtripProof]
u:54 [binder, in Ceres.CeresParserRoundtripProof]
u:58 [binder, in Ceres.CeresParserRoundtripProof]
V
v:29 [binder, in Ceres.CeresSerialize]v:53 [binder, in Ceres.CeresParserRoundtripProof]
W
whitespaces [definition, in Ceres.CeresParserRoundtrip]whitespace_no_atom [lemma, in Ceres.CeresParserRoundtripProof]
ws:36 [binder, in Ceres.CeresParserRoundtrip]
X
xs':57 [binder, in Ceres.CeresS]xs:12 [binder, in Ceres.CeresUtils]
xs:149 [binder, in Ceres.CeresRoundtrip]
xs:162 [binder, in Ceres.CeresRoundtrip]
xs:19 [binder, in Ceres.CeresS]
xs:228 [binder, in Ceres.CeresDeserialize]
xs:24 [binder, in Ceres.CeresUtils]
xs:34 [binder, in Ceres.CeresS]
xs:35 [binder, in Ceres.CeresSerialize]
xs:5 [binder, in Ceres.CeresS]
xs:53 [binder, in Ceres.CeresS]
xs:56 [binder, in Ceres.CeresParserRoundtrip]
xs:58 [binder, in Ceres.CeresRoundtrip]
xs:67 [binder, in Ceres.CeresS]
xs:67 [binder, in Ceres.CeresRoundtrip]
xs:71 [binder, in Ceres.CeresS]
xs:73 [binder, in Ceres.CeresString]
x1:47 [binder, in Ceres.CeresS]
x1:58 [binder, in Ceres.CeresS]
x1:60 [binder, in Ceres.CeresS]
x1:62 [binder, in Ceres.CeresS]
x2:48 [binder, in Ceres.CeresS]
x2:59 [binder, in Ceres.CeresS]
x2:61 [binder, in Ceres.CeresS]
x2:63 [binder, in Ceres.CeresS]
x:10 [binder, in Ceres.CeresString]
x:10 [binder, in Ceres.CeresFormat]
x:13 [binder, in Ceres.CeresString]
x:15 [binder, in Ceres.CeresS]
x:2 [binder, in Ceres.CeresString]
x:20 [binder, in Ceres.CeresUtils]
x:25 [binder, in Ceres.CeresUtils]
x:3 [binder, in Ceres.CeresFormat]
x:42 [binder, in Ceres.CeresDeserialize]
x:5 [binder, in Ceres.CeresUtils]
x:55 [binder, in Ceres.CeresParserRoundtrip]
x:6 [binder, in Ceres.CeresString]
X:64 [binder, in Ceres.CeresS]
x:66 [binder, in Ceres.CeresS]
x:68 [binder, in Ceres.CeresRoundtrip]
x:7 [binder, in Ceres.CeresFormat]
x:73 [binder, in Ceres.CeresParserRoundtrip]
x:8 [binder, in Ceres.CeresString]
x:9 [binder, in Ceres.CeresS]
Y
ys:231 [binder, in Ceres.CeresDeserialize]ys:26 [binder, in Ceres.CeresUtils]
ys:35 [binder, in Ceres.CeresS]
ys:58 [binder, in Ceres.CeresParserRoundtrip]
y:11 [binder, in Ceres.CeresString]
y:14 [binder, in Ceres.CeresString]
y:5 [binder, in Ceres.CeresString]
y:57 [binder, in Ceres.CeresParserRoundtrip]
y:7 [binder, in Ceres.CeresString]
y:9 [binder, in Ceres.CeresString]
Z
z:12 [binder, in Ceres.CeresSerialize]z:32 [binder, in Ceres.CeresRoundtrip]
z:63 [binder, in Ceres.CeresParserRoundtrip]
_
_sexp_to_list [definition, in Ceres.CeresDeserialize]_fields [projection, in Ceres.CeresDeserialize]
_from_sexp [projection, in Ceres.CeresDeserialize]
_from_sexp [constructor, in Ceres.CeresDeserialize]
_bind_sum [definition, in Ceres.CeresUtils]
_find_or [definition, in Ceres.CeresUtils]
_done_or_fail [definition, in Ceres.CeresParserInternal]
_fold_stack [definition, in Ceres.CeresParserInternal]
_unescape_string [definition, in Ceres.CeresString]
_unthree_digit [definition, in Ceres.CeresString]
_end:88 [binder, in Ceres.CeresString]
_escape_string [definition, in Ceres.CeresString]
_three_digit [definition, in Ceres.CeresString]
_units_digit [definition, in Ceres.CeresString]
_string_reverse [definition, in Ceres.CeresString]
_parse_sexps_sound [lemma, in Ceres.CeresParserRoundtripProof]
_done_or_fail_sound [lemma, in Ceres.CeresParserRoundtripProof]
_fold_stack_sound [lemma, in Ceres.CeresParserRoundtripProof]
_fold_stack_sound_ [lemma, in Ceres.CeresParserRoundtripProof]
_string_reverse_app [lemma, in Ceres.CeresParserRoundtripProof]
_find_or_spec [lemma, in Ceres.CeresRoundtrip]
other
_ <=? _ (char2_scope) [notation, in Ceres.CeresString]_ =? _ (char2_scope) [notation, in Ceres.CeresString]
_ :: _ (compare_scope) [notation, in Ceres.CeresString]
_ ++ _ (dstring_scope) [notation, in Ceres.CeresString]
[ _ ; _ ; .. ; _ ] (sexp_scope) [notation, in Ceres.CeresS]
[ _ ] (sexp_scope) [notation, in Ceres.CeresS]
[ ] (sexp_scope) [notation, in Ceres.CeresS]
_ :: _ (string_scope) [notation, in Ceres.CeresString]
_ ++ _ (s_msg_scope) [notation, in Ceres.CeresDeserialize]
Notation Index
D
_ >>= _ (deser_scope) [in Ceres.CeresDeserialize]other
_ <=? _ (char2_scope) [in Ceres.CeresString]_ =? _ (char2_scope) [in Ceres.CeresString]
_ :: _ (compare_scope) [in Ceres.CeresString]
_ ++ _ (dstring_scope) [in Ceres.CeresString]
[ _ ; _ ; .. ; _ ] (sexp_scope) [in Ceres.CeresS]
[ _ ] (sexp_scope) [in Ceres.CeresS]
[ ] (sexp_scope) [in Ceres.CeresS]
_ :: _ (string_scope) [in Ceres.CeresString]
_ ++ _ (s_msg_scope) [in Ceres.CeresDeserialize]
Binder Index
A
ab:22 [in Ceres.CeresSerialize]ab:28 [in Ceres.CeresSerialize]
all_con:45 [in Ceres.CeresDeserialize]
all_con:39 [in Ceres.CeresDeserialize]
a_eqb:41 [in Ceres.CeresS]
a':120 [in Ceres.CeresRoundtrip]
A:1 [in Ceres.CeresSerialize]
A:1 [in Ceres.CeresUtils]
A:1 [in Ceres.CeresString]
A:1 [in Ceres.CeresS]
A:1 [in Ceres.CeresFormat]
A:1 [in Ceres.CeresRoundtrip]
A:10 [in Ceres.CeresSerialize]
A:10 [in Ceres.CeresRoundtrip]
a:104 [in Ceres.CeresRoundtrip]
a:107 [in Ceres.CeresDeserialize]
A:108 [in Ceres.CeresRoundtrip]
A:11 [in Ceres.CeresDeserialize]
a:11 [in Ceres.CeresUtils]
a:11 [in Ceres.CeresFormat]
A:111 [in Ceres.CeresDeserialize]
a:114 [in Ceres.CeresRoundtrip]
A:12 [in Ceres.CeresS]
a:123 [in Ceres.CeresDeserialize]
A:123 [in Ceres.CeresRoundtrip]
A:127 [in Ceres.CeresRoundtrip]
A:128 [in Ceres.CeresDeserialize]
A:13 [in Ceres.CeresDeserialize]
A:132 [in Ceres.CeresDeserialize]
A:135 [in Ceres.CeresRoundtrip]
A:138 [in Ceres.CeresDeserialize]
A:14 [in Ceres.CeresSerialize]
A:143 [in Ceres.CeresRoundtrip]
A:146 [in Ceres.CeresDeserialize]
a:152 [in Ceres.CeresRoundtrip]
A:153 [in Ceres.CeresRoundtrip]
A:156 [in Ceres.CeresDeserialize]
A:157 [in Ceres.CeresRoundtrip]
A:16 [in Ceres.CeresDeserialize]
A:16 [in Ceres.CeresRoundtrip]
a:161 [in Ceres.CeresRoundtrip]
A:165 [in Ceres.CeresRoundtrip]
A:168 [in Ceres.CeresDeserialize]
A:17 [in Ceres.CeresUtils]
a:17 [in Ceres.CeresString]
A:177 [in Ceres.CeresDeserialize]
A:18 [in Ceres.CeresSerialize]
A:18 [in Ceres.CeresS]
a:185 [in Ceres.CeresDeserialize]
A:186 [in Ceres.CeresDeserialize]
A:19 [in Ceres.CeresDeserialize]
a:190 [in Ceres.CeresDeserialize]
A:191 [in Ceres.CeresDeserialize]
A:194 [in Ceres.CeresDeserialize]
A:201 [in Ceres.CeresDeserialize]
A:203 [in Ceres.CeresDeserialize]
A:207 [in Ceres.CeresDeserialize]
a:21 [in Ceres.CeresString]
a:214 [in Ceres.CeresDeserialize]
A:22 [in Ceres.CeresDeserialize]
A:22 [in Ceres.CeresRoundtrip]
A:226 [in Ceres.CeresDeserialize]
A:23 [in Ceres.CeresUtils]
A:234 [in Ceres.CeresDeserialize]
A:24 [in Ceres.CeresSerialize]
a:25 [in Ceres.CeresString]
a:25 [in Ceres.CeresS]
a:26 [in Ceres.CeresRoundtrip]
A:27 [in Ceres.CeresString]
a:27 [in Ceres.CeresS]
A:28 [in Ceres.CeresRoundtrip]
A:29 [in Ceres.CeresDeserialize]
a:29 [in Ceres.CeresString]
a:29 [in Ceres.CeresS]
a:3 [in Tutorial]
a:31 [in Ceres.CeresSerialize]
A:31 [in Ceres.CeresDeserialize]
A:31 [in Ceres.CeresS]
A:33 [in Ceres.CeresSerialize]
a:33 [in Ceres.CeresString]
a:33 [in Ceres.CeresRoundtrip]
a:35 [in Ceres.CeresString]
A:35 [in Ceres.CeresRoundtrip]
a:37 [in Ceres.CeresString]
a:39 [in Ceres.CeresString]
A:39 [in Ceres.CeresS]
A:39 [in Ceres.CeresRoundtrip]
A:4 [in Ceres.CeresSerialize]
a:4 [in Ceres.CeresS]
a:4 [in Ceres.CeresRoundtrip]
A:43 [in Ceres.CeresRoundtrip]
A:48 [in Ceres.CeresDeserialize]
a:49 [in Ceres.CeresRoundtrip]
A:5 [in Ceres.CeresRoundtrip]
A:50 [in Ceres.CeresParserRoundtrip]
A:51 [in Ceres.CeresS]
A:53 [in Ceres.CeresRoundtrip]
a:54 [in Ceres.CeresS]
a:57 [in Ceres.CeresRoundtrip]
A:59 [in Ceres.CeresDeserialize]
a:6 [in Ceres.CeresSerialize]
A:6 [in Ceres.CeresS]
A:64 [in Ceres.CeresRoundtrip]
a:67 [in Ceres.CeresParserRoundtrip]
A:68 [in Ceres.CeresS]
a:69 [in Ceres.CeresDeserialize]
A:69 [in Ceres.CeresRoundtrip]
A:7 [in Ceres.CeresSerialize]
A:7 [in Ceres.CeresDeserialize]
A:7 [in Ceres.CeresUtils]
a:70 [in Ceres.CeresS]
A:71 [in Ceres.CeresParserRoundtrip]
A:73 [in Ceres.CeresDeserialize]
A:73 [in Ceres.CeresS]
a:75 [in Ceres.CeresRoundtrip]
a:77 [in Ceres.CeresDeserialize]
A:78 [in Ceres.CeresDeserialize]
A:79 [in Ceres.CeresRoundtrip]
A:8 [in Ceres.CeresDeserialize]
A:8 [in Ceres.CeresFormat]
A:83 [in Ceres.CeresRoundtrip]
a:84 [in Ceres.CeresDeserialize]
A:86 [in Ceres.CeresDeserialize]
a:9 [in Ceres.CeresRoundtrip]
A:91 [in Ceres.CeresRoundtrip]
a:94 [in Ceres.CeresDeserialize]
A:97 [in Ceres.CeresDeserialize]
B
B':3 [in Ceres.CeresUtils]b:108 [in Ceres.CeresDeserialize]
B:109 [in Ceres.CeresRoundtrip]
B:112 [in Ceres.CeresDeserialize]
b:112 [in Ceres.CeresString]
b:124 [in Ceres.CeresDeserialize]
B:128 [in Ceres.CeresRoundtrip]
b:13 [in Ceres.CeresSerialize]
B:13 [in Ceres.CeresS]
B:133 [in Ceres.CeresDeserialize]
B:136 [in Ceres.CeresRoundtrip]
B:139 [in Ceres.CeresDeserialize]
b:14 [in Ceres.CeresUtils]
B:147 [in Ceres.CeresDeserialize]
B:157 [in Ceres.CeresDeserialize]
B:178 [in Ceres.CeresDeserialize]
B:18 [in Ceres.CeresUtils]
b:18 [in Ceres.CeresString]
B:19 [in Ceres.CeresSerialize]
B:2 [in Ceres.CeresUtils]
B:204 [in Ceres.CeresDeserialize]
B:208 [in Ceres.CeresDeserialize]
b:215 [in Ceres.CeresDeserialize]
b:22 [in Ceres.CeresString]
B:25 [in Ceres.CeresSerialize]
b:26 [in Ceres.CeresString]
b:30 [in Ceres.CeresString]
B:32 [in Ceres.CeresS]
b:34 [in Ceres.CeresString]
b:36 [in Ceres.CeresString]
b:38 [in Ceres.CeresString]
b:40 [in Ceres.CeresString]
B:40 [in Ceres.CeresS]
B:51 [in Ceres.CeresParserRoundtrip]
B:54 [in Ceres.CeresRoundtrip]
b:55 [in Ceres.CeresS]
B:60 [in Ceres.CeresDeserialize]
b:60 [in Ceres.CeresRoundtrip]
B:7 [in Ceres.CeresS]
B:72 [in Ceres.CeresParserRoundtrip]
B:79 [in Ceres.CeresDeserialize]
B:8 [in Ceres.CeresUtils]
B:84 [in Ceres.CeresRoundtrip]
b:85 [in Ceres.CeresDeserialize]
B:87 [in Ceres.CeresDeserialize]
B:92 [in Ceres.CeresRoundtrip]
b:95 [in Ceres.CeresDeserialize]
B:98 [in Ceres.CeresDeserialize]
C
c':69 [in Ceres.CeresString]c':72 [in Ceres.CeresString]
c0:31 [in Ceres.CeresString]
c0:33 [in Ceres.CeresDeserialize]
c0:71 [in Ceres.CeresRoundtrip]
c0:99 [in Ceres.CeresString]
c1:32 [in Ceres.CeresString]
c1:34 [in Ceres.CeresDeserialize]
c1:72 [in Ceres.CeresRoundtrip]
c1:98 [in Ceres.CeresString]
c2:97 [in Ceres.CeresString]
c:109 [in Ceres.CeresDeserialize]
C:113 [in Ceres.CeresDeserialize]
c:116 [in Ceres.CeresString]
c:12 [in Ceres.CeresParserRoundtrip]
c:12 [in Ceres.CeresParserRoundtripProof]
c:125 [in Ceres.CeresDeserialize]
C:140 [in Ceres.CeresDeserialize]
C:148 [in Ceres.CeresDeserialize]
C:158 [in Ceres.CeresDeserialize]
c:17 [in Ceres.CeresParserRoundtrip]
c:183 [in Ceres.CeresParserRoundtripProof]
c:189 [in Ceres.CeresParserRoundtripProof]
C:19 [in Ceres.CeresUtils]
c:193 [in Ceres.CeresParserRoundtripProof]
c:194 [in Ceres.CeresParserRoundtripProof]
c:2 [in Ceres.CeresParserRoundtripProof]
c:200 [in Ceres.CeresParserRoundtripProof]
c:210 [in Ceres.CeresParserRoundtripProof]
c:221 [in Ceres.CeresParserRoundtripProof]
c:27 [in Ceres.CeresParserInternal]
c:35 [in Ceres.CeresDeserialize]
c:39 [in Ceres.CeresParserRoundtrip]
c:42 [in Ceres.CeresParserInternal]
c:43 [in Ceres.CeresDeserialize]
c:44 [in Ceres.CeresParserInternal]
c:44 [in Ceres.CeresParserRoundtrip]
c:48 [in Ceres.CeresParserRoundtrip]
c:49 [in Ceres.CeresParserInternal]
c:50 [in Ceres.CeresRoundtrip]
c:51 [in Ceres.CeresRoundtrip]
c:52 [in Ceres.CeresString]
C:55 [in Ceres.CeresRoundtrip]
c:6 [in Ceres.CeresParserUtils]
c:63 [in Ceres.CeresParserRoundtripProof]
c:65 [in Ceres.CeresString]
c:65 [in Ceres.CeresParserRoundtripProof]
c:68 [in Ceres.CeresString]
c:71 [in Ceres.CeresString]
c:76 [in Ceres.CeresString]
c:76 [in Ceres.CeresParserRoundtripProof]
c:77 [in Ceres.CeresString]
c:79 [in Ceres.CeresString]
c:80 [in Ceres.CeresString]
c:81 [in Ceres.CeresString]
c:81 [in Ceres.CeresParserRoundtripProof]
c:82 [in Ceres.CeresString]
C:88 [in Ceres.CeresDeserialize]
C:9 [in Ceres.CeresUtils]
c:91 [in Ceres.CeresParserRoundtripProof]
c:95 [in Ceres.CeresString]
c:96 [in Ceres.CeresDeserialize]
C:99 [in Ceres.CeresDeserialize]
D
de:3 [in Ceres.CeresRoundtrip]de:7 [in Ceres.CeresRoundtrip]
doa:100 [in Ceres.CeresString]
dstring_A:2 [in Ceres.CeresFormat]
D:100 [in Ceres.CeresDeserialize]
d:105 [in Ceres.CeresParserRoundtripProof]
d:110 [in Ceres.CeresDeserialize]
d:112 [in Ceres.CeresParserRoundtripProof]
D:114 [in Ceres.CeresDeserialize]
d:126 [in Ceres.CeresDeserialize]
d:127 [in Ceres.CeresParserRoundtripProof]
d:138 [in Ceres.CeresParserRoundtripProof]
D:149 [in Ceres.CeresDeserialize]
d:151 [in Ceres.CeresParserRoundtripProof]
D:159 [in Ceres.CeresDeserialize]
d:159 [in Ceres.CeresParserRoundtripProof]
d:17 [in Ceres.CeresParserInternal]
d:174 [in Ceres.CeresParserRoundtripProof]
d:223 [in Ceres.CeresParserRoundtripProof]
d:33 [in Ceres.CeresParserInternal]
E
Ei:214 [in Ceres.CeresParserRoundtripProof]eqb_A:74 [in Ceres.CeresS]
eqb:10 [in Ceres.CeresUtils]
eqb:28 [in Ceres.CeresString]
eqb:52 [in Ceres.CeresS]
eqb:56 [in Ceres.CeresRoundtrip]
err:106 [in Ceres.CeresRoundtrip]
err:117 [in Ceres.CeresRoundtrip]
err:37 [in Ceres.CeresDeserialize]
escaped_s':92 [in Ceres.CeresString]
es':122 [in Ceres.CeresRoundtrip]
es1:5 [in Ceres.CeresParserRoundtripProof]
es2:6 [in Ceres.CeresParserRoundtripProof]
es:107 [in Ceres.CeresRoundtrip]
es:115 [in Ceres.CeresRoundtrip]
es:145 [in Ceres.CeresParserRoundtripProof]
es:147 [in Ceres.CeresRoundtrip]
es:164 [in Ceres.CeresParserRoundtripProof]
es:228 [in Ceres.CeresParserRoundtripProof]
es:234 [in Ceres.CeresParserRoundtripProof]
es:240 [in Ceres.CeresParserRoundtripProof]
es:38 [in Ceres.CeresDeserialize]
es:52 [in Ceres.CeresRoundtrip]
es:56 [in Ceres.CeresDeserialize]
es:67 [in Ceres.CeresDeserialize]
es:69 [in Ceres.CeresParserRoundtrip]
es:77 [in Ceres.CeresParserRoundtrip]
es:78 [in Ceres.CeresParserRoundtrip]
es:78 [in Ceres.CeresRoundtrip]
e':121 [in Ceres.CeresRoundtrip]
e':30 [in Ceres.CeresParserInternal]
e:101 [in Ceres.CeresParserRoundtripProof]
E:115 [in Ceres.CeresDeserialize]
e:127 [in Ceres.CeresDeserialize]
E:160 [in Ceres.CeresDeserialize]
e:19 [in Ceres.CeresParserInternal]
e:197 [in Ceres.CeresDeserialize]
e:201 [in Ceres.CeresParserRoundtripProof]
e:212 [in Ceres.CeresDeserialize]
e:218 [in Ceres.CeresDeserialize]
e:221 [in Ceres.CeresDeserialize]
e:224 [in Ceres.CeresDeserialize]
e:237 [in Ceres.CeresDeserialize]
e:25 [in Ceres.CeresParserInternal]
e:27 [in Ceres.CeresDeserialize]
e:3 [in Ceres.CeresParserRoundtripProof]
e:4 [in Ceres.CeresParserUtils]
e:41 [in Ceres.CeresParserRoundtripProof]
e:48 [in Ceres.CeresRoundtrip]
e:60 [in Ceres.CeresParserRoundtripProof]
e:7 [in Tutorial]
e:71 [in Ceres.CeresParserRoundtripProof]
e:74 [in Ceres.CeresRoundtrip]
e:8 [in Ceres.CeresRoundtrip]
F
fs:148 [in Ceres.CeresRoundtrip]f:102 [in Ceres.CeresDeserialize]
f:113 [in Ceres.CeresRoundtrip]
f:117 [in Ceres.CeresDeserialize]
f:13 [in Ceres.CeresUtils]
f:130 [in Ceres.CeresDeserialize]
f:135 [in Ceres.CeresDeserialize]
f:14 [in Ceres.CeresS]
f:142 [in Ceres.CeresDeserialize]
f:151 [in Ceres.CeresDeserialize]
f:162 [in Ceres.CeresDeserialize]
f:184 [in Ceres.CeresDeserialize]
f:21 [in Ceres.CeresUtils]
f:25 [in Ceres.CeresDeserialize]
f:30 [in Ceres.CeresDeserialize]
f:33 [in Ceres.CeresS]
f:4 [in Ceres.CeresUtils]
f:46 [in Ceres.CeresRoundtrip]
f:56 [in Ceres.CeresString]
f:59 [in Ceres.CeresRoundtrip]
f:64 [in Ceres.CeresDeserialize]
f:75 [in Ceres.CeresDeserialize]
f:8 [in Ceres.CeresS]
f:81 [in Ceres.CeresDeserialize]
f:90 [in Ceres.CeresDeserialize]
G
g:24 [in Ceres.CeresDeserialize]g:45 [in Ceres.CeresRoundtrip]
H
Hdone:147 [in Ceres.CeresParserRoundtripProof]Hdone:169 [in Ceres.CeresParserRoundtripProof]
Hdu:131 [in Ceres.CeresParserRoundtripProof]
Heqb_eq:75 [in Ceres.CeresS]
Heqb:56 [in Ceres.CeresS]
Hes:150 [in Ceres.CeresParserRoundtripProof]
Hes:172 [in Ceres.CeresParserRoundtripProof]
Hi:157 [in Ceres.CeresParserRoundtripProof]
Hi:206 [in Ceres.CeresParserRoundtripProof]
Hi:213 [in Ceres.CeresParserRoundtripProof]
Hmore:133 [in Ceres.CeresParserRoundtripProof]
Hstackend:149 [in Ceres.CeresParserRoundtripProof]
Hstackend:171 [in Ceres.CeresParserRoundtripProof]
Hstack:148 [in Ceres.CeresParserRoundtripProof]
Hstack:170 [in Ceres.CeresParserRoundtripProof]
Hs0:146 [in Ceres.CeresParserRoundtripProof]
Hs0:168 [in Ceres.CeresParserRoundtripProof]
Hs:216 [in Ceres.CeresParserRoundtripProof]
H0:12 [in Ceres.CeresRoundtrip]
H0:136 [in Ceres.CeresParserRoundtripProof]
H0:137 [in Ceres.CeresDeserialize]
H0:144 [in Ceres.CeresDeserialize]
H0:153 [in Ceres.CeresDeserialize]
H0:164 [in Ceres.CeresDeserialize]
H0:18 [in Ceres.CeresRoundtrip]
H0:183 [in Ceres.CeresDeserialize]
H0:206 [in Ceres.CeresDeserialize]
H0:21 [in Ceres.CeresSerialize]
H0:210 [in Ceres.CeresDeserialize]
H0:24 [in Ceres.CeresRoundtrip]
H0:27 [in Ceres.CeresSerialize]
H0:30 [in Ceres.CeresRoundtrip]
H1:126 [in Ceres.CeresRoundtrip]
H1:131 [in Ceres.CeresRoundtrip]
H1:139 [in Ceres.CeresRoundtrip]
H1:145 [in Ceres.CeresDeserialize]
H1:146 [in Ceres.CeresRoundtrip]
H1:154 [in Ceres.CeresDeserialize]
H1:156 [in Ceres.CeresRoundtrip]
H1:160 [in Ceres.CeresRoundtrip]
H1:165 [in Ceres.CeresDeserialize]
H1:168 [in Ceres.CeresRoundtrip]
H1:38 [in Ceres.CeresRoundtrip]
H1:42 [in Ceres.CeresRoundtrip]
H1:82 [in Ceres.CeresRoundtrip]
H1:87 [in Ceres.CeresRoundtrip]
H1:95 [in Ceres.CeresRoundtrip]
H2:155 [in Ceres.CeresDeserialize]
H2:166 [in Ceres.CeresDeserialize]
H3:167 [in Ceres.CeresDeserialize]
H4:134 [in Ceres.CeresRoundtrip]
H4:142 [in Ceres.CeresRoundtrip]
H4:90 [in Ceres.CeresRoundtrip]
H4:98 [in Ceres.CeresRoundtrip]
H:11 [in Ceres.CeresSerialize]
H:11 [in Ceres.CeresRoundtrip]
H:12 [in Ceres.CeresDeserialize]
H:131 [in Ceres.CeresDeserialize]
H:135 [in Ceres.CeresParserRoundtripProof]
H:136 [in Ceres.CeresDeserialize]
H:14 [in Ceres.CeresDeserialize]
H:143 [in Ceres.CeresDeserialize]
H:15 [in Ceres.CeresSerialize]
H:152 [in Ceres.CeresDeserialize]
H:158 [in Ceres.CeresParserRoundtripProof]
H:163 [in Ceres.CeresDeserialize]
H:17 [in Ceres.CeresRoundtrip]
H:182 [in Ceres.CeresDeserialize]
H:189 [in Ceres.CeresDeserialize]
H:195 [in Ceres.CeresDeserialize]
H:20 [in Ceres.CeresSerialize]
H:202 [in Ceres.CeresDeserialize]
H:205 [in Ceres.CeresDeserialize]
H:207 [in Ceres.CeresParserRoundtripProof]
H:209 [in Ceres.CeresDeserialize]
H:227 [in Ceres.CeresParserRoundtripProof]
H:23 [in Ceres.CeresRoundtrip]
H:233 [in Ceres.CeresParserRoundtripProof]
H:235 [in Ceres.CeresDeserialize]
H:26 [in Ceres.CeresSerialize]
H:29 [in Ceres.CeresRoundtrip]
H:34 [in Ceres.CeresSerialize]
H:5 [in Ceres.CeresSerialize]
I
i':137 [in Ceres.CeresParserRoundtripProof]i':173 [in Ceres.CeresParserRoundtripProof]
i':179 [in Ceres.CeresParserRoundtripProof]
i':190 [in Ceres.CeresParserRoundtripProof]
i':208 [in Ceres.CeresParserRoundtripProof]
i':217 [in Ceres.CeresParserRoundtripProof]
i':222 [in Ceres.CeresParserRoundtripProof]
i':50 [in Ceres.CeresParserInternal]
i:119 [in Ceres.CeresParserRoundtripProof]
i:14 [in Ceres.CeresParserInternal]
i:185 [in Ceres.CeresParserRoundtripProof]
i:197 [in Ceres.CeresParserRoundtripProof]
i:209 [in Ceres.CeresParserRoundtripProof]
i:218 [in Ceres.CeresParserRoundtripProof]
i:22 [in Ceres.CeresParserInternal]
i:230 [in Ceres.CeresParserRoundtripProof]
i:236 [in Ceres.CeresParserRoundtripProof]
i:40 [in Ceres.CeresParserInternal]
i:43 [in Ceres.CeresParserInternal]
i:47 [in Ceres.CeresParserInternal]
i:55 [in Ceres.CeresParserInternal]
i:57 [in Ceres.CeresParserInternal]
i:58 [in Ceres.CeresParserInternal]
i:59 [in Ceres.CeresParserInternal]
i:60 [in Ceres.CeresParserInternal]
L
l:105 [in Ceres.CeresRoundtrip]l:116 [in Ceres.CeresRoundtrip]
l:14 [in Ceres.CeresRoundtrip]
l:151 [in Ceres.CeresRoundtrip]
l:164 [in Ceres.CeresRoundtrip]
l:196 [in Ceres.CeresDeserialize]
l:20 [in Ceres.CeresRoundtrip]
l:211 [in Ceres.CeresDeserialize]
l:216 [in Ceres.CeresDeserialize]
l:217 [in Ceres.CeresDeserialize]
l:220 [in Ceres.CeresDeserialize]
l:223 [in Ceres.CeresDeserialize]
l:230 [in Ceres.CeresDeserialize]
l:236 [in Ceres.CeresDeserialize]
l:26 [in Ceres.CeresDeserialize]
l:36 [in Ceres.CeresDeserialize]
l:44 [in Ceres.CeresDeserialize]
l:47 [in Ceres.CeresRoundtrip]
l:54 [in Ceres.CeresDeserialize]
l:6 [in Tutorial]
l:65 [in Ceres.CeresDeserialize]
l:73 [in Ceres.CeresRoundtrip]
M
mk_error:66 [in Ceres.CeresDeserialize]mk_error:55 [in Ceres.CeresDeserialize]
more':115 [in Ceres.CeresParserRoundtripProof]
more:104 [in Ceres.CeresParserRoundtripProof]
more:114 [in Ceres.CeresParserRoundtripProof]
more:122 [in Ceres.CeresParserRoundtripProof]
more:125 [in Ceres.CeresParserRoundtripProof]
more:130 [in Ceres.CeresParserRoundtripProof]
more:14 [in Ceres.CeresParserRoundtrip]
more:144 [in Ceres.CeresParserRoundtripProof]
more:15 [in Ceres.CeresParserRoundtrip]
more:15 [in Ceres.CeresParserRoundtripProof]
more:153 [in Ceres.CeresParserRoundtripProof]
more:16 [in Ceres.CeresParserRoundtrip]
more:16 [in Ceres.CeresParserRoundtripProof]
more:162 [in Ceres.CeresParserRoundtripProof]
more:177 [in Ceres.CeresParserRoundtripProof]
more:180 [in Ceres.CeresParserRoundtripProof]
more:186 [in Ceres.CeresParserRoundtripProof]
more:19 [in Ceres.CeresParserRoundtripProof]
more:191 [in Ceres.CeresParserRoundtripProof]
more:202 [in Ceres.CeresParserRoundtripProof]
more:21 [in Ceres.CeresParserRoundtrip]
more:211 [in Ceres.CeresParserRoundtripProof]
more:225 [in Ceres.CeresParserRoundtripProof]
more:25 [in Ceres.CeresParserRoundtripProof]
more:28 [in Ceres.CeresParserRoundtripProof]
more:32 [in Ceres.CeresParserRoundtripProof]
more:46 [in Ceres.CeresParserRoundtrip]
more:47 [in Ceres.CeresParserRoundtrip]
more:69 [in Ceres.CeresParserRoundtripProof]
msg:4 [in Ceres.CeresDeserialize]
msg:41 [in Ceres.CeresDeserialize]
msg:47 [in Ceres.CeresDeserialize]
msg:58 [in Ceres.CeresDeserialize]
msg:70 [in Ceres.CeresDeserialize]
m:112 [in Ceres.CeresRoundtrip]
m:17 [in Ceres.CeresDeserialize]
m:171 [in Ceres.CeresDeserialize]
m:175 [in Ceres.CeresDeserialize]
m:181 [in Ceres.CeresDeserialize]
m:188 [in Ceres.CeresDeserialize]
m:63 [in Ceres.CeresDeserialize]
N
n0:85 [in Ceres.CeresString]n1:86 [in Ceres.CeresString]
n2:87 [in Ceres.CeresString]
n:101 [in Ceres.CeresRoundtrip]
n:109 [in Ceres.CeresString]
n:110 [in Ceres.CeresString]
n:111 [in Ceres.CeresString]
n:111 [in Ceres.CeresRoundtrip]
n:150 [in Ceres.CeresRoundtrip]
n:163 [in Ceres.CeresRoundtrip]
n:170 [in Ceres.CeresDeserialize]
n:18 [in Ceres.CeresDeserialize]
n:180 [in Ceres.CeresDeserialize]
n:199 [in Ceres.CeresDeserialize]
n:200 [in Ceres.CeresDeserialize]
n:22 [in Ceres.CeresS]
n:229 [in Ceres.CeresDeserialize]
n:49 [in Ceres.CeresDeserialize]
n:53 [in Ceres.CeresDeserialize]
n:62 [in Ceres.CeresDeserialize]
n:83 [in Ceres.CeresString]
n:84 [in Ceres.CeresString]
n:93 [in Ceres.CeresString]
n:96 [in Ceres.CeresString]
O
oa:16 [in Ceres.CeresSerialize]P
pa:103 [in Ceres.CeresDeserialize]pa:110 [in Ceres.CeresRoundtrip]
pa:118 [in Ceres.CeresDeserialize]
pa:227 [in Ceres.CeresDeserialize]
pa:61 [in Ceres.CeresDeserialize]
pa:76 [in Ceres.CeresDeserialize]
pa:82 [in Ceres.CeresDeserialize]
pa:91 [in Ceres.CeresDeserialize]
pb:104 [in Ceres.CeresDeserialize]
pb:119 [in Ceres.CeresDeserialize]
pb:83 [in Ceres.CeresDeserialize]
pb:92 [in Ceres.CeresDeserialize]
pc:105 [in Ceres.CeresDeserialize]
pc:120 [in Ceres.CeresDeserialize]
pc:93 [in Ceres.CeresDeserialize]
pd:106 [in Ceres.CeresDeserialize]
pd:121 [in Ceres.CeresDeserialize]
pe:122 [in Ceres.CeresDeserialize]
p0:23 [in Ceres.CeresParserInternal]
p1:199 [in Ceres.CeresParserRoundtripProof]
p:1 [in Ceres.CeresParserUtils]
p:160 [in Ceres.CeresParserRoundtripProof]
p:175 [in Ceres.CeresParserRoundtripProof]
p:188 [in Ceres.CeresParserRoundtripProof]
p:198 [in Ceres.CeresParserRoundtripProof]
p:220 [in Ceres.CeresParserRoundtripProof]
p:231 [in Ceres.CeresParserRoundtripProof]
p:237 [in Ceres.CeresParserRoundtripProof]
p:26 [in Ceres.CeresParserInternal]
p:34 [in Ceres.CeresParserInternal]
p:38 [in Ceres.CeresParserRoundtripProof]
p:41 [in Ceres.CeresParserInternal]
p:47 [in Ceres.CeresParserRoundtripProof]
p:48 [in Ceres.CeresParserInternal]
p:50 [in Ceres.CeresDeserialize]
p:56 [in Ceres.CeresParserInternal]
p:56 [in Ceres.CeresParserRoundtripProof]
p:61 [in Ceres.CeresParserInternal]
P:61 [in Ceres.CeresRoundtrip]
p:62 [in Ceres.CeresRoundtrip]
p:63 [in Ceres.CeresRoundtrip]
P:65 [in Ceres.CeresS]
P:65 [in Ceres.CeresRoundtrip]
P:69 [in Ceres.CeresS]
P:74 [in Ceres.CeresParserRoundtrip]
p:76 [in Ceres.CeresRoundtrip]
p:77 [in Ceres.CeresRoundtrip]
p:96 [in Ceres.CeresParserRoundtripProof]
p:99 [in Ceres.CeresParserRoundtripProof]
Q
Q:66 [in Ceres.CeresRoundtrip]R
ret:31 [in Ceres.CeresParserInternal]r:100 [in Ceres.CeresRoundtrip]
R:101 [in Ceres.CeresDeserialize]
R:116 [in Ceres.CeresDeserialize]
R:129 [in Ceres.CeresDeserialize]
R:134 [in Ceres.CeresDeserialize]
R:141 [in Ceres.CeresDeserialize]
R:150 [in Ceres.CeresDeserialize]
R:161 [in Ceres.CeresDeserialize]
R:169 [in Ceres.CeresDeserialize]
R:174 [in Ceres.CeresDeserialize]
r:176 [in Ceres.CeresDeserialize]
R:179 [in Ceres.CeresDeserialize]
R:187 [in Ceres.CeresDeserialize]
r:35 [in Ceres.CeresParserInternal]
R:51 [in Ceres.CeresDeserialize]
r:51 [in Ceres.CeresParserInternal]
r:52 [in Ceres.CeresDeserialize]
r:60 [in Ceres.CeresString]
R:71 [in Ceres.CeresDeserialize]
r:72 [in Ceres.CeresDeserialize]
R:74 [in Ceres.CeresDeserialize]
R:80 [in Ceres.CeresDeserialize]
R:89 [in Ceres.CeresDeserialize]
R:99 [in Ceres.CeresRoundtrip]
S
ser:2 [in Ceres.CeresRoundtrip]ser:6 [in Ceres.CeresRoundtrip]
string_A:9 [in Ceres.CeresFormat]
s_str:34 [in Ceres.CeresParserRoundtripProof]
s_com:30 [in Ceres.CeresParserRoundtripProof]
s':102 [in Ceres.CeresParserRoundtripProof]
s':115 [in Ceres.CeresString]
s':132 [in Ceres.CeresParserRoundtripProof]
s':14 [in Ceres.CeresParserRoundtripProof]
s':156 [in Ceres.CeresParserRoundtripProof]
s':196 [in Ceres.CeresParserRoundtripProof]
s':205 [in Ceres.CeresParserRoundtripProof]
s':98 [in Ceres.CeresParserRoundtripProof]
s0':117 [in Ceres.CeresParserRoundtripProof]
s0:107 [in Ceres.CeresParserRoundtripProof]
s0:116 [in Ceres.CeresParserRoundtripProof]
s0:123 [in Ceres.CeresParserRoundtripProof]
s0:129 [in Ceres.CeresParserRoundtripProof]
s0:140 [in Ceres.CeresParserRoundtripProof]
s0:154 [in Ceres.CeresParserRoundtripProof]
s0:161 [in Ceres.CeresParserRoundtripProof]
s0:176 [in Ceres.CeresParserRoundtripProof]
s0:187 [in Ceres.CeresParserRoundtripProof]
s0:19 [in Ceres.CeresParserRoundtrip]
s0:203 [in Ceres.CeresParserRoundtripProof]
s0:212 [in Ceres.CeresParserRoundtripProof]
s0:226 [in Ceres.CeresParserRoundtripProof]
s0:238 [in Ceres.CeresParserRoundtripProof]
s0:32 [in Ceres.CeresParserRoundtrip]
s0:6 [in Ceres.CeresFormat]
s0:78 [in Ceres.CeresParserRoundtripProof]
s0:9 [in Ceres.CeresParserRoundtripProof]
s1':134 [in Ceres.CeresParserRoundtripProof]
s1:10 [in Ceres.CeresParserRoundtripProof]
s1:124 [in Ceres.CeresParserRoundtripProof]
s1:20 [in Ceres.CeresParserRoundtrip]
s1:215 [in Ceres.CeresParserRoundtripProof]
s1:24 [in Ceres.CeresParserRoundtripProof]
s1:29 [in Ceres.CeresParserRoundtrip]
s1:33 [in Ceres.CeresParserRoundtrip]
s1:41 [in Ceres.CeresString]
s1:42 [in Ceres.CeresS]
s1:46 [in Ceres.CeresString]
s1:48 [in Ceres.CeresString]
s1:50 [in Ceres.CeresString]
s1:66 [in Ceres.CeresString]
s1:76 [in Ceres.CeresS]
s1:78 [in Ceres.CeresS]
s1:79 [in Ceres.CeresParserRoundtripProof]
s1:80 [in Ceres.CeresS]
s2:11 [in Ceres.CeresParserRoundtripProof]
s2:42 [in Ceres.CeresString]
s2:43 [in Ceres.CeresS]
s2:47 [in Ceres.CeresString]
s2:49 [in Ceres.CeresString]
s2:51 [in Ceres.CeresString]
s2:67 [in Ceres.CeresString]
s2:77 [in Ceres.CeresS]
s2:79 [in Ceres.CeresS]
s2:80 [in Ceres.CeresParserRoundtripProof]
s2:81 [in Ceres.CeresS]
s:1 [in Ceres.CeresParser]
s:1 [in Ceres.CeresParserRoundtripProof]
s:101 [in Ceres.CeresString]
s:103 [in Ceres.CeresParserRoundtripProof]
s:107 [in Ceres.CeresString]
s:114 [in Ceres.CeresString]
s:117 [in Ceres.CeresString]
s:118 [in Ceres.CeresString]
s:126 [in Ceres.CeresParserRoundtripProof]
s:13 [in Ceres.CeresParserRoundtrip]
s:13 [in Ceres.CeresParserRoundtripProof]
s:15 [in Ceres.CeresDeserialize]
s:18 [in Ceres.CeresParserInternal]
s:18 [in Ceres.CeresParserRoundtrip]
s:18 [in Ceres.CeresParserRoundtripProof]
s:182 [in Ceres.CeresParserRoundtripProof]
s:192 [in Ceres.CeresParserRoundtripProof]
s:195 [in Ceres.CeresParserRoundtripProof]
s:2 [in Ceres.CeresParser]
s:21 [in Ceres.CeresParserRoundtripProof]
s:219 [in Ceres.CeresParserRoundtripProof]
s:23 [in Ceres.CeresS]
s:23 [in Ceres.CeresParserRoundtripProof]
s:232 [in Ceres.CeresParserRoundtripProof]
s:239 [in Ceres.CeresParserRoundtripProof]
s:24 [in Ceres.CeresS]
s:25 [in Ceres.CeresParserRoundtrip]
s:26 [in Ceres.CeresParserRoundtripProof]
s:27 [in Ceres.CeresParserRoundtrip]
s:29 [in Ceres.CeresParserRoundtripProof]
s:3 [in Ceres.CeresParserRoundtrip]
s:30 [in Ceres.CeresParserRoundtrip]
s:32 [in Ceres.CeresSerialize]
s:33 [in Ceres.CeresParserRoundtripProof]
s:34 [in Ceres.CeresParserRoundtrip]
s:36 [in Ceres.CeresParserInternal]
s:37 [in Ceres.CeresParserRoundtrip]
s:4 [in Ceres.CeresParserRoundtrip]
s:40 [in Ceres.CeresParserRoundtrip]
s:43 [in Ceres.CeresParserRoundtrip]
s:45 [in Ceres.CeresParserInternal]
s:45 [in Ceres.CeresParserRoundtrip]
s:46 [in Ceres.CeresParserInternal]
s:49 [in Ceres.CeresParserRoundtrip]
s:5 [in Ceres.CeresParserRoundtrip]
s:52 [in Ceres.CeresParserInternal]
s:53 [in Ceres.CeresString]
s:57 [in Ceres.CeresString]
s:61 [in Ceres.CeresParserRoundtrip]
s:61 [in Ceres.CeresString]
s:62 [in Ceres.CeresParserInternal]
s:62 [in Ceres.CeresParserRoundtrip]
s:62 [in Ceres.CeresParserRoundtripProof]
s:64 [in Ceres.CeresParserRoundtrip]
s:64 [in Ceres.CeresString]
s:64 [in Ceres.CeresParserRoundtripProof]
s:70 [in Ceres.CeresString]
s:72 [in Ceres.CeresS]
s:72 [in Ceres.CeresParserRoundtripProof]
s:73 [in Ceres.CeresParserRoundtripProof]
s:74 [in Ceres.CeresParserRoundtripProof]
s:75 [in Ceres.CeresParserRoundtripProof]
s:76 [in Ceres.CeresParserRoundtrip]
s:77 [in Ceres.CeresParserRoundtripProof]
s:8 [in Ceres.CeresParserRoundtrip]
s:82 [in Ceres.CeresParserRoundtripProof]
s:84 [in Ceres.CeresParserRoundtripProof]
s:86 [in Ceres.CeresParserRoundtripProof]
s:88 [in Ceres.CeresParserRoundtripProof]
s:89 [in Ceres.CeresString]
s:9 [in Ceres.CeresParserRoundtrip]
s:90 [in Ceres.CeresParserRoundtripProof]
s:93 [in Ceres.CeresParserRoundtripProof]
s:94 [in Ceres.CeresString]
s:97 [in Ceres.CeresParserRoundtripProof]
T
tks:52 [in Ceres.CeresParserRoundtrip]tok':29 [in Ceres.CeresParserInternal]
tok:100 [in Ceres.CeresParserRoundtripProof]
tok:155 [in Ceres.CeresParserRoundtripProof]
tok:204 [in Ceres.CeresParserRoundtripProof]
tok:24 [in Ceres.CeresParserInternal]
tok:66 [in Ceres.CeresParserRoundtripProof]
tok:70 [in Ceres.CeresParserRoundtripProof]
tok:83 [in Ceres.CeresParserRoundtripProof]
tok:85 [in Ceres.CeresParserRoundtripProof]
tok:87 [in Ceres.CeresParserRoundtripProof]
tok:89 [in Ceres.CeresParserRoundtripProof]
tok:92 [in Ceres.CeresParserRoundtripProof]
ts00:110 [in Ceres.CeresParserRoundtripProof]
ts00:141 [in Ceres.CeresParserRoundtripProof]
ts00:165 [in Ceres.CeresParserRoundtripProof]
ts01:111 [in Ceres.CeresParserRoundtripProof]
ts01:142 [in Ceres.CeresParserRoundtripProof]
ts01:166 [in Ceres.CeresParserRoundtripProof]
ts02:143 [in Ceres.CeresParserRoundtripProof]
ts02:167 [in Ceres.CeresParserRoundtripProof]
ts0:44 [in Ceres.CeresParserRoundtripProof]
ts1:7 [in Ceres.CeresParserRoundtripProof]
ts2:8 [in Ceres.CeresParserRoundtripProof]
ts:118 [in Ceres.CeresParserRoundtripProof]
ts:17 [in Ceres.CeresParserRoundtripProof]
ts:181 [in Ceres.CeresParserRoundtripProof]
ts:20 [in Ceres.CeresParserRoundtripProof]
ts:22 [in Ceres.CeresParserRoundtripProof]
ts:229 [in Ceres.CeresParserRoundtripProof]
ts:235 [in Ceres.CeresParserRoundtripProof]
ts:24 [in Ceres.CeresParserRoundtrip]
ts:241 [in Ceres.CeresParserRoundtripProof]
ts:26 [in Ceres.CeresParserRoundtrip]
ts:27 [in Ceres.CeresParserRoundtripProof]
ts:28 [in Ceres.CeresParserRoundtrip]
ts:31 [in Ceres.CeresParserRoundtrip]
ts:31 [in Ceres.CeresParserRoundtripProof]
ts:35 [in Ceres.CeresParserRoundtrip]
ts:35 [in Ceres.CeresParserRoundtripProof]
ts:38 [in Ceres.CeresParserRoundtrip]
ts:4 [in Ceres.CeresParserRoundtripProof]
ts:40 [in Ceres.CeresParserRoundtripProof]
ts:43 [in Ceres.CeresParserRoundtripProof]
ts:70 [in Ceres.CeresParserRoundtrip]
ts:79 [in Ceres.CeresParserRoundtrip]
tyname:23 [in Ceres.CeresDeserialize]
tyname:3 [in Ceres.CeresDeserialize]
tyname:32 [in Ceres.CeresDeserialize]
tyname:44 [in Ceres.CeresRoundtrip]
tyname:70 [in Ceres.CeresRoundtrip]
T:12 [in Ceres.CeresParserInternal]
T:16 [in Ceres.CeresParserInternal]
T:184 [in Ceres.CeresParserRoundtripProof]
t:20 [in Ceres.CeresParserInternal]
T:39 [in Ceres.CeresParserInternal]
t:68 [in Ceres.CeresParserRoundtrip]
T:7 [in Ceres.CeresParserInternal]
U
us:39 [in Ceres.CeresParserRoundtripProof]us:42 [in Ceres.CeresParserRoundtripProof]
us:49 [in Ceres.CeresParserRoundtripProof]
us:52 [in Ceres.CeresParserRoundtripProof]
us:55 [in Ceres.CeresParserRoundtripProof]
us:57 [in Ceres.CeresParserRoundtripProof]
us:59 [in Ceres.CeresParserRoundtripProof]
u:106 [in Ceres.CeresParserRoundtripProof]
u:113 [in Ceres.CeresParserRoundtripProof]
u:128 [in Ceres.CeresParserRoundtripProof]
U:13 [in Ceres.CeresParserInternal]
u:139 [in Ceres.CeresParserRoundtripProof]
u:15 [in Ceres.CeresParserInternal]
u:152 [in Ceres.CeresParserRoundtripProof]
u:163 [in Ceres.CeresParserRoundtripProof]
u:178 [in Ceres.CeresParserRoundtripProof]
u:224 [in Ceres.CeresParserRoundtripProof]
u:48 [in Ceres.CeresParserRoundtripProof]
u:54 [in Ceres.CeresParserRoundtripProof]
u:58 [in Ceres.CeresParserRoundtripProof]
V
v:29 [in Ceres.CeresSerialize]v:53 [in Ceres.CeresParserRoundtripProof]
W
ws:36 [in Ceres.CeresParserRoundtrip]X
xs':57 [in Ceres.CeresS]xs:12 [in Ceres.CeresUtils]
xs:149 [in Ceres.CeresRoundtrip]
xs:162 [in Ceres.CeresRoundtrip]
xs:19 [in Ceres.CeresS]
xs:228 [in Ceres.CeresDeserialize]
xs:24 [in Ceres.CeresUtils]
xs:34 [in Ceres.CeresS]
xs:35 [in Ceres.CeresSerialize]
xs:5 [in Ceres.CeresS]
xs:53 [in Ceres.CeresS]
xs:56 [in Ceres.CeresParserRoundtrip]
xs:58 [in Ceres.CeresRoundtrip]
xs:67 [in Ceres.CeresS]
xs:67 [in Ceres.CeresRoundtrip]
xs:71 [in Ceres.CeresS]
xs:73 [in Ceres.CeresString]
x1:47 [in Ceres.CeresS]
x1:58 [in Ceres.CeresS]
x1:60 [in Ceres.CeresS]
x1:62 [in Ceres.CeresS]
x2:48 [in Ceres.CeresS]
x2:59 [in Ceres.CeresS]
x2:61 [in Ceres.CeresS]
x2:63 [in Ceres.CeresS]
x:10 [in Ceres.CeresString]
x:10 [in Ceres.CeresFormat]
x:13 [in Ceres.CeresString]
x:15 [in Ceres.CeresS]
x:2 [in Ceres.CeresString]
x:20 [in Ceres.CeresUtils]
x:25 [in Ceres.CeresUtils]
x:3 [in Ceres.CeresFormat]
x:42 [in Ceres.CeresDeserialize]
x:5 [in Ceres.CeresUtils]
x:55 [in Ceres.CeresParserRoundtrip]
x:6 [in Ceres.CeresString]
X:64 [in Ceres.CeresS]
x:66 [in Ceres.CeresS]
x:68 [in Ceres.CeresRoundtrip]
x:7 [in Ceres.CeresFormat]
x:73 [in Ceres.CeresParserRoundtrip]
x:8 [in Ceres.CeresString]
x:9 [in Ceres.CeresS]
Y
ys:231 [in Ceres.CeresDeserialize]ys:26 [in Ceres.CeresUtils]
ys:35 [in Ceres.CeresS]
ys:58 [in Ceres.CeresParserRoundtrip]
y:11 [in Ceres.CeresString]
y:14 [in Ceres.CeresString]
y:5 [in Ceres.CeresString]
y:57 [in Ceres.CeresParserRoundtrip]
y:7 [in Ceres.CeresString]
y:9 [in Ceres.CeresString]
Z
z:12 [in Ceres.CeresSerialize]z:32 [in Ceres.CeresRoundtrip]
z:63 [in Ceres.CeresParserRoundtrip]
_
_end:88 [in Ceres.CeresString]Module Index
D
Deser [in Ceres.CeresDeserialize]Deser.Notations [in Ceres.CeresDeserialize]
DString [in Ceres.CeresString]
T
Token [in Ceres.CeresParserRoundtrip]Variable Index
E
Example.example_2 [in Ceres.CeresS]Example.example_1 [in Ceres.CeresS]
Library Index
C
CeresCeresDeserialize
CeresFormat
CeresParser
CeresParserInternal
CeresParserRoundtrip
CeresParserRoundtripProof
CeresParserUtils
CeresRoundtrip
CeresS
CeresSerialize
CeresString
CeresUtils
T
TutorialConstructor Index
A
after_atom_cons [in Ceres.CeresParserRoundtrip]after_atom_nil [in Ceres.CeresParserRoundtrip]
atom_token_Str [in Ceres.CeresParserRoundtrip]
atom_token_Num [in Ceres.CeresParserRoundtrip]
atom_token_Raw [in Ceres.CeresParserRoundtrip]
Atom_ [in Ceres.CeresS]
B
Bool [in Tutorial]C
Comment [in Ceres.CeresParserInternal]comment_mk [in Ceres.CeresParserRoundtrip]
complete_integral [in Ceres.CeresRoundtrip]
complete_class [in Ceres.CeresRoundtrip]
D
DeserError [in Ceres.CeresDeserialize]Deser._from_sexp_list [in Ceres.CeresDeserialize]
E
EmptyInput [in Ceres.CeresParserUtils]EscBackslash [in Ceres.CeresParserInternal]
EscNone [in Ceres.CeresParserInternal]
Exp [in Ceres.CeresParserInternal]
F
from_Z [in Ceres.CeresDeserialize]I
If [in Tutorial]InvalidChar [in Ceres.CeresParserUtils]
InvalidStringChar [in Ceres.CeresParserUtils]
L
List [in Ceres.CeresS]list_tokens_cons [in Ceres.CeresParserRoundtrip]
list_tokens_nil [in Ceres.CeresParserRoundtrip]
M
MkUnconsFields [in Ceres.CeresRoundtrip]MkUnnilFields [in Ceres.CeresRoundtrip]
more_ok_true [in Ceres.CeresParserRoundtrip]
more_ok_false [in Ceres.CeresParserRoundtrip]
MsgApp [in Ceres.CeresDeserialize]
MsgSexp [in Ceres.CeresDeserialize]
MsgStr [in Ceres.CeresDeserialize]
N
NoToken [in Ceres.CeresParserInternal]Num [in Ceres.CeresS]
Number [in Tutorial]
O
Open [in Ceres.CeresParserInternal]P
ParseError [in Ceres.CeresDeserialize]parser_state_string_mk [in Ceres.CeresParserRoundtripProof]
parser_state_string_mk_ [in Ceres.CeresParserRoundtripProof]
partial_token_string_Comment [in Ceres.CeresParserRoundtripProof]
partial_token_string_StrToken [in Ceres.CeresParserRoundtripProof]
partial_token_string_SimpleToken [in Ceres.CeresParserRoundtripProof]
partial_token_string_NoToken [in Ceres.CeresParserRoundtripProof]
Plus [in Tutorial]
R
Raw [in Ceres.CeresS]reflect_eq_false [in Ceres.CeresString]
reflect_eq_true [in Ceres.CeresString]
S
sexp_tokens_List [in Ceres.CeresParserRoundtrip]sexp_tokens_Atom [in Ceres.CeresParserRoundtrip]
SimpleToken [in Ceres.CeresParserInternal]
sound_integral [in Ceres.CeresRoundtrip]
sound_class [in Ceres.CeresRoundtrip]
stack_end_nonempty [in Ceres.CeresParserRoundtripProof]
stack_end_nil [in Ceres.CeresParserRoundtripProof]
stack_end_last_cons [in Ceres.CeresParserRoundtripProof]
stack_end_last_last [in Ceres.CeresParserRoundtripProof]
stack_tokens_sexp [in Ceres.CeresParserRoundtripProof]
stack_tokens_open [in Ceres.CeresParserRoundtripProof]
stack_tokens_nil [in Ceres.CeresParserRoundtripProof]
Str [in Ceres.CeresS]
StrToken [in Ceres.CeresParserInternal]
str_token_string_EscNone [in Ceres.CeresParserRoundtripProof]
str_token_string_EscBackslash [in Ceres.CeresParserRoundtripProof]
T
token_string_comment [in Ceres.CeresParserRoundtrip]token_string_spaces [in Ceres.CeresParserRoundtrip]
token_string_string [in Ceres.CeresParserRoundtrip]
token_string_atom [in Ceres.CeresParserRoundtrip]
token_string_close [in Ceres.CeresParserRoundtrip]
token_string_open [in Ceres.CeresParserRoundtrip]
token_string_nil [in Ceres.CeresParserRoundtrip]
Token.Atom [in Ceres.CeresParserRoundtrip]
Token.Close [in Ceres.CeresParserRoundtrip]
Token.Open [in Ceres.CeresParserRoundtrip]
Token.Str [in Ceres.CeresParserRoundtrip]
to_Z [in Ceres.CeresSerialize]
to_sexp [in Ceres.CeresSerialize]
U
UnknownEscape [in Ceres.CeresParserUtils]UnmatchedClose [in Ceres.CeresParserUtils]
UnmatchedOpen [in Ceres.CeresParserUtils]
UnterminatedString [in Ceres.CeresParserUtils]
_
_from_sexp [in Ceres.CeresDeserialize]Lemma Index
A
after_atom_string_cons [in Ceres.CeresParserRoundtrip]after_atom_string_nil_inv [in Ceres.CeresParserRoundtrip]
after_atom_string_snoc [in Ceres.CeresParserRoundtripProof]
app_cons_assoc [in Ceres.CeresUtils]
atom_token_atom [in Ceres.CeresParserRoundtripProof]
C
complete_class_list [in Ceres.CeresRoundtrip]E
eof_sound [in Ceres.CeresParserRoundtripProof]eqb_eq_string [in Ceres.CeresString]
eqb_eq_ascii' [in Ceres.CeresString]
eqb_eq_ascii [in Ceres.CeresString]
eqb_eq_bool' [in Ceres.CeresString]
eqb_eq_bool [in Ceres.CeresString]
eqb_eq_sexp_ [in Ceres.CeresS]
eqb_eq_atom [in Ceres.CeresS]
eqb_eq_list [in Ceres.CeresS]
escape_string_regular [in Ceres.CeresParserRoundtripProof]
escape_string_dquote [in Ceres.CeresParserRoundtripProof]
escape_string_backslash [in Ceres.CeresParserRoundtripProof]
escape_string_newline [in Ceres.CeresParserRoundtripProof]
F
forall_Forall [in Ceres.CeresS]I
is_atom_app [in Ceres.CeresParserRoundtripProof]is_atom_singleton [in Ceres.CeresParserRoundtripProof]
L
list_sexp_tokens_app [in Ceres.CeresParserRoundtripProof]list_sexp_tokens_singleton [in Ceres.CeresParserRoundtripProof]
List_Exists_impl [in Ceres.CeresRoundtrip]
M
more_ok_cons [in Ceres.CeresParserRoundtrip]more_ok_nil_inv [in Ceres.CeresParserRoundtrip]
more_ok_atom [in Ceres.CeresParserRoundtripProof]
more_ok_atom_inv [in Ceres.CeresParserRoundtripProof]
more_ok_str_token [in Ceres.CeresParserRoundtripProof]
N
neqb_neq_ascii [in Ceres.CeresString]new_sexp_Str_sound [in Ceres.CeresParserRoundtripProof]
new_sexp_List_sound [in Ceres.CeresParserRoundtripProof]
new_sexp_Atom_sound [in Ceres.CeresParserRoundtripProof]
next_sound [in Ceres.CeresParserRoundtripProof]
next_comment_sound [in Ceres.CeresParserRoundtripProof]
next_str_sound [in Ceres.CeresParserRoundtripProof]
next_sound' [in Ceres.CeresParserRoundtripProof]
not_string_elem_singleton [in Ceres.CeresString]
not_string_elem_head [in Ceres.CeresString]
not_string_elem_app [in Ceres.CeresString]
P
parser_state_empty [in Ceres.CeresParserRoundtripProof]parser_state_string_map [in Ceres.CeresParserRoundtripProof]
parse_sexps_sound [in Ceres.CeresParserRoundtripProof]
S
sexp__ind [in Ceres.CeresS]sound_class_list [in Ceres.CeresRoundtrip]
sound_bind_field [in Ceres.CeresRoundtrip]
sound_ret_field [in Ceres.CeresRoundtrip]
sound_match_con [in Ceres.CeresRoundtrip]
sound__con [in Ceres.CeresRoundtrip]
stack_end_inv [in Ceres.CeresParserRoundtripProof]
stack_end_cons_Open [in Ceres.CeresParserRoundtripProof]
stack_end_cons [in Ceres.CeresParserRoundtripProof]
string_app_nil_r [in Ceres.CeresString]
string_reverse_cons' [in Ceres.CeresParserRoundtripProof]
string_reverse_cons [in Ceres.CeresParserRoundtripProof]
string_app_assoc [in Ceres.CeresParserRoundtripProof]
str_token_string_regular [in Ceres.CeresParserRoundtripProof]
str_token_string_escape [in Ceres.CeresParserRoundtripProof]
str_token_string_dquote [in Ceres.CeresParserRoundtripProof]
str_token_string_backslash [in Ceres.CeresParserRoundtripProof]
str_token_string_newline [in Ceres.CeresParserRoundtripProof]
str_token_string_new [in Ceres.CeresParserRoundtripProof]
T
token_string_spaces_app [in Ceres.CeresParserRoundtripProof]token_string_string_snoc [in Ceres.CeresParserRoundtripProof]
token_string_comment_snoc [in Ceres.CeresParserRoundtripProof]
token_string_newline_snoc [in Ceres.CeresParserRoundtripProof]
token_string_atom_snoc [in Ceres.CeresParserRoundtripProof]
token_string_close_snoc [in Ceres.CeresParserRoundtripProof]
token_string_open_snoc [in Ceres.CeresParserRoundtripProof]
W
whitespace_no_atom [in Ceres.CeresParserRoundtripProof]_
_parse_sexps_sound [in Ceres.CeresParserRoundtripProof]_done_or_fail_sound [in Ceres.CeresParserRoundtripProof]
_fold_stack_sound [in Ceres.CeresParserRoundtripProof]
_fold_stack_sound_ [in Ceres.CeresParserRoundtripProof]
_string_reverse_app [in Ceres.CeresParserRoundtripProof]
_find_or_spec [in Ceres.CeresRoundtrip]
Projection Index
C
complete_integral [in Ceres.CeresRoundtrip]complete_class [in Ceres.CeresRoundtrip]
D
Deser._from_sexp_list [in Ceres.CeresDeserialize]F
from_Z [in Ceres.CeresDeserialize]P
parser_cur_token [in Ceres.CeresParserInternal]parser_stack [in Ceres.CeresParserInternal]
parser_done [in Ceres.CeresParserInternal]
S
sound_integral [in Ceres.CeresRoundtrip]sound_class [in Ceres.CeresRoundtrip]
T
to_Z [in Ceres.CeresSerialize]to_sexp [in Ceres.CeresSerialize]
_
_fields [in Ceres.CeresDeserialize]_from_sexp [in Ceres.CeresDeserialize]
Inductive Index
A
after_atom_string [in Ceres.CeresParserRoundtrip]atom [in Ceres.CeresS]
atom_token [in Ceres.CeresParserRoundtrip]
C
comment [in Ceres.CeresParserRoundtrip]CompleteClass [in Ceres.CeresRoundtrip]
CompleteIntegral [in Ceres.CeresRoundtrip]
D
Deserialize [in Ceres.CeresDeserialize]Deser.DeserFromSexpList [in Ceres.CeresDeserialize]
E
error [in Ceres.CeresDeserialize]error [in Ceres.CeresParserUtils]
escape [in Ceres.CeresParserInternal]
I
Integral [in Ceres.CeresSerialize]L
list_tokens [in Ceres.CeresParserRoundtrip]M
message [in Ceres.CeresDeserialize]more_ok [in Ceres.CeresParserRoundtrip]
P
parser_state_string [in Ceres.CeresParserRoundtripProof]parser_state_string_ [in Ceres.CeresParserRoundtripProof]
partial_token [in Ceres.CeresParserInternal]
partial_token_string [in Ceres.CeresParserRoundtripProof]
R
reflect_eq [in Ceres.CeresString]S
SemiIntegral [in Ceres.CeresDeserialize]Serialize [in Ceres.CeresSerialize]
sexp_tokens [in Ceres.CeresParserRoundtrip]
sexp_ [in Ceres.CeresS]
SoundClass [in Ceres.CeresRoundtrip]
SoundIntegral [in Ceres.CeresRoundtrip]
stack_end [in Ceres.CeresParserRoundtripProof]
stack_end_last [in Ceres.CeresParserRoundtripProof]
stack_tokens [in Ceres.CeresParserRoundtripProof]
str_token_string [in Ceres.CeresParserRoundtripProof]
symbol [in Ceres.CeresParserInternal]
T
t [in Tutorial]token_string [in Ceres.CeresParserRoundtrip]
Token.t [in Ceres.CeresParserRoundtrip]
U
UnconsFields [in Ceres.CeresRoundtrip]UnnilFields [in Ceres.CeresRoundtrip]
Instance Index
C
CompleteClass_ascii [in Ceres.CeresRoundtrip]CompleteClass_string [in Ceres.CeresRoundtrip]
CompleteClass_list [in Ceres.CeresRoundtrip]
CompleteClass_prod [in Ceres.CeresRoundtrip]
CompleteClass_sum [in Ceres.CeresRoundtrip]
CompleteClass_option [in Ceres.CeresRoundtrip]
CompleteClass_bool [in Ceres.CeresRoundtrip]
CompleteClass_Integral [in Ceres.CeresRoundtrip]
Complete_nat [in Ceres.CeresRoundtrip]
Complete_N [in Ceres.CeresRoundtrip]
Complete_Z [in Ceres.CeresRoundtrip]
D
Decidable_eq_string [in Ceres.CeresString]Decidable_eq_ascii [in Ceres.CeresString]
Decidable_eq_sexp [in Ceres.CeresS]
Decidable_eq_atom [in Ceres.CeresS]
Deserialize_sexp [in Ceres.CeresDeserialize]
Deserialize_list [in Ceres.CeresDeserialize]
Deserialize_ascii [in Ceres.CeresDeserialize]
Deserialize_string [in Ceres.CeresDeserialize]
Deserialize_unit [in Ceres.CeresDeserialize]
Deserialize_Empty_set [in Ceres.CeresDeserialize]
Deserialize_prod [in Ceres.CeresDeserialize]
Deserialize_sum [in Ceres.CeresDeserialize]
Deserialize_option [in Ceres.CeresDeserialize]
Deserialize_bool [in Ceres.CeresDeserialize]
Deserialize_SemiIntegral [in Ceres.CeresDeserialize]
Deserialize_t [in Tutorial]
Deser.DeserFromSexpList_S [in Ceres.CeresDeserialize]
Deser.DeserFromSexpList_0 [in Ceres.CeresDeserialize]
I
Integral_Z [in Ceres.CeresSerialize]Integral_N [in Ceres.CeresSerialize]
Integral_nat [in Ceres.CeresSerialize]
S
SemiIntegral_nat [in Ceres.CeresDeserialize]SemiIntegral_N [in Ceres.CeresDeserialize]
SemiIntegral_Z [in Ceres.CeresDeserialize]
Serialize_sexp [in Ceres.CeresSerialize]
Serialize_list [in Ceres.CeresSerialize]
Serialize_string [in Ceres.CeresSerialize]
Serialize_ascii [in Ceres.CeresSerialize]
Serialize_unit [in Ceres.CeresSerialize]
Serialize_Empty_set [in Ceres.CeresSerialize]
Serialize_product [in Ceres.CeresSerialize]
Serialize_sum [in Ceres.CeresSerialize]
Serialize_option [in Ceres.CeresSerialize]
Serialize_bool [in Ceres.CeresSerialize]
Serialize_Integral [in Ceres.CeresSerialize]
Serialize_t [in Tutorial]
SoundClass_ascii [in Ceres.CeresRoundtrip]
SoundClass_string [in Ceres.CeresRoundtrip]
SoundClass_list [in Ceres.CeresRoundtrip]
SoundClass_prod [in Ceres.CeresRoundtrip]
SoundClass_sum [in Ceres.CeresRoundtrip]
SoundClass_option [in Ceres.CeresRoundtrip]
SoundClass_bool [in Ceres.CeresRoundtrip]
SoundClass_Integral [in Ceres.CeresRoundtrip]
Sound_nat [in Ceres.CeresRoundtrip]
Sound_N [in Ceres.CeresRoundtrip]
Sound_Z [in Ceres.CeresRoundtrip]
Section Index
A
AsciiTest [in Ceres.CeresString]D
DeBindField [in Ceres.CeresRoundtrip]DeRetField [in Ceres.CeresRoundtrip]
E
Example [in Ceres.CeresS]Abbreviation Index
A
Atom [in Ceres.CeresS]L
list_sexp_tokens [in Ceres.CeresParserRoundtrip]N
newline [in Ceres.CeresString]S
sexp [in Ceres.CeresS]Record Index
C
CompleteClass [in Ceres.CeresRoundtrip]CompleteIntegral [in Ceres.CeresRoundtrip]
D
Deserialize [in Ceres.CeresDeserialize]Deser.DeserFromSexpList [in Ceres.CeresDeserialize]
F
FromSexpListN [in Ceres.CeresDeserialize]I
Integral [in Ceres.CeresSerialize]P
parser_state_ [in Ceres.CeresParserInternal]S
SemiIntegral [in Ceres.CeresDeserialize]Serialize [in Ceres.CeresSerialize]
SoundClass [in Ceres.CeresRoundtrip]
SoundIntegral [in Ceres.CeresRoundtrip]
Definition Index
A
ascii_compare [in Ceres.CeresString]atom_string [in Ceres.CeresParserRoundtrip]
C
comma_sep [in Ceres.CeresString]compb [in Ceres.CeresString]
compcomp [in Ceres.CeresString]
Complete [in Ceres.CeresRoundtrip]
D
Deser.as_fun [in Ceres.CeresDeserialize]Deser.bind_field [in Ceres.CeresDeserialize]
Deser.con_ [in Ceres.CeresDeserialize]
Deser.con0 [in Ceres.CeresDeserialize]
Deser.con1 [in Ceres.CeresDeserialize]
Deser.con1_ [in Ceres.CeresDeserialize]
Deser.con2 [in Ceres.CeresDeserialize]
Deser.con2_ [in Ceres.CeresDeserialize]
Deser.con3 [in Ceres.CeresDeserialize]
Deser.con3_ [in Ceres.CeresDeserialize]
Deser.con4 [in Ceres.CeresDeserialize]
Deser.con4_ [in Ceres.CeresDeserialize]
Deser.con5 [in Ceres.CeresDeserialize]
Deser.con5_ [in Ceres.CeresDeserialize]
Deser.fields [in Ceres.CeresDeserialize]
Deser.match_con [in Ceres.CeresDeserialize]
Deser.ret [in Ceres.CeresDeserialize]
Deser._con [in Ceres.CeresDeserialize]
digit_of_ascii [in Ceres.CeresString]
dstring_of_sexp [in Ceres.CeresFormat]
DString.app_string [in Ceres.CeresString]
DString.of_ascii [in Ceres.CeresString]
DString.of_string [in Ceres.CeresString]
DString.t [in Ceres.CeresString]
E
eof [in Ceres.CeresParserInternal]eqb_string [in Ceres.CeresString]
eqb_eq [in Ceres.CeresString]
eqb_ascii [in Ceres.CeresString]
eqb_eq_sexp [in Ceres.CeresS]
eqb_sexp [in Ceres.CeresS]
eqb_atom [in Ceres.CeresS]
eqb_sexp_ [in Ceres.CeresS]
eqb_list [in Ceres.CeresS]
escape_string [in Ceres.CeresString]
escape_to_string [in Ceres.CeresParserRoundtripProof]
example1 [in Tutorial]
example2 [in Tutorial]
F
FromSexp [in Ceres.CeresDeserialize]FromSexpList [in Ceres.CeresDeserialize]
from_string [in Ceres.CeresDeserialize]
from_sexp [in Ceres.CeresDeserialize]
G
get_one [in Ceres.CeresParserInternal]get_done [in Ceres.CeresParserInternal]
get_Raw [in Ceres.CeresS]
get_Str [in Ceres.CeresS]
get_Num [in Ceres.CeresS]
I
initial_state [in Ceres.CeresParserInternal]is_atom_char [in Ceres.CeresParserUtils]
is_alphanum [in Ceres.CeresString]
is_lower [in Ceres.CeresString]
is_upper [in Ceres.CeresString]
is_digit [in Ceres.CeresString]
is_whitespace [in Ceres.CeresString]
is_printable [in Ceres.CeresString]
L
leb_ascii [in Ceres.CeresString]loc [in Ceres.CeresDeserialize]
loc [in Ceres.CeresParserUtils]
M
map_sum [in Ceres.CeresUtils]map_sexp_ [in Ceres.CeresS]
N
new_sexp [in Ceres.CeresParserInternal]next [in Ceres.CeresParserInternal]
next_comment [in Ceres.CeresParserInternal]
next_str [in Ceres.CeresParserInternal]
next' [in Ceres.CeresParserInternal]
no_newline [in Ceres.CeresParserRoundtripProof]
O
on_right [in Ceres.CeresParserRoundtrip]P
parser_state [in Ceres.CeresParserInternal]parse_sexps_ [in Ceres.CeresParserInternal]
PARSE_SEXPS_SOUND [in Ceres.CeresParserRoundtrip]
parse_sexp [in Ceres.CeresParser]
parse_sexps [in Ceres.CeresParser]
pretty_error [in Ceres.CeresParserUtils]
pretty_loc [in Ceres.CeresParserUtils]
R
raw_or_num [in Ceres.CeresParserInternal]S
set_cur_token [in Ceres.CeresParserInternal]sexp_of_atoms [in Ceres.CeresS]
Sound [in Ceres.CeresRoundtrip]
string_string [in Ceres.CeresParserRoundtrip]
string_of_bool [in Ceres.CeresString]
string_of_N [in Ceres.CeresString]
string_of_Z [in Ceres.CeresString]
string_of_nat [in Ceres.CeresString]
string_reverse [in Ceres.CeresString]
string_forall [in Ceres.CeresString]
string_elem [in Ceres.CeresString]
string_of_sexp [in Ceres.CeresFormat]
string_of_atom [in Ceres.CeresFormat]
string_of_sexp_ [in Ceres.CeresFormat]
subst_sexp_ [in Ceres.CeresS]
T
to_string [in Ceres.CeresSerialize]type_error [in Ceres.CeresDeserialize]
U
unescape_string [in Ceres.CeresString]W
whitespaces [in Ceres.CeresParserRoundtrip]_
_sexp_to_list [in Ceres.CeresDeserialize]_bind_sum [in Ceres.CeresUtils]
_find_or [in Ceres.CeresUtils]
_done_or_fail [in Ceres.CeresParserInternal]
_fold_stack [in Ceres.CeresParserInternal]
_unescape_string [in Ceres.CeresString]
_unthree_digit [in Ceres.CeresString]
_escape_string [in Ceres.CeresString]
_three_digit [in Ceres.CeresString]
_units_digit [in Ceres.CeresString]
_string_reverse [in Ceres.CeresString]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1310 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (887 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (80 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (77 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (36 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (58 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (110 entries) |