| 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 | (628 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 | (2 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 | (491 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 | (1 entry) |
| 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 | (2 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 | (12 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 | (1 entry) |
| 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 | (8 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 | (5 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 | (104 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 | (2 entries) |
Global Index
A
AbstractReflectionDefinitions [section, in Arith.GeneralReflection]addRelIndex [definition, in Arith.GeneralReflection]
amnt:43 [binder, in Arith.GeneralReflection]
appendAndLift [definition, in Arith.GeneralReflection]
appendZero [definition, in Arith.GeneralReflection]
applyRecursively [definition, in Arith.GeneralReflection]
applyRecursivelyNP [definition, in Arith.GeneralReflection]
atrIH:356 [binder, in Arith.GeneralReflection]
av:367 [binder, in Arith.GeneralReflection]
av:374 [binder, in Arith.GeneralReflection]
av:381 [binder, in Arith.GeneralReflection]
av:387 [binder, in Arith.GeneralReflection]
A':151 [binder, in Arith.GeneralReflection]
A:1 [binder, in Arith.GeneralReflection]
a:11 [binder, in Arith.GeneralReflection]
A:13 [binder, in Arith.GeneralReflection]
A:133 [binder, in Arith.GeneralReflection]
A:149 [binder, in Arith.GeneralReflection]
a:161 [binder, in Arith.GeneralReflection]
A:19 [binder, in Arith.GeneralReflection]
A:23 [binder, in Arith.GeneralReflection]
A:4 [binder, in Arith.GeneralReflection]
a:408 [binder, in Arith.GeneralReflection]
a:471 [binder, in Arith.GeneralReflection]
a:48 [binder, in Arith.GeneralReflection]
A:50 [binder, in Arith.GeneralReflection]
a:78 [binder, in Arith.GeneralReflection]
B
baseConnectiveReifier [definition, in Arith.GeneralReflection]baseConnectiveReifierNP [definition, in Arith.GeneralReflection]
baseConnectiveVars [definition, in Arith.GeneralReflection]
baseEnv:593 [binder, in Arith.GeneralReflection]
baseLogicConn [abbreviation, in Arith.GeneralReflection]
baseLogicConn [abbreviation, in Arith.GeneralReflection]
baseLogicConn [abbreviation, in Arith.GeneralReflection]
baseLogicConnHelper [projection, in Arith.GeneralReflection]
baseLogicVarHelper [projection, in Arith.GeneralReflection]
base:468 [binder, in Arith.GeneralReflection]
bind [definition, in Arith.GeneralReflection]
bodyf:53 [binder, in Arith.GeneralReflection]
both:349 [binder, in Arith.GeneralReflection]
buildDefaultTarski [definition, in Arith.GeneralReflection]
B':152 [binder, in Arith.GeneralReflection]
B:150 [binder, in Arith.GeneralReflection]
b:162 [binder, in Arith.GeneralReflection]
B:20 [binder, in Arith.GeneralReflection]
b:47 [binder, in Arith.GeneralReflection]
B:5 [binder, in Arith.GeneralReflection]
B:51 [binder, in Arith.GeneralReflection]
b:77 [binder, in Arith.GeneralReflection]
C
constructForm [definition, in Arith.GeneralReflection]constructTerm [definition, in Arith.GeneralReflection]
createEnvTerms [definition, in Arith.GeneralReflection]
C':154 [binder, in Arith.GeneralReflection]
C:153 [binder, in Arith.GeneralReflection]
c:165 [binder, in Arith.GeneralReflection]
c:184 [binder, in Arith.GeneralReflection]
c:185 [binder, in Arith.GeneralReflection]
c:204 [binder, in Arith.GeneralReflection]
c:365 [binder, in Arith.GeneralReflection]
c:372 [binder, in Arith.GeneralReflection]
c:379 [binder, in Arith.GeneralReflection]
c:385 [binder, in Arith.GeneralReflection]
D
D [projection, in Arith.GeneralReflection]dbr:56 [binder, in Arith.GeneralReflection]
defaultExtensions [definition, in Arith.GeneralReflection]
dtr:55 [binder, in Arith.GeneralReflection]
D:103 [binder, in Arith.GeneralReflection]
d:121 [binder, in Arith.GeneralReflection]
d:126 [binder, in Arith.GeneralReflection]
d:129 [binder, in Arith.GeneralReflection]
d:168 [binder, in Arith.GeneralReflection]
d:170 [binder, in Arith.GeneralReflection]
d:176 [binder, in Arith.GeneralReflection]
d:178 [binder, in Arith.GeneralReflection]
d:190 [binder, in Arith.GeneralReflection]
d:198 [binder, in Arith.GeneralReflection]
d:406 [binder, in Arith.GeneralReflection]
d:54 [binder, in Arith.GeneralReflection]
E
emptyEnv [projection, in Arith.GeneralReflection]EnvConstructor [section, in Arith.GeneralReflection]
EnvHelpers [section, in Arith.GeneralReflection]
envSub:530 [binder, in Arith.GeneralReflection]
envSub:564 [binder, in Arith.GeneralReflection]
envTermSub:529 [binder, in Arith.GeneralReflection]
envTermSub:563 [binder, in Arith.GeneralReflection]
envTerm:241 [binder, in Arith.GeneralReflection]
envTerm:247 [binder, in Arith.GeneralReflection]
envTerm:255 [binder, in Arith.GeneralReflection]
envTerm:263 [binder, in Arith.GeneralReflection]
envTerm:271 [binder, in Arith.GeneralReflection]
envTerm:280 [binder, in Arith.GeneralReflection]
envTerm:288 [binder, in Arith.GeneralReflection]
envTerm:294 [binder, in Arith.GeneralReflection]
envTerm:302 [binder, in Arith.GeneralReflection]
envTerm:310 [binder, in Arith.GeneralReflection]
envTerm:317 [binder, in Arith.GeneralReflection]
envTerm:326 [binder, in Arith.GeneralReflection]
envTerm:335 [binder, in Arith.GeneralReflection]
envTerm:513 [binder, in Arith.GeneralReflection]
envTerm:537 [binder, in Arith.GeneralReflection]
envToD:595 [binder, in Arith.GeneralReflection]
envv:482 [binder, in Arith.GeneralReflection]
envv:496 [binder, in Arith.GeneralReflection]
env:242 [binder, in Arith.GeneralReflection]
env:248 [binder, in Arith.GeneralReflection]
env:256 [binder, in Arith.GeneralReflection]
env:264 [binder, in Arith.GeneralReflection]
env:272 [binder, in Arith.GeneralReflection]
env:281 [binder, in Arith.GeneralReflection]
env:289 [binder, in Arith.GeneralReflection]
env:295 [binder, in Arith.GeneralReflection]
env:303 [binder, in Arith.GeneralReflection]
env:311 [binder, in Arith.GeneralReflection]
env:318 [binder, in Arith.GeneralReflection]
env:327 [binder, in Arith.GeneralReflection]
env:336 [binder, in Arith.GeneralReflection]
env:342 [binder, in Arith.GeneralReflection]
env:368 [binder, in Arith.GeneralReflection]
env:375 [binder, in Arith.GeneralReflection]
env:382 [binder, in Arith.GeneralReflection]
env:388 [binder, in Arith.GeneralReflection]
env:391 [binder, in Arith.GeneralReflection]
env:397 [binder, in Arith.GeneralReflection]
env:407 [binder, in Arith.GeneralReflection]
env:479 [binder, in Arith.GeneralReflection]
env:493 [binder, in Arith.GeneralReflection]
env:514 [binder, in Arith.GeneralReflection]
env:538 [binder, in Arith.GeneralReflection]
eT:341 [binder, in Arith.GeneralReflection]
et:346 [binder, in Arith.GeneralReflection]
et:543 [binder, in Arith.GeneralReflection]
et:548 [binder, in Arith.GeneralReflection]
e':501 [binder, in Arith.GeneralReflection]
e:347 [binder, in Arith.GeneralReflection]
e:544 [binder, in Arith.GeneralReflection]
e:549 [binder, in Arith.GeneralReflection]
F
fail [constructor, in Arith.GeneralReflection]FailureMonad [inductive, in Arith.GeneralReflection]
FailureMonad [section, in Arith.GeneralReflection]
_ <- _ ;; _ [notation, in Arith.GeneralReflection]
fallback:485 [binder, in Arith.GeneralReflection]
fallback:505 [binder, in Arith.GeneralReflection]
ffail:30 [binder, in Arith.GeneralReflection]
ffail:422 [binder, in Arith.GeneralReflection]
ffail:459 [binder, in Arith.GeneralReflection]
ffail:518 [binder, in Arith.GeneralReflection]
ffail:553 [binder, in Arith.GeneralReflection]
ff:74 [binder, in Arith.GeneralReflection]
findPropRepresentation [definition, in Arith.GeneralReflection]
findPropRepresentationNP [definition, in Arith.GeneralReflection]
findTermRepresentation [definition, in Arith.GeneralReflection]
findTermRepresentationNP [definition, in Arith.GeneralReflection]
findUBAnd [definition, in Arith.GeneralReflection]
findUBBase [definition, in Arith.GeneralReflection]
findUBExists [definition, in Arith.GeneralReflection]
findUBFalse [definition, in Arith.GeneralReflection]
findUBIff [definition, in Arith.GeneralReflection]
findUBOr [definition, in Arith.GeneralReflection]
findUBRecursively [definition, in Arith.GeneralReflection]
findUBTrue [definition, in Arith.GeneralReflection]
findUnboundVariablesForm [definition, in Arith.GeneralReflection]
findUnboundVariablesTerm [definition, in Arith.GeneralReflection]
flatten_monad [definition, in Arith.GeneralReflection]
formReifierReifyHelper [projection, in Arith.GeneralReflection]
formReifierVarHelper [projection, in Arith.GeneralReflection]
fPR:243 [binder, in Arith.GeneralReflection]
fPR:249 [binder, in Arith.GeneralReflection]
fPR:257 [binder, in Arith.GeneralReflection]
fPR:265 [binder, in Arith.GeneralReflection]
fPR:273 [binder, in Arith.GeneralReflection]
fPR:282 [binder, in Arith.GeneralReflection]
fPR:290 [binder, in Arith.GeneralReflection]
fPR:296 [binder, in Arith.GeneralReflection]
fPR:304 [binder, in Arith.GeneralReflection]
fPR:312 [binder, in Arith.GeneralReflection]
fPR:319 [binder, in Arith.GeneralReflection]
fPR:328 [binder, in Arith.GeneralReflection]
fPR:337 [binder, in Arith.GeneralReflection]
fPR:426 [binder, in Arith.GeneralReflection]
fPR:429 [binder, in Arith.GeneralReflection]
fPR:434 [binder, in Arith.GeneralReflection]
fPR:439 [binder, in Arith.GeneralReflection]
fPR:446 [binder, in Arith.GeneralReflection]
fP:211 [binder, in Arith.GeneralReflection]
fP:216 [binder, in Arith.GeneralReflection]
fP:220 [binder, in Arith.GeneralReflection]
fP:225 [binder, in Arith.GeneralReflection]
fP:234 [binder, in Arith.GeneralReflection]
fP:236 [binder, in Arith.GeneralReflection]
fQ:212 [binder, in Arith.GeneralReflection]
fQ:217 [binder, in Arith.GeneralReflection]
fQ:226 [binder, in Arith.GeneralReflection]
fQ:235 [binder, in Arith.GeneralReflection]
fQ:237 [binder, in Arith.GeneralReflection]
frees:457 [binder, in Arith.GeneralReflection]
frees:512 [binder, in Arith.GeneralReflection]
frees:536 [binder, in Arith.GeneralReflection]
fs [projection, in Arith.GeneralReflection]
fs:101 [binder, in Arith.GeneralReflection]
fTR:338 [binder, in Arith.GeneralReflection]
FUEL [definition, in Arith.GeneralReflection]
fuel:279 [binder, in Arith.GeneralReflection]
fuel:325 [binder, in Arith.GeneralReflection]
fuel:334 [binder, in Arith.GeneralReflection]
fuel:417 [binder, in Arith.GeneralReflection]
fuel:442 [binder, in Arith.GeneralReflection]
fuel:455 [binder, in Arith.GeneralReflection]
fuel:476 [binder, in Arith.GeneralReflection]
fuel:490 [binder, in Arith.GeneralReflection]
fuel:510 [binder, in Arith.GeneralReflection]
fuel:534 [binder, in Arith.GeneralReflection]
fZ:173 [binder, in Arith.GeneralReflection]
fZ:182 [binder, in Arith.GeneralReflection]
fZ:193 [binder, in Arith.GeneralReflection]
fZ:202 [binder, in Arith.GeneralReflection]
F1:24 [binder, in Arith.GeneralReflection]
f2t [definition, in Arith.GeneralReflection]
F2:25 [binder, in Arith.GeneralReflection]
f:21 [binder, in Arith.GeneralReflection]
f:28 [binder, in Arith.GeneralReflection]
f:547 [binder, in Arith.GeneralReflection]
f:7 [binder, in Arith.GeneralReflection]
G
GeneralReflection [library]g:567 [binder, in Arith.GeneralReflection]
g:579 [binder, in Arith.GeneralReflection]
g:589 [binder, in Arith.GeneralReflection]
H
helperFormReifierType [definition, in Arith.GeneralReflection]helperFormVarsType [definition, in Arith.GeneralReflection]
helperTermReifierType [definition, in Arith.GeneralReflection]
helperTermVarsType [definition, in Arith.GeneralReflection]
HiddenTerm [definition, in Arith.GeneralReflection]
I
I [projection, in Arith.GeneralReflection]ifZ:174 [binder, in Arith.GeneralReflection]
ifZ:183 [binder, in Arith.GeneralReflection]
ifZ:194 [binder, in Arith.GeneralReflection]
ifZ:203 [binder, in Arith.GeneralReflection]
IHt:355 [binder, in Arith.GeneralReflection]
IH:352 [binder, in Arith.GeneralReflection]
IH:360 [binder, in Arith.GeneralReflection]
IH:369 [binder, in Arith.GeneralReflection]
IH:376 [binder, in Arith.GeneralReflection]
IH:383 [binder, in Arith.GeneralReflection]
IH:389 [binder, in Arith.GeneralReflection]
IH:412 [binder, in Arith.GeneralReflection]
isD [projection, in Arith.GeneralReflection]
isD:106 [binder, in Arith.GeneralReflection]
I:104 [binder, in Arith.GeneralReflection]
K
k:146 [binder, in Arith.GeneralReflection]k:147 [binder, in Arith.GeneralReflection]
k:396 [binder, in Arith.GeneralReflection]
k:402 [binder, in Arith.GeneralReflection]
k:403 [binder, in Arith.GeneralReflection]
k:531 [binder, in Arith.GeneralReflection]
k:6 [binder, in Arith.GeneralReflection]
L
lowerRelIndex [definition, in Arith.GeneralReflection]lst:240 [binder, in Arith.GeneralReflection]
lst:246 [binder, in Arith.GeneralReflection]
lst:254 [binder, in Arith.GeneralReflection]
lst:262 [binder, in Arith.GeneralReflection]
lst:270 [binder, in Arith.GeneralReflection]
lst:287 [binder, in Arith.GeneralReflection]
lst:293 [binder, in Arith.GeneralReflection]
lst:301 [binder, in Arith.GeneralReflection]
lst:309 [binder, in Arith.GeneralReflection]
lst:316 [binder, in Arith.GeneralReflection]
lst:333 [binder, in Arith.GeneralReflection]
lst:425 [binder, in Arith.GeneralReflection]
lst:428 [binder, in Arith.GeneralReflection]
lst:433 [binder, in Arith.GeneralReflection]
lst:438 [binder, in Arith.GeneralReflection]
lst:441 [binder, in Arith.GeneralReflection]
lst:445 [binder, in Arith.GeneralReflection]
lst:594 [binder, in Arith.GeneralReflection]
ls:37 [binder, in Arith.GeneralReflection]
lt:351 [binder, in Arith.GeneralReflection]
lt:359 [binder, in Arith.GeneralReflection]
lt:411 [binder, in Arith.GeneralReflection]
l:14 [binder, in Arith.GeneralReflection]
l:22 [binder, in Arith.GeneralReflection]
l:278 [binder, in Arith.GeneralReflection]
l:324 [binder, in Arith.GeneralReflection]
l:33 [binder, in Arith.GeneralReflection]
l:36 [binder, in Arith.GeneralReflection]
l:467 [binder, in Arith.GeneralReflection]
l:484 [binder, in Arith.GeneralReflection]
l:517 [binder, in Arith.GeneralReflection]
l:541 [binder, in Arith.GeneralReflection]
M
MainReificationFunctions [section, in Arith.GeneralReflection]mal:73 [binder, in Arith.GeneralReflection]
mAnd [definition, in Arith.GeneralReflection]
map_def_monad [definition, in Arith.GeneralReflection]
map_monad [definition, in Arith.GeneralReflection]
maybeD [definition, in Arith.GeneralReflection]
mA:157 [binder, in Arith.GeneralReflection]
mA:159 [binder, in Arith.GeneralReflection]
mB:158 [binder, in Arith.GeneralReflection]
mB:160 [binder, in Arith.GeneralReflection]
mb:80 [binder, in Arith.GeneralReflection]
mD:453 [binder, in Arith.GeneralReflection]
mergeAnd [definition, in Arith.GeneralReflection]
mergeExists [definition, in Arith.GeneralReflection]
mergeFalse [definition, in Arith.GeneralReflection]
mergeForall [definition, in Arith.GeneralReflection]
mergeForm [definition, in Arith.GeneralReflection]
mergeFormBase [definition, in Arith.GeneralReflection]
mergeFormProto [definition, in Arith.GeneralReflection]
mergeFormProtoType [definition, in Arith.GeneralReflection]
mergeIff [definition, in Arith.GeneralReflection]
mergeImpl [definition, in Arith.GeneralReflection]
mergeOr [definition, in Arith.GeneralReflection]
mergeTerm [definition, in Arith.GeneralReflection]
mergeTermBase [definition, in Arith.GeneralReflection]
mergeTermProto [definition, in Arith.GeneralReflection]
mergeTermProtoType [definition, in Arith.GeneralReflection]
mergeTrue [definition, in Arith.GeneralReflection]
MetaCoqUtils [section, in Arith.GeneralReflection]
mExists [definition, in Arith.GeneralReflection]
me:72 [binder, in Arith.GeneralReflection]
mFalse [definition, in Arith.GeneralReflection]
mForall [definition, in Arith.GeneralReflection]
mIff [definition, in Arith.GeneralReflection]
mImpl [definition, in Arith.GeneralReflection]
minn:42 [binder, in Arith.GeneralReflection]
minn:57 [binder, in Arith.GeneralReflection]
mi:75 [binder, in Arith.GeneralReflection]
mmft:83 [binder, in Arith.GeneralReflection]
mmft:84 [binder, in Arith.GeneralReflection]
mm:577 [binder, in Arith.GeneralReflection]
mm:81 [binder, in Arith.GeneralReflection]
mOr [definition, in Arith.GeneralReflection]
mr:76 [binder, in Arith.GeneralReflection]
mTrue [definition, in Arith.GeneralReflection]
mt2:65 [binder, in Arith.GeneralReflection]
mt:64 [binder, in Arith.GeneralReflection]
mt:66 [binder, in Arith.GeneralReflection]
mt:68 [binder, in Arith.GeneralReflection]
mt:70 [binder, in Arith.GeneralReflection]
mt:82 [binder, in Arith.GeneralReflection]
mv:67 [binder, in Arith.GeneralReflection]
mv:69 [binder, in Arith.GeneralReflection]
mv:71 [binder, in Arith.GeneralReflection]
m:63 [binder, in Arith.GeneralReflection]
N
naryGFunc [definition, in Arith.GeneralReflection]naryProp [definition, in Arith.GeneralReflection]
nary3GFunc [definition, in Arith.GeneralReflection]
noProofDummy [definition, in Arith.GeneralReflection]
num:483 [binder, in Arith.GeneralReflection]
num:497 [binder, in Arith.GeneralReflection]
n:107 [binder, in Arith.GeneralReflection]
n:109 [binder, in Arith.GeneralReflection]
n:112 [binder, in Arith.GeneralReflection]
n:122 [binder, in Arith.GeneralReflection]
n:132 [binder, in Arith.GeneralReflection]
n:137 [binder, in Arith.GeneralReflection]
n:148 [binder, in Arith.GeneralReflection]
n:172 [binder, in Arith.GeneralReflection]
n:181 [binder, in Arith.GeneralReflection]
n:192 [binder, in Arith.GeneralReflection]
n:201 [binder, in Arith.GeneralReflection]
n:34 [binder, in Arith.GeneralReflection]
n:345 [binder, in Arith.GeneralReflection]
n:39 [binder, in Arith.GeneralReflection]
O
orelse [definition, in Arith.GeneralReflection]P
pat:49 [binder, in Arith.GeneralReflection]pat:574 [binder, in Arith.GeneralReflection]
pat:79 [binder, in Arith.GeneralReflection]
phi:113 [binder, in Arith.GeneralReflection]
phi:124 [binder, in Arith.GeneralReflection]
phi:229 [binder, in Arith.GeneralReflection]
point:105 [binder, in Arith.GeneralReflection]
popListStart [definition, in Arith.GeneralReflection]
popNElements [definition, in Arith.GeneralReflection]
pPq:572 [binder, in Arith.GeneralReflection]
propFinderReifier [definition, in Arith.GeneralReflection]
propFinderVars [definition, in Arith.GeneralReflection]
pr:370 [binder, in Arith.GeneralReflection]
pr:377 [binder, in Arith.GeneralReflection]
pr:503 [binder, in Arith.GeneralReflection]
ps [projection, in Arith.GeneralReflection]
ps:102 [binder, in Arith.GeneralReflection]
P:115 [binder, in Arith.GeneralReflection]
P:118 [binder, in Arith.GeneralReflection]
P:119 [binder, in Arith.GeneralReflection]
P:120 [binder, in Arith.GeneralReflection]
P:123 [binder, in Arith.GeneralReflection]
P:188 [binder, in Arith.GeneralReflection]
P:196 [binder, in Arith.GeneralReflection]
P:209 [binder, in Arith.GeneralReflection]
P:214 [binder, in Arith.GeneralReflection]
P:219 [binder, in Arith.GeneralReflection]
P:223 [binder, in Arith.GeneralReflection]
P:232 [binder, in Arith.GeneralReflection]
P:344 [binder, in Arith.GeneralReflection]
Q
qe:571 [binder, in Arith.GeneralReflection]qe:583 [binder, in Arith.GeneralReflection]
Ql:464 [binder, in Arith.GeneralReflection]
Ql:525 [binder, in Arith.GeneralReflection]
Ql:560 [binder, in Arith.GeneralReflection]
quoteNumber [definition, in Arith.GeneralReflection]
Q:210 [binder, in Arith.GeneralReflection]
Q:215 [binder, in Arith.GeneralReflection]
q:221 [binder, in Arith.GeneralReflection]
Q:224 [binder, in Arith.GeneralReflection]
Q:228 [binder, in Arith.GeneralReflection]
Q:233 [binder, in Arith.GeneralReflection]
R
raiseEnvTerm [definition, in Arith.GeneralReflection]recoverVector [definition, in Arith.GeneralReflection]
ReificationHelpers [section, in Arith.GeneralReflection]
reifyAnd [definition, in Arith.GeneralReflection]
reifyAndNP [definition, in Arith.GeneralReflection]
reifyBase [definition, in Arith.GeneralReflection]
reifyBaseNP [definition, in Arith.GeneralReflection]
reifyExist [definition, in Arith.GeneralReflection]
reifyExistNP [definition, in Arith.GeneralReflection]
reifyFalse [definition, in Arith.GeneralReflection]
reifyFalseNP [definition, in Arith.GeneralReflection]
reifyForm [definition, in Arith.GeneralReflection]
reifyFormNP [definition, in Arith.GeneralReflection]
reifyIff [definition, in Arith.GeneralReflection]
reifyIffNP [definition, in Arith.GeneralReflection]
reifyOr [definition, in Arith.GeneralReflection]
reifyOrNP [definition, in Arith.GeneralReflection]
reifyTerm [definition, in Arith.GeneralReflection]
reifyTermNP [definition, in Arith.GeneralReflection]
reifyTrue [definition, in Arith.GeneralReflection]
reifyTrueNP [definition, in Arith.GeneralReflection]
replist:364 [binder, in Arith.GeneralReflection]
replist:416 [binder, in Arith.GeneralReflection]
representableF [definition, in Arith.GeneralReflection]
representableP [definition, in Arith.GeneralReflection]
representsF [definition, in Arith.GeneralReflection]
representsP [definition, in Arith.GeneralReflection]
rep:363 [binder, in Arith.GeneralReflection]
rep:415 [binder, in Arith.GeneralReflection]
ret [constructor, in Arith.GeneralReflection]
rho:114 [binder, in Arith.GeneralReflection]
rho:125 [binder, in Arith.GeneralReflection]
rho:128 [binder, in Arith.GeneralReflection]
rho:131 [binder, in Arith.GeneralReflection]
rho:166 [binder, in Arith.GeneralReflection]
rho:171 [binder, in Arith.GeneralReflection]
rho:180 [binder, in Arith.GeneralReflection]
rho:186 [binder, in Arith.GeneralReflection]
rho:191 [binder, in Arith.GeneralReflection]
rho:200 [binder, in Arith.GeneralReflection]
rho:207 [binder, in Arith.GeneralReflection]
rho:208 [binder, in Arith.GeneralReflection]
rho:213 [binder, in Arith.GeneralReflection]
rho:218 [binder, in Arith.GeneralReflection]
rho:222 [binder, in Arith.GeneralReflection]
rho:227 [binder, in Arith.GeneralReflection]
rho:231 [binder, in Arith.GeneralReflection]
rho:238 [binder, in Arith.GeneralReflection]
rP:463 [binder, in Arith.GeneralReflection]
rP:524 [binder, in Arith.GeneralReflection]
rQ:465 [binder, in Arith.GeneralReflection]
rQ:526 [binder, in Arith.GeneralReflection]
rQ:527 [binder, in Arith.GeneralReflection]
rr:267 [binder, in Arith.GeneralReflection]
rr:343 [binder, in Arith.GeneralReflection]
rr:348 [binder, in Arith.GeneralReflection]
rr:551 [binder, in Arith.GeneralReflection]
rt:314 [binder, in Arith.GeneralReflection]
R:134 [binder, in Arith.GeneralReflection]
R:142 [binder, in Arith.GeneralReflection]
R:143 [binder, in Arith.GeneralReflection]
S
s:284 [binder, in Arith.GeneralReflection]s:330 [binder, in Arith.GeneralReflection]
s:450 [binder, in Arith.GeneralReflection]
T
takeMultiple [definition, in Arith.GeneralReflection]TarskiMerging [section, in Arith.GeneralReflection]
tarski_reflector_extensions [record, in Arith.GeneralReflection]
tarski_reflector [record, in Arith.GeneralReflection]
tct':498 [binder, in Arith.GeneralReflection]
tct:239 [binder, in Arith.GeneralReflection]
tct:245 [binder, in Arith.GeneralReflection]
tct:253 [binder, in Arith.GeneralReflection]
tct:261 [binder, in Arith.GeneralReflection]
tct:269 [binder, in Arith.GeneralReflection]
tct:277 [binder, in Arith.GeneralReflection]
tct:286 [binder, in Arith.GeneralReflection]
tct:292 [binder, in Arith.GeneralReflection]
tct:300 [binder, in Arith.GeneralReflection]
tct:308 [binder, in Arith.GeneralReflection]
tct:315 [binder, in Arith.GeneralReflection]
tct:323 [binder, in Arith.GeneralReflection]
tct:332 [binder, in Arith.GeneralReflection]
tct:339 [binder, in Arith.GeneralReflection]
tct:366 [binder, in Arith.GeneralReflection]
tct:373 [binder, in Arith.GeneralReflection]
tct:380 [binder, in Arith.GeneralReflection]
tct:386 [binder, in Arith.GeneralReflection]
tct:405 [binder, in Arith.GeneralReflection]
tct:443 [binder, in Arith.GeneralReflection]
tct:452 [binder, in Arith.GeneralReflection]
tct:454 [binder, in Arith.GeneralReflection]
tct:466 [binder, in Arith.GeneralReflection]
tct:475 [binder, in Arith.GeneralReflection]
tct:489 [binder, in Arith.GeneralReflection]
tct:509 [binder, in Arith.GeneralReflection]
tct:519 [binder, in Arith.GeneralReflection]
tct:520 [binder, in Arith.GeneralReflection]
tct:521 [binder, in Arith.GeneralReflection]
tct:533 [binder, in Arith.GeneralReflection]
tct:554 [binder, in Arith.GeneralReflection]
tct:555 [binder, in Arith.GeneralReflection]
tct:556 [binder, in Arith.GeneralReflection]
tct:566 [binder, in Arith.GeneralReflection]
tct:578 [binder, in Arith.GeneralReflection]
tct:588 [binder, in Arith.GeneralReflection]
termEnv:478 [binder, in Arith.GeneralReflection]
termEnv:492 [binder, in Arith.GeneralReflection]
termFinderReifier [definition, in Arith.GeneralReflection]
termFinderVars [definition, in Arith.GeneralReflection]
termReifier [definition, in Arith.GeneralReflection]
termReifierNP [definition, in Arith.GeneralReflection]
termReifierReifyHelper [projection, in Arith.GeneralReflection]
termReifierVarHelper [projection, in Arith.GeneralReflection]
te':500 [binder, in Arith.GeneralReflection]
te:206 [binder, in Arith.GeneralReflection]
te:410 [binder, in Arith.GeneralReflection]
te:474 [binder, in Arith.GeneralReflection]
tk:565 [binder, in Arith.GeneralReflection]
tPq:573 [binder, in Arith.GeneralReflection]
tPq:584 [binder, in Arith.GeneralReflection]
tP:559 [binder, in Arith.GeneralReflection]
tP:575 [binder, in Arith.GeneralReflection]
tP:585 [binder, in Arith.GeneralReflection]
tQ:561 [binder, in Arith.GeneralReflection]
tQ:562 [binder, in Arith.GeneralReflection]
tQ:576 [binder, in Arith.GeneralReflection]
treO:568 [binder, in Arith.GeneralReflection]
treO:580 [binder, in Arith.GeneralReflection]
treO:590 [binder, in Arith.GeneralReflection]
tre:570 [binder, in Arith.GeneralReflection]
tre:582 [binder, in Arith.GeneralReflection]
tre:592 [binder, in Arith.GeneralReflection]
trm:127 [binder, in Arith.GeneralReflection]
trm:130 [binder, in Arith.GeneralReflection]
trm:384 [binder, in Arith.GeneralReflection]
trm:390 [binder, in Arith.GeneralReflection]
tr:100 [binder, in Arith.GeneralReflection]
tr:108 [binder, in Arith.GeneralReflection]
tr:205 [binder, in Arith.GeneralReflection]
tr:409 [binder, in Arith.GeneralReflection]
tr:473 [binder, in Arith.GeneralReflection]
tv:58 [binder, in Arith.GeneralReflection]
tyf:52 [binder, in Arith.GeneralReflection]
t':499 [binder, in Arith.GeneralReflection]
T:10 [binder, in Arith.GeneralReflection]
t:167 [binder, in Arith.GeneralReflection]
t:169 [binder, in Arith.GeneralReflection]
t:175 [binder, in Arith.GeneralReflection]
t:177 [binder, in Arith.GeneralReflection]
t:187 [binder, in Arith.GeneralReflection]
t:189 [binder, in Arith.GeneralReflection]
t:195 [binder, in Arith.GeneralReflection]
t:197 [binder, in Arith.GeneralReflection]
t:340 [binder, in Arith.GeneralReflection]
t:393 [binder, in Arith.GeneralReflection]
t:399 [binder, in Arith.GeneralReflection]
t:418 [binder, in Arith.GeneralReflection]
t:44 [binder, in Arith.GeneralReflection]
t:456 [binder, in Arith.GeneralReflection]
t:462 [binder, in Arith.GeneralReflection]
t:477 [binder, in Arith.GeneralReflection]
t:488 [binder, in Arith.GeneralReflection]
t:491 [binder, in Arith.GeneralReflection]
t:508 [binder, in Arith.GeneralReflection]
t:511 [binder, in Arith.GeneralReflection]
t:523 [binder, in Arith.GeneralReflection]
t:535 [binder, in Arith.GeneralReflection]
t:542 [binder, in Arith.GeneralReflection]
t:546 [binder, in Arith.GeneralReflection]
t:558 [binder, in Arith.GeneralReflection]
t:59 [binder, in Arith.GeneralReflection]
t:92 [binder, in Arith.GeneralReflection]
U
unboundEnv [definition, in Arith.GeneralReflection]V
vectorCons [abbreviation, in Arith.GeneralReflection]vectorNil [abbreviation, in Arith.GeneralReflection]
vr:145 [binder, in Arith.GeneralReflection]
vr:424 [binder, in Arith.GeneralReflection]
vr:461 [binder, in Arith.GeneralReflection]
vr:487 [binder, in Arith.GeneralReflection]
vr:507 [binder, in Arith.GeneralReflection]
vr:522 [binder, in Arith.GeneralReflection]
vr:557 [binder, in Arith.GeneralReflection]
v:144 [binder, in Arith.GeneralReflection]
v:163 [binder, in Arith.GeneralReflection]
v:164 [binder, in Arith.GeneralReflection]
v:179 [binder, in Arith.GeneralReflection]
v:199 [binder, in Arith.GeneralReflection]
v:404 [binder, in Arith.GeneralReflection]
v:472 [binder, in Arith.GeneralReflection]
v:502 [binder, in Arith.GeneralReflection]
v:545 [binder, in Arith.GeneralReflection]
v:550 [binder, in Arith.GeneralReflection]
X
xm:17 [binder, in Arith.GeneralReflection]xrl:32 [binder, in Arith.GeneralReflection]
xrm:18 [binder, in Arith.GeneralReflection]
xr:251 [binder, in Arith.GeneralReflection]
xr:259 [binder, in Arith.GeneralReflection]
xr:275 [binder, in Arith.GeneralReflection]
xt:298 [binder, in Arith.GeneralReflection]
xt:306 [binder, in Arith.GeneralReflection]
xt:321 [binder, in Arith.GeneralReflection]
xt:431 [binder, in Arith.GeneralReflection]
xt:436 [binder, in Arith.GeneralReflection]
xt:448 [binder, in Arith.GeneralReflection]
X:138 [binder, in Arith.GeneralReflection]
x:230 [binder, in Arith.GeneralReflection]
x:27 [binder, in Arith.GeneralReflection]
X:586 [binder, in Arith.GeneralReflection]
x:587 [binder, in Arith.GeneralReflection]
x:9 [binder, in Arith.GeneralReflection]
Y
yr:252 [binder, in Arith.GeneralReflection]yr:260 [binder, in Arith.GeneralReflection]
yr:276 [binder, in Arith.GeneralReflection]
yt:299 [binder, in Arith.GeneralReflection]
yt:307 [binder, in Arith.GeneralReflection]
yt:322 [binder, in Arith.GeneralReflection]
yt:432 [binder, in Arith.GeneralReflection]
yt:437 [binder, in Arith.GeneralReflection]
yt:449 [binder, in Arith.GeneralReflection]
Y:139 [binder, in Arith.GeneralReflection]
Z
zv:392 [binder, in Arith.GeneralReflection]zv:398 [binder, in Arith.GeneralReflection]
other
_ <- _ ;; _ [notation, in Arith.GeneralReflection]Notation Index
F
_ <- _ ;; _ [in Arith.GeneralReflection]other
_ <- _ ;; _ [in Arith.GeneralReflection]Binder Index
A
amnt:43 [in Arith.GeneralReflection]atrIH:356 [in Arith.GeneralReflection]
av:367 [in Arith.GeneralReflection]
av:374 [in Arith.GeneralReflection]
av:381 [in Arith.GeneralReflection]
av:387 [in Arith.GeneralReflection]
A':151 [in Arith.GeneralReflection]
A:1 [in Arith.GeneralReflection]
a:11 [in Arith.GeneralReflection]
A:13 [in Arith.GeneralReflection]
A:133 [in Arith.GeneralReflection]
A:149 [in Arith.GeneralReflection]
a:161 [in Arith.GeneralReflection]
A:19 [in Arith.GeneralReflection]
A:23 [in Arith.GeneralReflection]
A:4 [in Arith.GeneralReflection]
a:408 [in Arith.GeneralReflection]
a:471 [in Arith.GeneralReflection]
a:48 [in Arith.GeneralReflection]
A:50 [in Arith.GeneralReflection]
a:78 [in Arith.GeneralReflection]
B
baseEnv:593 [in Arith.GeneralReflection]base:468 [in Arith.GeneralReflection]
bodyf:53 [in Arith.GeneralReflection]
both:349 [in Arith.GeneralReflection]
B':152 [in Arith.GeneralReflection]
B:150 [in Arith.GeneralReflection]
b:162 [in Arith.GeneralReflection]
B:20 [in Arith.GeneralReflection]
b:47 [in Arith.GeneralReflection]
B:5 [in Arith.GeneralReflection]
B:51 [in Arith.GeneralReflection]
b:77 [in Arith.GeneralReflection]
C
C':154 [in Arith.GeneralReflection]C:153 [in Arith.GeneralReflection]
c:165 [in Arith.GeneralReflection]
c:184 [in Arith.GeneralReflection]
c:185 [in Arith.GeneralReflection]
c:204 [in Arith.GeneralReflection]
c:365 [in Arith.GeneralReflection]
c:372 [in Arith.GeneralReflection]
c:379 [in Arith.GeneralReflection]
c:385 [in Arith.GeneralReflection]
D
dbr:56 [in Arith.GeneralReflection]dtr:55 [in Arith.GeneralReflection]
D:103 [in Arith.GeneralReflection]
d:121 [in Arith.GeneralReflection]
d:126 [in Arith.GeneralReflection]
d:129 [in Arith.GeneralReflection]
d:168 [in Arith.GeneralReflection]
d:170 [in Arith.GeneralReflection]
d:176 [in Arith.GeneralReflection]
d:178 [in Arith.GeneralReflection]
d:190 [in Arith.GeneralReflection]
d:198 [in Arith.GeneralReflection]
d:406 [in Arith.GeneralReflection]
d:54 [in Arith.GeneralReflection]
E
envSub:530 [in Arith.GeneralReflection]envSub:564 [in Arith.GeneralReflection]
envTermSub:529 [in Arith.GeneralReflection]
envTermSub:563 [in Arith.GeneralReflection]
envTerm:241 [in Arith.GeneralReflection]
envTerm:247 [in Arith.GeneralReflection]
envTerm:255 [in Arith.GeneralReflection]
envTerm:263 [in Arith.GeneralReflection]
envTerm:271 [in Arith.GeneralReflection]
envTerm:280 [in Arith.GeneralReflection]
envTerm:288 [in Arith.GeneralReflection]
envTerm:294 [in Arith.GeneralReflection]
envTerm:302 [in Arith.GeneralReflection]
envTerm:310 [in Arith.GeneralReflection]
envTerm:317 [in Arith.GeneralReflection]
envTerm:326 [in Arith.GeneralReflection]
envTerm:335 [in Arith.GeneralReflection]
envTerm:513 [in Arith.GeneralReflection]
envTerm:537 [in Arith.GeneralReflection]
envToD:595 [in Arith.GeneralReflection]
envv:482 [in Arith.GeneralReflection]
envv:496 [in Arith.GeneralReflection]
env:242 [in Arith.GeneralReflection]
env:248 [in Arith.GeneralReflection]
env:256 [in Arith.GeneralReflection]
env:264 [in Arith.GeneralReflection]
env:272 [in Arith.GeneralReflection]
env:281 [in Arith.GeneralReflection]
env:289 [in Arith.GeneralReflection]
env:295 [in Arith.GeneralReflection]
env:303 [in Arith.GeneralReflection]
env:311 [in Arith.GeneralReflection]
env:318 [in Arith.GeneralReflection]
env:327 [in Arith.GeneralReflection]
env:336 [in Arith.GeneralReflection]
env:342 [in Arith.GeneralReflection]
env:368 [in Arith.GeneralReflection]
env:375 [in Arith.GeneralReflection]
env:382 [in Arith.GeneralReflection]
env:388 [in Arith.GeneralReflection]
env:391 [in Arith.GeneralReflection]
env:397 [in Arith.GeneralReflection]
env:407 [in Arith.GeneralReflection]
env:479 [in Arith.GeneralReflection]
env:493 [in Arith.GeneralReflection]
env:514 [in Arith.GeneralReflection]
env:538 [in Arith.GeneralReflection]
eT:341 [in Arith.GeneralReflection]
et:346 [in Arith.GeneralReflection]
et:543 [in Arith.GeneralReflection]
et:548 [in Arith.GeneralReflection]
e':501 [in Arith.GeneralReflection]
e:347 [in Arith.GeneralReflection]
e:544 [in Arith.GeneralReflection]
e:549 [in Arith.GeneralReflection]
F
fallback:485 [in Arith.GeneralReflection]fallback:505 [in Arith.GeneralReflection]
ffail:30 [in Arith.GeneralReflection]
ffail:422 [in Arith.GeneralReflection]
ffail:459 [in Arith.GeneralReflection]
ffail:518 [in Arith.GeneralReflection]
ffail:553 [in Arith.GeneralReflection]
ff:74 [in Arith.GeneralReflection]
fPR:243 [in Arith.GeneralReflection]
fPR:249 [in Arith.GeneralReflection]
fPR:257 [in Arith.GeneralReflection]
fPR:265 [in Arith.GeneralReflection]
fPR:273 [in Arith.GeneralReflection]
fPR:282 [in Arith.GeneralReflection]
fPR:290 [in Arith.GeneralReflection]
fPR:296 [in Arith.GeneralReflection]
fPR:304 [in Arith.GeneralReflection]
fPR:312 [in Arith.GeneralReflection]
fPR:319 [in Arith.GeneralReflection]
fPR:328 [in Arith.GeneralReflection]
fPR:337 [in Arith.GeneralReflection]
fPR:426 [in Arith.GeneralReflection]
fPR:429 [in Arith.GeneralReflection]
fPR:434 [in Arith.GeneralReflection]
fPR:439 [in Arith.GeneralReflection]
fPR:446 [in Arith.GeneralReflection]
fP:211 [in Arith.GeneralReflection]
fP:216 [in Arith.GeneralReflection]
fP:220 [in Arith.GeneralReflection]
fP:225 [in Arith.GeneralReflection]
fP:234 [in Arith.GeneralReflection]
fP:236 [in Arith.GeneralReflection]
fQ:212 [in Arith.GeneralReflection]
fQ:217 [in Arith.GeneralReflection]
fQ:226 [in Arith.GeneralReflection]
fQ:235 [in Arith.GeneralReflection]
fQ:237 [in Arith.GeneralReflection]
frees:457 [in Arith.GeneralReflection]
frees:512 [in Arith.GeneralReflection]
frees:536 [in Arith.GeneralReflection]
fs:101 [in Arith.GeneralReflection]
fTR:338 [in Arith.GeneralReflection]
fuel:279 [in Arith.GeneralReflection]
fuel:325 [in Arith.GeneralReflection]
fuel:334 [in Arith.GeneralReflection]
fuel:417 [in Arith.GeneralReflection]
fuel:442 [in Arith.GeneralReflection]
fuel:455 [in Arith.GeneralReflection]
fuel:476 [in Arith.GeneralReflection]
fuel:490 [in Arith.GeneralReflection]
fuel:510 [in Arith.GeneralReflection]
fuel:534 [in Arith.GeneralReflection]
fZ:173 [in Arith.GeneralReflection]
fZ:182 [in Arith.GeneralReflection]
fZ:193 [in Arith.GeneralReflection]
fZ:202 [in Arith.GeneralReflection]
F1:24 [in Arith.GeneralReflection]
F2:25 [in Arith.GeneralReflection]
f:21 [in Arith.GeneralReflection]
f:28 [in Arith.GeneralReflection]
f:547 [in Arith.GeneralReflection]
f:7 [in Arith.GeneralReflection]
G
g:567 [in Arith.GeneralReflection]g:579 [in Arith.GeneralReflection]
g:589 [in Arith.GeneralReflection]
I
ifZ:174 [in Arith.GeneralReflection]ifZ:183 [in Arith.GeneralReflection]
ifZ:194 [in Arith.GeneralReflection]
ifZ:203 [in Arith.GeneralReflection]
IHt:355 [in Arith.GeneralReflection]
IH:352 [in Arith.GeneralReflection]
IH:360 [in Arith.GeneralReflection]
IH:369 [in Arith.GeneralReflection]
IH:376 [in Arith.GeneralReflection]
IH:383 [in Arith.GeneralReflection]
IH:389 [in Arith.GeneralReflection]
IH:412 [in Arith.GeneralReflection]
isD:106 [in Arith.GeneralReflection]
I:104 [in Arith.GeneralReflection]
K
k:146 [in Arith.GeneralReflection]k:147 [in Arith.GeneralReflection]
k:396 [in Arith.GeneralReflection]
k:402 [in Arith.GeneralReflection]
k:403 [in Arith.GeneralReflection]
k:531 [in Arith.GeneralReflection]
k:6 [in Arith.GeneralReflection]
L
lst:240 [in Arith.GeneralReflection]lst:246 [in Arith.GeneralReflection]
lst:254 [in Arith.GeneralReflection]
lst:262 [in Arith.GeneralReflection]
lst:270 [in Arith.GeneralReflection]
lst:287 [in Arith.GeneralReflection]
lst:293 [in Arith.GeneralReflection]
lst:301 [in Arith.GeneralReflection]
lst:309 [in Arith.GeneralReflection]
lst:316 [in Arith.GeneralReflection]
lst:333 [in Arith.GeneralReflection]
lst:425 [in Arith.GeneralReflection]
lst:428 [in Arith.GeneralReflection]
lst:433 [in Arith.GeneralReflection]
lst:438 [in Arith.GeneralReflection]
lst:441 [in Arith.GeneralReflection]
lst:445 [in Arith.GeneralReflection]
lst:594 [in Arith.GeneralReflection]
ls:37 [in Arith.GeneralReflection]
lt:351 [in Arith.GeneralReflection]
lt:359 [in Arith.GeneralReflection]
lt:411 [in Arith.GeneralReflection]
l:14 [in Arith.GeneralReflection]
l:22 [in Arith.GeneralReflection]
l:278 [in Arith.GeneralReflection]
l:324 [in Arith.GeneralReflection]
l:33 [in Arith.GeneralReflection]
l:36 [in Arith.GeneralReflection]
l:467 [in Arith.GeneralReflection]
l:484 [in Arith.GeneralReflection]
l:517 [in Arith.GeneralReflection]
l:541 [in Arith.GeneralReflection]
M
mal:73 [in Arith.GeneralReflection]mA:157 [in Arith.GeneralReflection]
mA:159 [in Arith.GeneralReflection]
mB:158 [in Arith.GeneralReflection]
mB:160 [in Arith.GeneralReflection]
mb:80 [in Arith.GeneralReflection]
mD:453 [in Arith.GeneralReflection]
me:72 [in Arith.GeneralReflection]
minn:42 [in Arith.GeneralReflection]
minn:57 [in Arith.GeneralReflection]
mi:75 [in Arith.GeneralReflection]
mmft:83 [in Arith.GeneralReflection]
mmft:84 [in Arith.GeneralReflection]
mm:577 [in Arith.GeneralReflection]
mm:81 [in Arith.GeneralReflection]
mr:76 [in Arith.GeneralReflection]
mt2:65 [in Arith.GeneralReflection]
mt:64 [in Arith.GeneralReflection]
mt:66 [in Arith.GeneralReflection]
mt:68 [in Arith.GeneralReflection]
mt:70 [in Arith.GeneralReflection]
mt:82 [in Arith.GeneralReflection]
mv:67 [in Arith.GeneralReflection]
mv:69 [in Arith.GeneralReflection]
mv:71 [in Arith.GeneralReflection]
m:63 [in Arith.GeneralReflection]
N
num:483 [in Arith.GeneralReflection]num:497 [in Arith.GeneralReflection]
n:107 [in Arith.GeneralReflection]
n:109 [in Arith.GeneralReflection]
n:112 [in Arith.GeneralReflection]
n:122 [in Arith.GeneralReflection]
n:132 [in Arith.GeneralReflection]
n:137 [in Arith.GeneralReflection]
n:148 [in Arith.GeneralReflection]
n:172 [in Arith.GeneralReflection]
n:181 [in Arith.GeneralReflection]
n:192 [in Arith.GeneralReflection]
n:201 [in Arith.GeneralReflection]
n:34 [in Arith.GeneralReflection]
n:345 [in Arith.GeneralReflection]
n:39 [in Arith.GeneralReflection]
P
pat:49 [in Arith.GeneralReflection]pat:574 [in Arith.GeneralReflection]
pat:79 [in Arith.GeneralReflection]
phi:113 [in Arith.GeneralReflection]
phi:124 [in Arith.GeneralReflection]
phi:229 [in Arith.GeneralReflection]
point:105 [in Arith.GeneralReflection]
pPq:572 [in Arith.GeneralReflection]
pr:370 [in Arith.GeneralReflection]
pr:377 [in Arith.GeneralReflection]
pr:503 [in Arith.GeneralReflection]
ps:102 [in Arith.GeneralReflection]
P:115 [in Arith.GeneralReflection]
P:118 [in Arith.GeneralReflection]
P:119 [in Arith.GeneralReflection]
P:120 [in Arith.GeneralReflection]
P:123 [in Arith.GeneralReflection]
P:188 [in Arith.GeneralReflection]
P:196 [in Arith.GeneralReflection]
P:209 [in Arith.GeneralReflection]
P:214 [in Arith.GeneralReflection]
P:219 [in Arith.GeneralReflection]
P:223 [in Arith.GeneralReflection]
P:232 [in Arith.GeneralReflection]
P:344 [in Arith.GeneralReflection]
Q
qe:571 [in Arith.GeneralReflection]qe:583 [in Arith.GeneralReflection]
Ql:464 [in Arith.GeneralReflection]
Ql:525 [in Arith.GeneralReflection]
Ql:560 [in Arith.GeneralReflection]
Q:210 [in Arith.GeneralReflection]
Q:215 [in Arith.GeneralReflection]
q:221 [in Arith.GeneralReflection]
Q:224 [in Arith.GeneralReflection]
Q:228 [in Arith.GeneralReflection]
Q:233 [in Arith.GeneralReflection]
R
replist:364 [in Arith.GeneralReflection]replist:416 [in Arith.GeneralReflection]
rep:363 [in Arith.GeneralReflection]
rep:415 [in Arith.GeneralReflection]
rho:114 [in Arith.GeneralReflection]
rho:125 [in Arith.GeneralReflection]
rho:128 [in Arith.GeneralReflection]
rho:131 [in Arith.GeneralReflection]
rho:166 [in Arith.GeneralReflection]
rho:171 [in Arith.GeneralReflection]
rho:180 [in Arith.GeneralReflection]
rho:186 [in Arith.GeneralReflection]
rho:191 [in Arith.GeneralReflection]
rho:200 [in Arith.GeneralReflection]
rho:207 [in Arith.GeneralReflection]
rho:208 [in Arith.GeneralReflection]
rho:213 [in Arith.GeneralReflection]
rho:218 [in Arith.GeneralReflection]
rho:222 [in Arith.GeneralReflection]
rho:227 [in Arith.GeneralReflection]
rho:231 [in Arith.GeneralReflection]
rho:238 [in Arith.GeneralReflection]
rP:463 [in Arith.GeneralReflection]
rP:524 [in Arith.GeneralReflection]
rQ:465 [in Arith.GeneralReflection]
rQ:526 [in Arith.GeneralReflection]
rQ:527 [in Arith.GeneralReflection]
rr:267 [in Arith.GeneralReflection]
rr:343 [in Arith.GeneralReflection]
rr:348 [in Arith.GeneralReflection]
rr:551 [in Arith.GeneralReflection]
rt:314 [in Arith.GeneralReflection]
R:134 [in Arith.GeneralReflection]
R:142 [in Arith.GeneralReflection]
R:143 [in Arith.GeneralReflection]
S
s:284 [in Arith.GeneralReflection]s:330 [in Arith.GeneralReflection]
s:450 [in Arith.GeneralReflection]
T
tct':498 [in Arith.GeneralReflection]tct:239 [in Arith.GeneralReflection]
tct:245 [in Arith.GeneralReflection]
tct:253 [in Arith.GeneralReflection]
tct:261 [in Arith.GeneralReflection]
tct:269 [in Arith.GeneralReflection]
tct:277 [in Arith.GeneralReflection]
tct:286 [in Arith.GeneralReflection]
tct:292 [in Arith.GeneralReflection]
tct:300 [in Arith.GeneralReflection]
tct:308 [in Arith.GeneralReflection]
tct:315 [in Arith.GeneralReflection]
tct:323 [in Arith.GeneralReflection]
tct:332 [in Arith.GeneralReflection]
tct:339 [in Arith.GeneralReflection]
tct:366 [in Arith.GeneralReflection]
tct:373 [in Arith.GeneralReflection]
tct:380 [in Arith.GeneralReflection]
tct:386 [in Arith.GeneralReflection]
tct:405 [in Arith.GeneralReflection]
tct:443 [in Arith.GeneralReflection]
tct:452 [in Arith.GeneralReflection]
tct:454 [in Arith.GeneralReflection]
tct:466 [in Arith.GeneralReflection]
tct:475 [in Arith.GeneralReflection]
tct:489 [in Arith.GeneralReflection]
tct:509 [in Arith.GeneralReflection]
tct:519 [in Arith.GeneralReflection]
tct:520 [in Arith.GeneralReflection]
tct:521 [in Arith.GeneralReflection]
tct:533 [in Arith.GeneralReflection]
tct:554 [in Arith.GeneralReflection]
tct:555 [in Arith.GeneralReflection]
tct:556 [in Arith.GeneralReflection]
tct:566 [in Arith.GeneralReflection]
tct:578 [in Arith.GeneralReflection]
tct:588 [in Arith.GeneralReflection]
termEnv:478 [in Arith.GeneralReflection]
termEnv:492 [in Arith.GeneralReflection]
te':500 [in Arith.GeneralReflection]
te:206 [in Arith.GeneralReflection]
te:410 [in Arith.GeneralReflection]
te:474 [in Arith.GeneralReflection]
tk:565 [in Arith.GeneralReflection]
tPq:573 [in Arith.GeneralReflection]
tPq:584 [in Arith.GeneralReflection]
tP:559 [in Arith.GeneralReflection]
tP:575 [in Arith.GeneralReflection]
tP:585 [in Arith.GeneralReflection]
tQ:561 [in Arith.GeneralReflection]
tQ:562 [in Arith.GeneralReflection]
tQ:576 [in Arith.GeneralReflection]
treO:568 [in Arith.GeneralReflection]
treO:580 [in Arith.GeneralReflection]
treO:590 [in Arith.GeneralReflection]
tre:570 [in Arith.GeneralReflection]
tre:582 [in Arith.GeneralReflection]
tre:592 [in Arith.GeneralReflection]
trm:127 [in Arith.GeneralReflection]
trm:130 [in Arith.GeneralReflection]
trm:384 [in Arith.GeneralReflection]
trm:390 [in Arith.GeneralReflection]
tr:100 [in Arith.GeneralReflection]
tr:108 [in Arith.GeneralReflection]
tr:205 [in Arith.GeneralReflection]
tr:409 [in Arith.GeneralReflection]
tr:473 [in Arith.GeneralReflection]
tv:58 [in Arith.GeneralReflection]
tyf:52 [in Arith.GeneralReflection]
t':499 [in Arith.GeneralReflection]
T:10 [in Arith.GeneralReflection]
t:167 [in Arith.GeneralReflection]
t:169 [in Arith.GeneralReflection]
t:175 [in Arith.GeneralReflection]
t:177 [in Arith.GeneralReflection]
t:187 [in Arith.GeneralReflection]
t:189 [in Arith.GeneralReflection]
t:195 [in Arith.GeneralReflection]
t:197 [in Arith.GeneralReflection]
t:340 [in Arith.GeneralReflection]
t:393 [in Arith.GeneralReflection]
t:399 [in Arith.GeneralReflection]
t:418 [in Arith.GeneralReflection]
t:44 [in Arith.GeneralReflection]
t:456 [in Arith.GeneralReflection]
t:462 [in Arith.GeneralReflection]
t:477 [in Arith.GeneralReflection]
t:488 [in Arith.GeneralReflection]
t:491 [in Arith.GeneralReflection]
t:508 [in Arith.GeneralReflection]
t:511 [in Arith.GeneralReflection]
t:523 [in Arith.GeneralReflection]
t:535 [in Arith.GeneralReflection]
t:542 [in Arith.GeneralReflection]
t:546 [in Arith.GeneralReflection]
t:558 [in Arith.GeneralReflection]
t:59 [in Arith.GeneralReflection]
t:92 [in Arith.GeneralReflection]
V
vr:145 [in Arith.GeneralReflection]vr:424 [in Arith.GeneralReflection]
vr:461 [in Arith.GeneralReflection]
vr:487 [in Arith.GeneralReflection]
vr:507 [in Arith.GeneralReflection]
vr:522 [in Arith.GeneralReflection]
vr:557 [in Arith.GeneralReflection]
v:144 [in Arith.GeneralReflection]
v:163 [in Arith.GeneralReflection]
v:164 [in Arith.GeneralReflection]
v:179 [in Arith.GeneralReflection]
v:199 [in Arith.GeneralReflection]
v:404 [in Arith.GeneralReflection]
v:472 [in Arith.GeneralReflection]
v:502 [in Arith.GeneralReflection]
v:545 [in Arith.GeneralReflection]
v:550 [in Arith.GeneralReflection]
X
xm:17 [in Arith.GeneralReflection]xrl:32 [in Arith.GeneralReflection]
xrm:18 [in Arith.GeneralReflection]
xr:251 [in Arith.GeneralReflection]
xr:259 [in Arith.GeneralReflection]
xr:275 [in Arith.GeneralReflection]
xt:298 [in Arith.GeneralReflection]
xt:306 [in Arith.GeneralReflection]
xt:321 [in Arith.GeneralReflection]
xt:431 [in Arith.GeneralReflection]
xt:436 [in Arith.GeneralReflection]
xt:448 [in Arith.GeneralReflection]
X:138 [in Arith.GeneralReflection]
x:230 [in Arith.GeneralReflection]
x:27 [in Arith.GeneralReflection]
X:586 [in Arith.GeneralReflection]
x:587 [in Arith.GeneralReflection]
x:9 [in Arith.GeneralReflection]
Y
yr:252 [in Arith.GeneralReflection]yr:260 [in Arith.GeneralReflection]
yr:276 [in Arith.GeneralReflection]
yt:299 [in Arith.GeneralReflection]
yt:307 [in Arith.GeneralReflection]
yt:322 [in Arith.GeneralReflection]
yt:432 [in Arith.GeneralReflection]
yt:437 [in Arith.GeneralReflection]
yt:449 [in Arith.GeneralReflection]
Y:139 [in Arith.GeneralReflection]
Z
zv:392 [in Arith.GeneralReflection]zv:398 [in Arith.GeneralReflection]
Library Index
G
GeneralReflectionConstructor Index
F
fail [in Arith.GeneralReflection]R
ret [in Arith.GeneralReflection]Projection Index
B
baseLogicConnHelper [in Arith.GeneralReflection]baseLogicVarHelper [in Arith.GeneralReflection]
D
D [in Arith.GeneralReflection]E
emptyEnv [in Arith.GeneralReflection]F
formReifierReifyHelper [in Arith.GeneralReflection]formReifierVarHelper [in Arith.GeneralReflection]
fs [in Arith.GeneralReflection]
I
I [in Arith.GeneralReflection]isD [in Arith.GeneralReflection]
P
ps [in Arith.GeneralReflection]T
termReifierReifyHelper [in Arith.GeneralReflection]termReifierVarHelper [in Arith.GeneralReflection]
Inductive Index
F
FailureMonad [in Arith.GeneralReflection]Section Index
A
AbstractReflectionDefinitions [in Arith.GeneralReflection]E
EnvConstructor [in Arith.GeneralReflection]EnvHelpers [in Arith.GeneralReflection]
F
FailureMonad [in Arith.GeneralReflection]M
MainReificationFunctions [in Arith.GeneralReflection]MetaCoqUtils [in Arith.GeneralReflection]
R
ReificationHelpers [in Arith.GeneralReflection]T
TarskiMerging [in Arith.GeneralReflection]Abbreviation Index
B
baseLogicConn [in Arith.GeneralReflection]baseLogicConn [in Arith.GeneralReflection]
baseLogicConn [in Arith.GeneralReflection]
V
vectorCons [in Arith.GeneralReflection]vectorNil [in Arith.GeneralReflection]
Definition Index
A
addRelIndex [in Arith.GeneralReflection]appendAndLift [in Arith.GeneralReflection]
appendZero [in Arith.GeneralReflection]
applyRecursively [in Arith.GeneralReflection]
applyRecursivelyNP [in Arith.GeneralReflection]
B
baseConnectiveReifier [in Arith.GeneralReflection]baseConnectiveReifierNP [in Arith.GeneralReflection]
baseConnectiveVars [in Arith.GeneralReflection]
bind [in Arith.GeneralReflection]
buildDefaultTarski [in Arith.GeneralReflection]
C
constructForm [in Arith.GeneralReflection]constructTerm [in Arith.GeneralReflection]
createEnvTerms [in Arith.GeneralReflection]
D
defaultExtensions [in Arith.GeneralReflection]F
findPropRepresentation [in Arith.GeneralReflection]findPropRepresentationNP [in Arith.GeneralReflection]
findTermRepresentation [in Arith.GeneralReflection]
findTermRepresentationNP [in Arith.GeneralReflection]
findUBAnd [in Arith.GeneralReflection]
findUBBase [in Arith.GeneralReflection]
findUBExists [in Arith.GeneralReflection]
findUBFalse [in Arith.GeneralReflection]
findUBIff [in Arith.GeneralReflection]
findUBOr [in Arith.GeneralReflection]
findUBRecursively [in Arith.GeneralReflection]
findUBTrue [in Arith.GeneralReflection]
findUnboundVariablesForm [in Arith.GeneralReflection]
findUnboundVariablesTerm [in Arith.GeneralReflection]
flatten_monad [in Arith.GeneralReflection]
FUEL [in Arith.GeneralReflection]
f2t [in Arith.GeneralReflection]
H
helperFormReifierType [in Arith.GeneralReflection]helperFormVarsType [in Arith.GeneralReflection]
helperTermReifierType [in Arith.GeneralReflection]
helperTermVarsType [in Arith.GeneralReflection]
HiddenTerm [in Arith.GeneralReflection]
L
lowerRelIndex [in Arith.GeneralReflection]M
mAnd [in Arith.GeneralReflection]map_def_monad [in Arith.GeneralReflection]
map_monad [in Arith.GeneralReflection]
maybeD [in Arith.GeneralReflection]
mergeAnd [in Arith.GeneralReflection]
mergeExists [in Arith.GeneralReflection]
mergeFalse [in Arith.GeneralReflection]
mergeForall [in Arith.GeneralReflection]
mergeForm [in Arith.GeneralReflection]
mergeFormBase [in Arith.GeneralReflection]
mergeFormProto [in Arith.GeneralReflection]
mergeFormProtoType [in Arith.GeneralReflection]
mergeIff [in Arith.GeneralReflection]
mergeImpl [in Arith.GeneralReflection]
mergeOr [in Arith.GeneralReflection]
mergeTerm [in Arith.GeneralReflection]
mergeTermBase [in Arith.GeneralReflection]
mergeTermProto [in Arith.GeneralReflection]
mergeTermProtoType [in Arith.GeneralReflection]
mergeTrue [in Arith.GeneralReflection]
mExists [in Arith.GeneralReflection]
mFalse [in Arith.GeneralReflection]
mForall [in Arith.GeneralReflection]
mIff [in Arith.GeneralReflection]
mImpl [in Arith.GeneralReflection]
mOr [in Arith.GeneralReflection]
mTrue [in Arith.GeneralReflection]
N
naryGFunc [in Arith.GeneralReflection]naryProp [in Arith.GeneralReflection]
nary3GFunc [in Arith.GeneralReflection]
noProofDummy [in Arith.GeneralReflection]
O
orelse [in Arith.GeneralReflection]P
popListStart [in Arith.GeneralReflection]popNElements [in Arith.GeneralReflection]
propFinderReifier [in Arith.GeneralReflection]
propFinderVars [in Arith.GeneralReflection]
Q
quoteNumber [in Arith.GeneralReflection]R
raiseEnvTerm [in Arith.GeneralReflection]recoverVector [in Arith.GeneralReflection]
reifyAnd [in Arith.GeneralReflection]
reifyAndNP [in Arith.GeneralReflection]
reifyBase [in Arith.GeneralReflection]
reifyBaseNP [in Arith.GeneralReflection]
reifyExist [in Arith.GeneralReflection]
reifyExistNP [in Arith.GeneralReflection]
reifyFalse [in Arith.GeneralReflection]
reifyFalseNP [in Arith.GeneralReflection]
reifyForm [in Arith.GeneralReflection]
reifyFormNP [in Arith.GeneralReflection]
reifyIff [in Arith.GeneralReflection]
reifyIffNP [in Arith.GeneralReflection]
reifyOr [in Arith.GeneralReflection]
reifyOrNP [in Arith.GeneralReflection]
reifyTerm [in Arith.GeneralReflection]
reifyTermNP [in Arith.GeneralReflection]
reifyTrue [in Arith.GeneralReflection]
reifyTrueNP [in Arith.GeneralReflection]
representableF [in Arith.GeneralReflection]
representableP [in Arith.GeneralReflection]
representsF [in Arith.GeneralReflection]
representsP [in Arith.GeneralReflection]
T
takeMultiple [in Arith.GeneralReflection]termFinderReifier [in Arith.GeneralReflection]
termFinderVars [in Arith.GeneralReflection]
termReifier [in Arith.GeneralReflection]
termReifierNP [in Arith.GeneralReflection]
U
unboundEnv [in Arith.GeneralReflection]Record Index
T
tarski_reflector_extensions [in Arith.GeneralReflection]tarski_reflector [in Arith.GeneralReflection]
| 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 | (628 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 | (2 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 | (491 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 | (1 entry) |
| 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 | (2 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 | (12 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 | (1 entry) |
| 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 | (8 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 | (5 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 | (104 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 | (2 entries) |
This page has been generated by coqdoc