Lectures onType Theory
Inference rules
Scholarly index

Inference rules

  1. Nat-Z, Nat-Schapter-001
  2. Nat-Schapter-001
  3. 1 inference ruleschapter-001
  4. Tree-Emp, Tree-Nodechapter-001
  5. Is-Z, Is-Schapter-001
  6. Nat-Schapter-001
  7. List-Nil, List-Conschapter-001
  8. List-Conschapter-001
  9. Ev-Z, Ev-S, Od-Schapter-001
  10. Sum-Z, Sum-Schapter-001
  11. 1 inference ruleschapter-001
  12. Nat-SSchapter-001
  13. Nat-Schapter-001
  14. Ev-Invchapter-001
  15. Num-Z, Num-Schapter-001
  16. A-Suc, A-Add-L, A-Add-R, A-Add-Z, A-Add-Schapter-001
  17. A-Add-Lchapter-001
  18. M-Refl, M-Stepchapter-001
  19. AB-Z, AB-S, AB-Addchapter-001
  20. AB-Addchapter-001
  21. V-Lam, V-True, V-False, V-Num, Num-Z, Num-Schapter-001
  22. E-App-L, E-App-R, E-Beta, E-If, E-If-T, E-If-F, E-Suc, E-Add-L, E-Add-R, E-Add-Z, E-Add-Schapter-001
  23. CBV-Reflchapter-001
  24. CBV-Stepchapter-001
  25. E-Betachapter-001
  26. B-Val, B-App, B-If-T, B-If-F, B-Suc, B-Addchapter-001
  27. Ty-Bool, Ty-Atom, Ty-Arrchapter-002
  28. Ty-Arrchapter-002
  29. Cx-Emp, Cx-Extchapter-002
  30. Cx-Extchapter-002
  31. Var, True, False, If, Lam, Appchapter-002
  32. Lamchapter-002
  33. Lamchapter-002
  34. Appchapter-002
  35. E-AppL, E-AppR, E-Beta, E-If, E-True, E-Falsechapter-002
  36. M-Refl, M-Stepchapter-002
  37. Ty-Prod, Pair, Fst, Sndchapter-002
  38. E-PairL, E-PairR, E-Fst, E-Fst-Pair, E-Snd, E-Snd-Pairchapter-002
  39. Pairchapter-002
  40. Ty-Sum, Inl, Inr, Casechapter-002
  41. E-Inl, E-Inr, E-Case, E-Case-L, E-Case-Rchapter-002
  42. Casechapter-002
  43. Ty-Unit, Unit-Ichapter-002
  44. Ty-Empty, Empty-E, E-Abortchapter-002
  45. Empty-Echapter-002
  46. Hyp, →p I, E, I, E_1, E_2chapter-002
  47. I, E, I_1, I_2, Echapter-002
  48. Hyp, E, I, E_ichapter-003
  49. I_1, I_2, E, → I, → Echapter-003
  50. I, E, I, Echapter-003
  51. Ax, Cut, W_L, C_L, Lchapter-003
  52. R, L_i, R_1, R_2, Lchapter-003
  53. → R, → L, R, L, R, Lchapter-003
  54. split → E, split Echapter-003
  55. split E, split Echapter-003
  56. I, E, Ichapter-003
  57. E, Echapter-003
  58. S-Ax, S-Bot-L, S-And-R, S-Or-R_ichapter-003
  59. S-Imp-R, S-All-R, S-Some-Rchapter-003
  60. S-And-L_i, S-Or-L, S-Imp-Lchapter-003
  61. S-All-L, S-Some-Lchapter-003
  62. Var, Inst, Gen, Lam, App, Letchapter-004
  63. Genchapter-004
  64. Inst, Instchapter-004
  65. Letchapter-004
  66. C-Var, C-Lam, C-Appchapter-004
  67. S-Var, S-Lam, S-App, S-Letchapter-004
  68. Ev-Var, Ev-Lam, Ev-App, Ev-Letchapter-004
  69. ListNil, ListCons, S-ListNil, S-ListConschapter-004
  70. ListCasechapter-004
  71. S-ListCasechapter-004
  72. ListConschapter-004
  73. ListCasechapter-004
  74. Unit, Ref, Deref, Assignchapter-004
  75. Let-Gen, Let-Monochapter-004
  76. S-Let-Gen, S-Let-Monochapter-004
  77. S-Unit, S-Ref, S-Deref, S-Assignchapter-004
  78. GenΣ, Let-GenΣchapter-004
  79. S-Loc, S-Let-GenΣchapter-004
  80. FO-Var, FO-Abs, FO-App, FO-Let, FO-Fixchapter-005
  81. SD-Var, SD-Abs, SD-App, SD-Let, SD-Fixchapter-005
  82. F-TVar, F-Num, F-Arrowchapter-006
  83. D-Lit, D-Add, D-Mulchapter-006
  84. D-Div, D-Powchapter-006
  85. C-Var, C-Lam, C-App, C-Letchapter-006
  86. C-Lit, C-Add, C-Mul, C-Div, C-Powchapter-006
  87. E-Var, E-Litchapter-006
  88. E-Lam, E-Appchapter-006
  89. E-Letchapter-006
  90. L-Assume, L-Empty, L-Extendchapter-007
  91. Row-Var, Row-Empty, Row-Extchapter-007
  92. Q-Var, Q-Const, Q-Lam, Q-App, Q-Let, Q-Convchapter-007
  93. Q-Empty, Q-Select, Q-Restrictchapter-007
  94. Q-Extendchapter-007
  95. Q-Inject, Q-Embedchapter-007
  96. Q-Casechapter-007
  97. Ev-Assume, Ev-Empty, Ev-Before, Ev-Afterchapter-007
  98. T-Convchapter-007
  99. T-Var, T-Const, T-Inst, T-Ev-Abs, T-Letchapter-007
  100. T-Empty, T-Lookupchapter-007
  101. Ty-Base, Ty-Var, Ty-Arr, Ty-Recchapter-008
  102. K-Type, K-VarRec, K-Recchapter-008
  103. R-Var, R-Const, R-Lam, R-Appchapter-008
  104. R-Record, R-Dotchapter-008
  105. R-TAbs, R-TAppchapter-008
  106. VK-U, VK-Recchapter-008
  107. VT-Mono, VT-All, VT-IArrowchapter-008
  108. IR-Var, IR-Poschapter-008
  109. IV-Var, IV-Poschapter-008
  110. V-Var, V-Const, V-Lam, V-Appchapter-008
  111. V-TAbs, V-TAppchapter-008
  112. V-Vec, V-Nth, V-IAbs, V-IAppchapter-008
  113. C-Var, C-Const, C-Lam, C-Appchapter-008
  114. C-Recordchapter-008
  115. C-Dotchapter-008
  116. C-TAbsRec, C-TAppRec, C-TAbsU, C-TAppUchapter-008
  117. F-Δ-Emp, F-Δ-Ext, F-Γ-Emp, F-Γ-Extchapter-009
  118. F-Ty-Var, F-Ty-Arr, F-Ty-Allchapter-009
  119. F-Var, F-Arr-I, F-Arr-E, F-All-I, F-All-Echapter-009
  120. C-Var, C-Arr-I, C-Arr-Echapter-009
  121. C-All-I, C-All-Echapter-009
  122. P-Var, P-Lam, P-App, P-TLam, P-TApp, P-Beta, P-TBetachapter-009
  123. ?chapter-011
  124. KCtx-Empty, KCtx-Extchapter-011
  125. K-Var, K-Nat, K-Arr, K-Prod, K-All, K-Some, K-Abs, K-Appchapter-011
  126. TR-Betachapter-011
  127. TR-App_1, TR-App_2, TR-Arr_1, TR-Arr_2, TR-Prod_1, TR-Prod_2chapter-011
  128. TR-Abs, TR-All, TR-Somechapter-011
  129. Q-Refl, Q-Sym, Q-Trans, Q-Arr, Q-Prod, Q-All, Q-Some, Q-Abs, Q-App, Q-Betachapter-011
  130. Ctx-Empty, Ctx-Extchapter-011
  131. T-Var, T-Lam, T-App, T-TLam, T-TApp, T-Pair, T-Prj, T-Zero, T-Suc, T-Convchapter-011
  132. E-Beta, E-TBeta, E-PrjPairchapter-011
  133. E-App_1, E-App_2, E-TAppchapter-011
  134. E-Pair_1, E-Pair_2, E-Prj, E-Succhapter-011
  135. T-Pack, T-Unpackchapter-012
  136. U-DictLam, U-DictAppchapter-013
  137. C-R-Main, C-R-IAbs, C-R-Simp, C-L-Match, C-L-NoMatch, C-M-Simp, C-M-IApp, C-M-TAppchapter-013
  138. Mix-Imp, Mix-Defchapter-015
  139. Mix-Withchapter-015
  140. Mix-Struct, Mix-Sealchapter-015
  141. Mix-Completechapter-015
  142. Mix-Withchapter-015
  143. Slot-Return, Slot-Get, Slot-Setchapter-015
  144. Slot-Seq, Slot-Newchapter-015
  145. Tr-Empty, Tr-Get, Tr-Setchapter-015
  146. Tr-Seq, Tr-Newchapter-015
  147. R-Base, R-Functorchapter-016
  148. T-EvPath, T-EvFunctorchapter-016
  149. E-Eq, E-Showchapter-016
  150. SI-Var, SI-Query, SI-ArrI, SI-ArrEchapter-016
  151. SI-ImpI, SI-ImpE, SI-AllI, SI-AllEchapter-016
  152. SI-LetEx, SI-LetIm, SI-Stitchchapter-016
  153. E-Suc, E-NatRec, E-NatZero, E-NatSucchapter-018
  154. F-Base, F-Arr, F-Prod, F-Sum, F-Rcdchapter-018
  155. S-Refl, S-Trans, S-Top, S-Bot, S-Arr, S-Prod, S-Sum, S-Rcdchapter-018
  156. T-Sub, T-Rcd, T-Projchapter-018
  157. E-Rcd, E-Proj, E-ProjCongchapter-018
  158. F-Var, F-Allchapter-018
  159. S-Var, S-AllKchapter-018
  160. T-TAbs, T-TAppchapter-018
  161. A-Eq, A-Top, A-Bot, A-Var, A-Arr, A-Prod, A-Sum, A-Rcd, A-AllKchapter-018
  162. S-AllFchapter-018
  163. Var-Let, Var-Lam, Abschapter-019
  164. App, Letchapter-019
  165. Unit, Bool, Ifchapter-019
  166. Subchapter-019
  167. T-Var, T-Abs, T-Interchapter-020
  168. T-App, T-Sub, T-Const, T-Pair, T-Proj, T-Casechapter-020
  169. _1, _2chapter-020
  170. DT-Var, DT-Int, DT-Lamchapter-021
  171. DT-App, DT-Pair, DT-Projchapter-021
  172. S-Int, S-Arrchapter-021
  173. S-Prod, S-&Rchapter-021
  174. S-&L_1, S-&L_2chapter-021
  175. WF-&chapter-021
  176. I-Var, I-Int, I-Pairchapter-021
  177. I-App, I-Projchapter-021
  178. I-Merge, I-Annchapter-021
  179. I-Lam, I-Subchapter-021
  180. E-Shift, E-Len, E-Get, E-Beta, E-Fix, E-IfT, E-IfFchapter-022
  181. WF-Empty, WF-Var, WF-Guard, WF-Base, WF-Arrowchapter-022
  182. S-Base, S-Arrowchapter-022
  183. D-Var, D-Int, D-Array, D-Lam, D-Fixchapter-022
  184. D-Shift, D-Length, D-Get, D-Appchapter-022
  185. D-Sub, D-Let, D-If, D-Errorchapter-022
  186. ST-Var, ST-Int, ST-Array, ST-Lam, ST-Fixchapter-022
  187. ST-Shift, ST-Length, ST-Get, ST-Appchapter-022
  188. ST-Atom, ST-Let, ST-If, ST-Errorchapter-022
  189. C-UnkL, C-UnkR, C-Bool, C-Nat, C-Arrchapter-023
  190. G-Bool, G-Nat, G-Var, G-Lam, G-Appchapter-023
  191. T-Bool, T-Nat, T-Varchapter-023
  192. T-Lam, T-Appchapter-023
  193. T-Cast, T-Blamechapter-023
  194. E-Beta, E-IdBase, E-IdUnk, E-Project, E-Mismatch, E-Ground, E-Expandchapter-023
  195. E-WrapApp, E-Blamechapter-023
  196. I-Bool, I-Nat, I-Var, I-Lam, I-Appchapter-023
  197. P-Bool, P-Nat, P-Unk, P-Arrchapter-023
  198. N-Bool, N-Nat, N-Unk, N-GroundUnk, N-Arrchapter-023
  199. Pr-Unk, Pr-Bool, Pr-Nat, Pr-Arrchapter-023
  200. PrCtx-Empty, PrCtx-Extendchapter-023
  201. PrTm-Bool, PrTm-Nat, PrTm-Varchapter-023
  202. PrTm-Lam, PrTm-Appchapter-023
  203. CPr-Bool, CPr-Nat, CPr-Varchapter-023
  204. CPr-Lam, CPr-Appchapter-023
  205. CPr-Castchapter-023
  206. CPr-CastL, CPr-CastRchapter-023
  207. CPr-Blamechapter-023
  208. FPr-AppL, FPr-AppRchapter-023
  209. FPr-Castchapter-023
  210. FPr-Hole, FPr-Conschapter-023
  211. Mu-Fchapter-024
  212. T-Fold, T-Unfoldchapter-024
  213. E-Beta, E-IfTrue, E-IfFalsechapter-024
  214. E-Fst, E-Sndchapter-024
  215. E-CaseL, E-CaseRchapter-024
  216. E-UnfoldFoldchapter-024
  217. P-Succ, P-Ifz, P-Fixchapter-024
  218. P-Beta, P-SuccN, P-IfZ, P-IfS, P-Unrollchapter-024
  219. Obs-Zero, Obs-Conschapter-024
  220. Pr-Fix, Pr-Unrollchapter-024
  221. T-Object, T-Invoke, T-Overridechapter-025
  222. S-Top, S-Objectchapter-025
  223. T-Subchapter-025
  224. M-Object, M-Overridechapter-025
  225. M-Invokechapter-025
  226. T-Lam, T-Appchapter-025
  227. FT-Arr, FT-Record, FT-Exists, FT-Muchapter-025
  228. S-Refl, S-Trans, S-Bound, S-Topchapter-025
  229. S-Arr, S-Rec, S-Existschapter-025
  230. S-Amberchapter-025
  231. F-Var, F-Subchapter-025
  232. F-Lam, F-App, F-Record, F-Projchapter-025
  233. F-Pack, F-Openchapter-025
  234. F-Fold, F-Unfoldchapter-025
  235. F-Letrecchapter-025
  236. S-Bound, S-Top, S-Arrow, S-Record, S-Selfchapter-027
  237. T-Var, T-Const, T-Bool, T-Unit, T-Succ, T-Abs, T-Appchapter-027
  238. T-If, T-Record, T-Proj, T-Fix, T-Subchapter-027
  239. T-PackSelf, T-UseSelfchapter-027
  240. F-All, F-Intro, F-Elimchapter-027
  241. S-H-Arrow, S-H-Recordchapter-027
  242. T-H-Var, T-H-Abs, T-H-App, T-H-Record, T-H-Proj, T-H-Subchapter-027
  243. K-OpAbs, K-OpApp, K-Mu, S-OpPoint, S-OpBound, S-OpAppchapter-027
  244. K-AllOp, T-AllOp-I, T-AllOp-E, T-Fold, T-Unfoldchapter-027
  245. T-Match-Var, T-Match-Abs, T-Match-Appchapter-027
  246. T-Match-I, T-Match-E, T-Match-Projchapter-027
  247. T-Ref, T-Deref, T-Assign, T-Locchapter-027
  248. V-Var, V-Const, V-Thunkchapter-028
  249. C-Return, C-To, C-Forcechapter-028
  250. C-Lam, C-Appchapter-028
  251. S-Var, S-Const, S-Lam, S-Appchapter-028
  252. V-Val, V-Appchapter-028
  253. N-Val, N-Appchapter-028
  254. V-Thunk^Σ, C-Return^Σ, C-To^Σchapter-028
  255. C-Force^Σ, C-Lam^Σ, C-App^Σchapter-028
  256. C-Op, C-Weakenchapter-028
  257. C-Handlechapter-028
  258. V-Var, V-Constchapter-031
  259. V-Lam, C-Returnchapter-031
  260. C-App, C-To, C-Opchapter-031
  261. C-Letchapter-031
  262. C-RowConvchapter-031
  263. C-Handlechapter-031
  264. X-Var, X-Constchapter-032
  265. X-BVar, X-Blockchapter-032
  266. X-Expr, X-Val, X-Defchapter-032
  267. X-Call, X-Handlechapter-032
  268. X-Cap, X-Delimchapter-032
  269. E-Expr, E-Valchapter-032
  270. E-Defchapter-032
  271. E-Call, E-Effectchapter-032
  272. E-Do, E-Trychapter-032
  273. WF-Emp, WF-EVar, WF-Label, WF-HLabelchapter-032
  274. WF-ESeq, WF-Unit, WF-Int, WF-Funchapter-032
  275. WF-EAll, WF-HAllchapter-032
  276. T-Unit, T-Int, T-Varchapter-032
  277. T-Lam, T-Appchapter-032
  278. T-Let, T-EAbschapter-032
  279. S-Unit, S-Int, S-Fun, S-AllEchapter-032
  280. S-AllH, S-Transchapter-032
  281. T-EApp, T-HAbschapter-032
  282. T-HAppchapter-032
  283. T-HVar, T-Upchapter-032
  284. T-HDef, T-Downchapter-032
  285. T-Letcc, T-Throwchapter-035
  286. K-Empty, K-Pushchapter-035
  287. T-Cont, S-Eval, S-Retchapter-035
  288. I, E, I_1, I_2chapter-035
  289. K-Var, K-Arr, K-Allchapter-035
  290. K-Nil, K-Conschapter-035
  291. P-Var, P-Lam, P-Appchapter-035
  292. Sub-Refl, Sub-Arr, Sub-Allchapter-035
  293. Sub-Nil, Sub-Conschapter-035
  294. P-Gen, P-Inst, P-Subchapter-035
  295. P-Liftchapter-035
  296. K-DH, Free-DHchapter-035
  297. DH-Dochapter-035
  298. DH-Handlechapter-035
  299. K-S0, Free-S0chapter-035
  300. S0-Shiftchapter-035
  301. S0-Resetchapter-035
  302. S0-Resetchapter-035
  303. K-SHchapter-035
  304. SH-Dochapter-035
  305. SH-Handlechapter-035
  306. K-C0chapter-035
  307. C0-Controlchapter-035
  308. C0-Resetchapter-035
  309. C0-Controlchapter-035
  310. Dep-Bot-F, Dep-Eq-F, Dep-Ex-F, Dep-Nat, Dep-Var-N, Dep-Var-Pchapter-035
  311. Dep-Pair, Dep-Wit, Dep-Prfchapter-035
  312. Dep-Refl, Dep-Substchapter-035
  313. Dep-Callcc-P, Dep-Throw-Pchapter-035
  314. Dep-Callcc-N, Dep-Throw-Nchapter-035
  315. ML-Var, ML-Constchapter-035
  316. ML-Abs, ML-Appchapter-035
  317. ML-Letchapter-035
  318. val0, val1chapter-035
  319. fn, argchapter-035
  320. beta, wrongchapter-035
  321. bind, subchapter-035
  322. seize, jumpchapter-035
  323. T-UVar, T-LVar, T-OneI, T-OneEchapter-036
  324. T-LolliI, T-LolliE, T-TensorI, T-TensorEchapter-036
  325. T-PlusI1, T-PlusI2chapter-036
  326. T-Casechapter-036
  327. T-BangI, T-BangEchapter-036
  328. E-LinBeta, E-Tensor, E-One, E-InL, E-InR, E-Bangchapter-036
  329. T-Open, T-Read, T-Close, T-Byteschapter-036
  330. E-Open, E-Read, E-Closechapter-036
  331. R-Appchapter-036
  332. Id, Prod-R, Prod-Lchapter-038
  333. Bslash-R, Bslash-Lchapter-038
  334. Slash-R, Slash-Lchapter-038
  335. Id, W, Cchapter-043
  336. Top-R, Top-L, I-R, I-Lchapter-043
  337. And-R, And-L, Or-R_1, Or-R_2chapter-043
  338. Or-L, Imp-R, Imp-Lchapter-043
  339. Star-R, Star-L, Wand-R, Wand-Lchapter-043
  340. Cutchapter-043
  341. E-Skip, E-Assign, E-Loadchapter-044
  342. E-Store, E-Alloc, E-Freechapter-044
  343. E-Seq, E-IfT, E-IfFchapter-044
  344. H-Skip, H-Assign, H-Seq, H-Conseqchapter-044
  345. H-Existschapter-044
  346. H-Load, H-Store, H-Alloc, H-Freechapter-044
  347. H-If, H-Framechapter-044
  348. Move, Drop, Share-begin, Share-nest, Share-end, Share-return, Ex-begin, Ex-reborrow, Ex-pop, Ex-returnchapter-046
  349. Read, Write, Seqchapter-046
  350. Region, Borrowchapter-046
  351. T-LetPropRef, T-VarPropRefchapter-049
  352. T-LetElemRef, T-VarElemRefchapter-049
  353. PSS-Name, PSS-Structchapter-049
  354. PSS-Prop, PSS-Elemchapter-049
  355. RI-Const, RI-Varchapter-050
  356. Cap-LetDec, Cap-Haltchapter-050
  357. L3-New, L3-Freechapter-050
  358. SC-Star, SC-Set-L, SC-Set-R, SC-Varchapter-051
  359. Var-C, Var-X, Abs-C, App-C, TAbs-C, TApp-C, Sub-Cchapter-051
  360. TS-Return, TS-Open, TS-Close, TS-Readchapter-052
  361. TSO-Open, TSO-Close, TSO-Read-More, TSO-Read-Eofchapter-052
  362. F-Const, F-Var, F-Abs, F-Appchapter-053
  363. S-Abs, S-Appchapter-053
  364. L-Var, L-Abs, L-App, L-Weak, L-Der, L-Prom, L-Let, L-Approxchapter-054
  365. G-Var, G-Weak, G-Approx, G-Abs, G-Appchapter-054
  366. EC-Ax, EC-Sub, EC-Abs, EC-App, EC-Unit, EC-LetT, EC-Der, EC-Pr, EC-LetD, EC-Dist, EC-Opchapter-054
  367. RaTT-Var, RaTT-Abs, RaTT-Appchapter-055
  368. RaTT-Delay, RaTT-Adv, RaTT-Box, RaTT-Unboxchapter-055
  369. RaTT-Progress, RaTT-Promotechapter-055
  370. TR-Let, TR-Delay, TR-Box, TR-Unboxchapter-055
  371. Soft-Promotion, Multiplexingchapter-056
  372. 1R, 1L, μltimapR, μltimapL, Cutchapter-058
  373. ⊕R_1, ⊕R_2, ⊕L, _1, _2chapter-058
  374. !R, !L, Copy, Cut!chapter-058
  375. Ctx-Emp, Ctx-Extchapter-071
  376. Presup-Ctx, Presup-Ext, Presup-Ty, Presup-Eq-Ty, Presup-Eq-Tmchapter-071
  377. Ctx-Extchapter-071
  378. Ty-Refl, Ty-Sym, Ty-Trans, Tm-Refl, Tm-Sym, Tm-Transchapter-071
  379. Ctx-Convchapter-071
  380. Subst, Subst-Eq-Ty, Subst-Eq-Tmchapter-071
  381. Substchapter-071
  382. Wkchapter-071
  383. Varchapter-071
  384. Wkchapter-071
  385. Renamechapter-071
  386. Substchapter-071
  387. Convchapter-071
  388. Substchapter-071
  389. Conv-Eqchapter-071
  390. Subst-Eq-Tmchapter-071
  391. Exchchapter-071
  392. Substchapter-071
  393. Assumchapter-071
  394. Q-formchapter-071
  395. Q-formchapter-071
  396. Q-formchapter-071
  397. Q-form-eqchapter-071
  398. Π-form, Π-intro, Π-elim, Π-β, Π-ηchapter-072
  399. Π-form-eq, λ-eq, app-eqchapter-072
  400. Π-elimchapter-072
  401. Π-evchapter-072
  402. Σ-form, Σ-intro, Σ-elim_1, Σ-elim_2, Σ-β_1, Σ-β_2, Σ-ηchapter-072
  403. pair-eq, 1-eq, 2-eqchapter-072
  404. -form, -intro, -ηchapter-072
  405. -form, -elimchapter-073
  406. -form, -intro_1, -intro_2, -elim, -comp_1, -comp_2chapter-073
  407. -elimchapter-073
  408. -ηchapter-073
  409. +-form, +-intro_1, +-intro_2, +-elim, +-comp_1, +-comp_2chapter-073
  410. failedchapter-073
  411. -form, -intro_1, -intro_2, -elim, -comp_1, -comp_2chapter-073
  412. W-form, W-intro, W-elim, W-compchapter-073
  413. U-Form, U-Hier, U-El, U-El-Eqchapter-074
  414. U-Pi, U-Sig, U-Wchapter-074
  415. U-Sum, U-Void, U-Unit, U-Bool, U-Natchapter-074
  416. U-Cumulchapter-074
  417. Lift-U, Lift-Elchapter-074
  418. TU-Form, TU-El, TU-El-Eqchapter-075
  419. TU-Hier, TU-Hier-Elchapter-075
  420. TU-Pi, TU-Sig, TU-Wchapter-075
  421. TU-Pi-El, TU-Sig-El, TU-W-Elchapter-075
  422. TU-Sum, TU-Sum-Elchapter-075
  423. TU-Void, TU-Unit, TU-Bool, TU-Natchapter-075
  424. TU-Void-El, TU-Unit-El, TU-Bool-El, TU-Nat-Elchapter-075
  425. TU-Congchapter-075
  426. Id-form, Id-form-, Id-intro, Id-elim, Id-compchapter-077
  427. Lift-Idchapter-077
  428. Id-form-eqchapter-077
  429. Id-elim-eqchapter-077
  430. Id-elim', Id-comp'chapter-077
  431. Vec-formchapter-078
  432. Vec-elimchapter-078
  433. Fin-elimchapter-078
  434. Rec-form, Rec-introchapter-079
  435. Rec-rest, Rec-projchapter-079
  436. Rec-rest-pass, Rec-proj-passchapter-079
  437. Acc-form, Acc-introchapter-082
  438. Acc-elimchapter-082
  439. Acc-βchapter-082
  440. Lt-zero, Lt-succhapter-082
  441. Mendler-form, Mendler-introchapter-084
  442. Mendler-elimchapter-084
  443. Mendler-βchapter-084
  444. Stream-form, Head, Tailchapter-085
  445. Stream-corecchapter-085
  446. Cutchapter-085
  447. ωStreamchapter-085
  448. Sized-Stream-form, Sized-head, Sized-tailchapter-085
  449. Sized-corecchapter-085
  450. ITree-Ret, ITree-Tauchapter-086
  451. ITree-Vischapter-086
  452. Eutt-Ret, Eutt-Vischapter-086
  453. Eutt-Tau, Eutt-TauL, Eutt-TauRchapter-086
  454. CL-Seq-nilchapter-087
  455. CL-Seq-callchapter-087
  456. CL-Seq-retchapter-087
  457. 1 inference ruleschapter-087
  458. 2 inference ruleschapter-087
  459. CL-Overlay-call, CL-Overlay-retchapter-087
  460. CL-Underlay-call, CL-Underlay-retchapter-087
  461. LHL-Commit-callchapter-088
  462. LHL-Commit-retchapter-088
  463. LHL-Returnchapter-088
  464. LHL-Tauchapter-088
  465. LHL-Vischapter-088
  466. PCUIC-Global-empty, PCUIC-Global-extendchapter-089
  467. PCUIC-Rel, PCUIC-Sortchapter-089
  468. PCUIC-Prod, PCUIC-Lambdachapter-089
  469. PCUIC-Let, PCUIC-Appchapter-089
  470. PCUIC-Const, PCUIC-Indchapter-089
  471. PCUIC-Constructchapter-089
  472. PCUIC-Casechapter-089
  473. PCUIC-Projchapter-089
  474. PCUIC-Fix, PCUIC-CoFixchapter-089
  475. PCUIC-Cumulchapter-089
  476. PCUIC-β, PCUIC-ζchapter-089
  477. PCUIC-Rel-δ, PCUIC-Global-δchapter-089
  478. PCUIC-ιchapter-089
  479. PCUIC-Fix-unfoldchapter-089
  480. PCUIC-CoFix-casechapter-089
  481. PCUIC-CoFix-projchapter-089
  482. PCUIC-Proj-ιchapter-089
  483. Cumul-refl, Cumul-red-l, Cumul-red-rchapter-089
  484. Eq-F, Eq-I, Eq-Reflect, Eq-Uniqchapter-090
  485. Eq-Form-Uchapter-090
  486. Eq-F-eq, Eq-I-eqchapter-090
  487. Convchapter-090
  488. Tr-F, Tr-I, Tr-Uniq, Tr-Echapter-090
  489. Tr-F-eq, Tr-I-eqchapter-090
  490. Tr-E-eqchapter-090
  491. Id-Reflect, Id-Uniqchapter-090
  492. UIP-Ax, Ext-Axchapter-090
  493. SK-K, SK-S, SK-Appchapter-090
  494. C-Π-I, C-Π-E, C-Σ-I, C-Σ-Echapter-091
  495. C-Eq-I, C-Set-I, C-Set-E_1, C-Set-E_2chapter-091
  496. C-Hyp, C-Nat-Succhapter-091
  497. LTT–F, LTT–F, LTT–F, LTT–Fchapter-092
  498. LTT-Hyp, LTT–I, LTT–E, LTT–I, LTT–E, LTT-Classicalchapter-092
  499. LTT–Ichapter-092
  500. LTT-Set-F, LTT-Set-I, LTT-Set-E, LTT-Set-β, LTT-Set-ηchapter-092
  501. LTT-Nat-rec, LTT-Nat-rec-0, LTT-Nat-rec-S, LTT-Nat-Ind_0chapter-092
  502. DI-F, DI-I, DI-E_1, DI-E_2, DI-β_1, DI-β_2, DI-ηchapter-093
  503. DI-Ichapter-093
  504. S–F, S–I, S–E, S–βchapter-094
  505. S-Self-F, S-Self-Gen, S-Self-Inst, S-Self-Erasechapter-094
  506. VDF-F, VDF-I, VDF-E, VDF-β, VDF-Extchapter-095
  507. CDLE-Π-F, CDLE–F, CDLE-Isect-F, CDLE-Eq-Fchapter-096
  508. CDLE-Π-I, CDLE-Π-E, CDLE-Π-β, CDLE–I, CDLE–E, CDLE–βchapter-096
  509. CDLE-Isect-I, CDLE-Isect-E_1, CDLE-Isect-E_2, CDLE-Isect-βchapter-096
  510. CDLE-Eq-I, CDLE-Eq-E, CDLE-φ, CDLE-δ, CDLE-Ascribechapter-096
  511. Mod-Var, Mod-Const, Mod-Typechapter-097
  512. Mod-Pi, Mod-Lam, Mod-Appchapter-097
  513. Mod-Convchapter-097
  514. Mod-Rewrite, Mod-Betachapter-097
  515. LD-μltimap-F, LD-⊗-Fchapter-098
  516. LD-→-F, LD-!-Fchapter-098
  517. LD-Var, LD-Lamchapter-098
  518. LD-App, LD-Pairchapter-098
  519. LD-Letchapter-098
  520. LD-Lift, LD-Forcechapter-098
  521. LD-Param-Lam, LD-Param-App, LD-Param-Forcechapter-098
  522. LD-Eval-App, LD-Eval-Letchapter-098
  523. LD-ConvEvalchapter-098
  524. QTT-Π-F, QTT-Lamchapter-099
  525. QTT-Appchapter-099
  526. QTT-Varchapter-099
  527. QTT-⊗-Fchapter-099
  528. QTT-Pair, QTT-Letchapter-099
  529. G-Typechapter-100
  530. G-Varchapter-100
  531. G-Π-Fchapter-100
  532. G-Lamchapter-100
  533. G-Appchapter-100
  534. G-⊗-Fchapter-100
  535. G-Pairchapter-100
  536. G-Letchapter-100
  537. G-Box-F, G-Box-Ichapter-100
  538. G-Box-Echapter-100
  539. Ctx-ε, Ctx-Ext, V-Zero, V-Succhapter-101
  540. Ty-U, Ty-Π, Ty-Σchapter-101
  541. Code-N, Code-Empty, Code-Π, Code-Σchapter-101
  542. T-Conv, T-Var, T-Lam, T-Appchapter-101
  543. T-Pair, T-Fst, T-Sndchapter-101
  544. T-Prodrecchapter-101
  545. T-Zero, T-Suc, T-Emptyrecchapter-101
  546. T-Natrecchapter-101
  547. Eq-Ty, Eq-Ty-Refl, Eq-Ty-Sym, Eq-Ty-Transchapter-101
  548. Eq-Π, Eq-Σchapter-101
  549. Eq-Refl, Eq-Sym, Eq-Trans, Eq-Convchapter-101
  550. Eq-Π-U, Eq-Σ-U, Eq-Appchapter-101
  551. Eq-β, Eq-ηchapter-101
  552. Eq-Fst-β, Eq-Fst, Eq-Snd-βchapter-101
  553. Eq-Snd, Eq-Σ_&-ηchapter-101
  554. Eq-Pair, Eq-Prodrec-βchapter-101
  555. Eq-Prodrecchapter-101
  556. Eq-Nat-Zero, Eq-Nat-Succhapter-101
  557. Eq-Suc, Eq-Natrecchapter-101
  558. Eq-Emptyrecchapter-101
  559. U-Universe, U-N, U-Empty, U-Var, U-Zerochapter-101
  560. U-Π, U-Σ, U-Lamchapter-101
  561. U-App, U-WeakPair, U-StrongPairchapter-101
  562. U-Fst, U-Snd, U-Succhapter-101
  563. U-Prodrec, U-Emptyrecchapter-101
  564. U-Natrec, U-Subchapter-101
  565. R-Convchapter-101
  566. R-App, R-βchapter-101
  567. R-Fst, R-Fst-βchapter-101
  568. R-Snd, R-Snd-βchapter-101
  569. R-Prodrecchapter-101
  570. R-Prodrec-βchapter-101
  571. R-Natrecchapter-101
  572. R-Nat-Zerochapter-101
  573. R-Nat-Succhapter-101
  574. R-Emptyrecchapter-101
  575. E-App, E-β, E-Fst, E-Fst-βchapter-101
  576. E-Snd, E-Snd-β, E-Prodrec, E-Prodrec-βchapter-101
  577. E-Natrec, E-Nat-Zero, E-Nat-Succhapter-101
  578. Idchapter-102
  579. 2 inference ruleschapter-102
  580. 2 inference ruleschapter-102
  581. ⊕Lchapter-102
  582. _1, ⊕R_1chapter-102
  583. !R, !L, Copychapter-102
  584. Cut, Cut^!chapter-102
  585. 2 inference ruleschapter-102
  586. 2 inference ruleschapter-102
  587. 2 inference ruleschapter-102
  588. Substchapter-103
  589. Dep- B-Echapter-103
  590. Diverge, Rec, Errorchapter-103
  591. Write, Printchapter-103
  592. Choose, Readchapter-103
  593. Return, Thunk, Forcechapter-103
  594. Bind^-chapter-103
  595. Bind^+chapter-103
  596. Nil, To, Argchapter-103
  597. Incl-Write, Incl-Readchapter-103
  598. Incl-Print, Incl-Choosechapter-103
  599. T-Contchapter-103
  600. WP-Subchapter-104
  601. WP-Return, WP-Bindchapter-104
  602. WP-Runchapter-104
  603. R-Runchapter-104
  604. Conv-Return, Conv-Stepchapter-105
  605. Π-F, Π-I, Π-E, Π-Subchapter-106
  606. R-Base-F, R-Π-Fchapter-106
  607. R-Base-Sub, R-Π-Subchapter-106
  608. R-Var, R-Int, R-Arrchapter-106
  609. R-Lam, R-App, R-Subchapter-106
  610. A-Var, A-Int, A-Arrchapter-106
  611. A-Lam, A-App, A-Checkchapter-106
  612. DOT-Var, DOT-All-I, DOT-All-Echapter-107
  613. DOT-Let, DOT-And-I, DOT-Subchapter-107
  614. DOT-Top, DOT-Bot, DOT-Refl, DOT-Transchapter-107
  615. DOT-And_1-, DOT-And_2-, DOT–And, DOT-Fld–Fldchapter-107
  616. DOT-Sel-L, DOT-Sel-U, DOT-Type-Mem-Subchapter-107
  617. DOT-Π-Subchapter-107
  618. DOT-Rec-I, DOT-Rec-E, DOT-Obj-I, DOT-Fld-Echapter-107
  619. DOT-Def-Type, DOT-Def-Val, DOT-Def-Andchapter-107
  620. DOT-T-Sel-L, DOT-T-Sel-Uchapter-107
  621. P-Var, P-Fldchapter-108
  622. Def-Path, Sngl-Trans, Sngl-Echapter-108
  623. RP-Here, RP-Fldchapter-108
  624. R-Sel, R-Snglchapter-108
  625. R-Fld, R-Mem-L, R-Mem-Uchapter-108
  626. R-And-L, R-And-Rchapter-108
  627. R-All-Dom, R-All-Codchapter-108
  628. R-Recchapter-108
  629. Repl-pqchapter-108
  630. Repl-qpchapter-108
  631. Def-Newchapter-108
  632. Lookup-Var, Lookup-Val, Lookup-Pathchapter-108
  633. Cut, μ-R, μ-Lchapter-109
  634. Π-R, Π-Lchapter-109
  635. -R, Wit, Prfchapter-109
  636. μtp, tp, Cut-d, μ-dchapter-109
  637. -Lchapter-109
  638. Pre-Pi, Pre-Var, Pre-Lam, Pre-Appchapter-110
  639. Ty-Pi, Ty-Sg, Ty-Id, Ty-1, Ty-, Ty-, Ty-Vec, Ty-Univ, Ty-Elchapter-110
  640. Syn-Var, Syn-App, Syn-Fst, Syn-Snd, Syn-★, Syn-Zero, Syn-Suc, Syn-True, Syn-False, Syn-Annchapter-110
  641. Syn-BoolInd, Syn-NatInd, Syn-Jchapter-110
  642. Syn-VNilchapter-110
  643. Syn-VConschapter-110
  644. Syn-VecIndchapter-110
  645. Chk-Lam, Chk-Pair, Chk-Refl, Chk-Convchapter-110
  646. Chk-Code-1, Chk-Code-, Chk-Code-, Chk-Code-Univchapter-110
  647. Chk-Code-Pi, Chk-Code-Sg, Chk-Code-Id, Chk-Code-Lift, Chk-Code-Vecchapter-110
  648. Syn-Var-Plain, Syn-Var-Defchapter-110
  649. Decls-Nil, Decls-Conschapter-110
  650. ne-var, ne-app, ne-fst, ne-snd, ne-ind-bool, ne-ind-nat, ne-J, ne-vindchapter-111
  651. nf-lam, nf-pair, nf-star, nf-true, nf-false, nf-zero, nf-suc, nf-refl, nf-vnil, nf-vcons, nf-nechapter-111
  652. nf-cd-K, nf-cd-univ, nf-cd-pi, nf-cd-sg, nf-cd-id, nf-cd-vec, nf-cd-liftchapter-111
  653. nf-ty-univ, nf-ty-pi, nf-ty-sg, nf-ty-K, nf-ty-id, nf-ty-vec, nf-ty-nechapter-111
  654. Clos-Raw, Clos-Lift, Clos-Step-1, Clos-Step-2chapter-111
  655. E-Syn-Var, E-Syn-Atom, E-Chk-Hole, E-Chk-Syn, E-Chk-Lamchapter-112
  656. E-Chk-Univchapter-112
  657. E-Syn-Hole, E-Syn-Ann, E-Ty-Holechapter-112
  658. E-Ty-Elchapter-112
  659. E-Ty-Univchapter-112
  660. E-Ty-Basechapter-112
  661. E-Ty-Idchapter-112
  662. E-Ty-Vecchapter-112
  663. E-Ty-Pichapter-112
  664. E-Ty-Sigmachapter-112
  665. E-Chk-Pair, E-Syn-Fst, E-Syn-Sndchapter-112
  666. E-Syn-Appchapter-112
  667. E-Spine-Donechapter-112
  668. E-Spine-Insertchapter-112
  669. E-Spine-Consumechapter-112
  670. E-Syn-Headchapter-112
  671. E-Head-Donechapter-112
  672. E-Head-Inferchapter-112
  673. E-Head-Writechapter-112
  674. P-Var, P-Atom, P-Hole, P-Ann, P-Lam, P-Pairchapter-112
  675. P-Ty-El, P-Ty-Univ, P-Ty-Basechapter-112
  676. P-Ty-Id, P-Ty-Vecchapter-112
  677. P-Ty-Pi, P-Ty-Sigmachapter-112
  678. P-App, P-Spine-Done, P-Spine-Insert, P-Spine-Consumechapter-112
  679. P-Headchapter-112
  680. Tac-Exact-Fail, Tac-Intro-Failchapter-114
  681. Tac-Split-Fail, Tac-Assumption-Failchapter-114
  682. Tac-Seqchapter-114
  683. Tac-Seq-Fail_1, Tac-Seq-Fail_2chapter-114
  684. Tac-Or-Left, Tac-Or-Right, Tac-Or-Failchapter-114
  685. Rep-Stepchapter-114
  686. Rep-Done, Rep-Morechapter-114
  687. Rw-Root, Rw-Atom, Rw-App, Rw-Lam, Rw-Subchapter-115
  688. Exp-Args-Nil, Exp-Args-Conschapter-116
  689. Exp-Var, Exp-Lam, Exp-App, Exp-Quote, Exp-Splice, Exp-Macrochapter-116
  690. Q-Quote, Q-Splice, Q-Varchapter-116
  691. Src-Var, Src-Lam, Src-App, Src-Quote, Src-Splice, Src-Macrochapter-116
  692. Level, L-Zero, L-Suc, L-Join, L-Univchapter-117
  693. Lift-F, Lift-I, Lift-Echapter-117
  694. Lift-β, Lift-ηchapter-117
  695. Same-Sortchapter-118
  696. DT-Type, DT-Pi, DT-AppTychapter-118
  697. Coe-Id, Coe-Edge, Coe-Comp, Coe-Convchapter-119
  698. Subchapter-119
  699. Coe-Var, Coe-Ann, Coe-App, Coe-Pair, Coe-Lam, Coe-Insertchapter-119
  700. Map-Ty, Map-Id, Map-Compchapter-120
  701. Desc-Map-Neutralchapter-120
  702. Desc-Map-Id, Desc-Map-Compchapter-120
  703. Ctx-Hole, Ctx-Framechapter-120
  704. Frame-Mapchapter-120
  705. Frame-ListInd, Frame-Sndchapter-120
  706. Select-Here, Select-Underchapter-120
  707. S0-Const, S0-Var, S0-Opchapter-127
  708. S0-If-F, S0-If-Tchapter-127
  709. S0-Callchapter-127
  710. PE-Num, PE-Static, PE-Dynamicchapter-127
  711. PE-Op-S, PE-Op-Dchapter-127
  712. PE-If-Z, PE-If-Nchapter-127
  713. PE-If-Dchapter-127
  714. N-Callchapter-127
  715. PE-Call-Hit, PE-Fuelchapter-127
  716. PE-Call-Newchapter-127
  717. N-Letchapter-127
  718. BT-Const, BT-Var, BT-Op-Schapter-127
  719. BT-Op-D, BT-If-Schapter-127
  720. BT-If-D, BT-Call-S0chapter-127
  721. BT-Call-S, BT-Call-Dchapter-127
  722. BT-Liftchapter-127
  723. Off-Const, Off-Var-S, Off-Var-Dchapter-127
  724. Off-Op-S, Off-Op-Dchapter-127
  725. Off-If-S, Off-If-Dchapter-127
  726. Off-Call-S, Off-Call-Dchapter-127
  727. Off-Liftchapter-127
  728. D-Betachapter-128
  729. D-Case-Known, D-Case-Openchapter-128
  730. Emb-Var, Emb-Num, Emb-Dive, Emb-Couplechapter-128
  731. T-Var, T-MVar, T-Abs, T-Appchapter-129
  732. T-Box, T-LetBoxchapter-129
  733. TS-Beta, TS-BoxBetachapter-129
  734. TS-Lam, TS-AppL, TS-AppRchapter-129
  735. TS-LetL, TS-LetRchapter-129
  736. Pers-Base, Pers-Codechapter-129
  737. MML-Quote, MML-Escape, MML-CSPchapter-129
  738. 2-Varp, 2-Lamp, 2-Apppchapter-129
  739. 2-Fixp, 2-Pairp, 2-Projpchapter-129
  740. 2-Unitp, 2-Zerop, 2-Succpchapter-129
  741. 2-Casepchapter-129
  742. 2-Down, 2-Upchapter-129
  743. I-Var, I-Abs, I-Appchapter-129
  744. I-Box, I-Unbox1chapter-129
  745. I-Fix, I-Pair, I-Projchapter-129
  746. I-Unit, I-Zero, I-Succchapter-129
  747. I-Casechapter-129
  748. A-Nat, A-SVar, A-DVarchapter-129
  749. A-Op-S, A-Op-Dchapter-129
  750. MC-Quote, MC-Splicechapter-129
  751. MC-CodeGenchapter-129
  752. TW-Pure, TW-Repchapter-129
  753. TW-Code, TW-Reflect, TW-LetCchapter-129
  754. MD-Kind-Star, MD-Kind-Pi, MD-TConstchapter-130
  755. MD-TApp, MD-TCode, MD-TForallchapter-130
  756. MD-TCSP, MD-TConvchapter-130
  757. MD-Pi, MD-Abs, MD-Appchapter-130
  758. MD-Const, MD-Var, MD-Convchapter-130
  759. MD-Quote, MD-Escapechapter-130
  760. MD-SAbs, MD-SAppchapter-130
  761. MD-CSPchapter-130
  762. MD-QK-Pi, MD-QK-CSPchapter-130
  763. MD-QK-Refl, MD-QK-Sym, MD-QK-Transchapter-130
  764. MD-QT-Pi, MD-QT-Appchapter-130
  765. MD-QT-Code, MD-QT-Forall, MD-QT-CSPchapter-130
  766. MD-QT-Refl, MD-QT-Sym, MD-QT-Transchapter-130
  767. MD-Q-Abs, MD-Q-Appchapter-130
  768. MD-Q-Quote, MD-Q-Escapechapter-130
  769. MD-Q-SAbs, MD-Q-SApp, MD-Q-CSPchapter-130
  770. MD-Q-Refl, MD-Q-Sym, MD-Q-Transchapter-130
  771. MD-Q-Beta, MD-Q-Splicechapter-130
  772. MD-Q-StageBeta, MD-Q-Percentchapter-130
  773. WP-Refl, WP-Congchapter-130
  774. WP-Beta, WP-Splice, WP-StageBetachapter-130
  775. Star, FunK, EqTy, EqCochapter-131
  776. TyVar, TyApp, TySCon, TyAllchapter-131
  777. CoRefl, CoVar, Sym, Transchapter-131
  778. CoAllT, CoInstTchapter-131
  779. Comp, SCompchapter-131
  780. Left, Rightchapter-131
  781. CompC, LeftC, RightCchapter-131
  782. EqCoerce, CastCchapter-131
  783. Var, Abs, App, Letchapter-131
  784. AbsT, AppT, Castchapter-131
  785. Case, Altchapter-131
  786. Data, Type, Coercechapter-131
  787. Left^r, Right^r, EqCoerce^rchapter-131
  788. CoAllT^r, CompC^rchapter-131
  789. G-Var, G-Eq, G-Gen, G-Instchapter-131
  790. G-CIntro, G-CElimchapter-131
  791. G-Altchapter-131
  792. E-AppAbs, E-CAppCAbs, E-Axiomchapter-132
  793. E-Prim, E-AbsTerm, E-AppLeft, E-CAppLeftchapter-132
  794. E-Star, E-Var, E-Pi, E-Abschapter-132
  795. E-App, E-IApp, E-Conv, E-Famchapter-132
  796. E-CPi, E-CAbs, E-CApp, E-Wffchapter-132
  797. E-Refl, E-Sym, E-Trans, E-Betachapter-132
  798. E-PiFst, E-PiSndchapter-132
  799. E-Assnchapter-132
  800. E-CPiCongchapter-132
  801. An-Abs, An-App, An-Conv, An-CAppchapter-132
  802. An-Refl, An-Assn, An-Beta, An-PiFstchapter-132
  803. An-PiCongchapter-132
  804. C-Fix, C-Pack, C-TAppchapter-133
  805. A-Proj, A-Malloc, A-Initchapter-133
  806. Ax-★, Var, Let, Prodchapter-137
  807. Lam, App, Conv, Sigchapter-137
  808. T-Code, Code, Clochapter-137
  809. -Clochapter-137
  810. -Clo_1chapter-137
  811. Snd, Ifchapter-138
  812. Letchapter-138
  813. If^δchapter-138
  814. -Reflectchapter-138
  815. K-Empty, K-Letchapter-138
  816. t-int, t-var, t-inst, t-relaxchapter-139
  817. t-index, t-iota, t-mapchapter-139
  818. t-lam, t-app, t-coercechapter-139
  819. t-let, t-let-genchapter-139
  820. d-iota, d-coerce, d-letchapter-139
  821. Ctx-Emp, Ctx-Extchapter-146
  822. Sb-Ty, Sb-Tmchapter-146
  823. Sb-Id, Sb-Comp, Sb-IdL, Sb-IdR, Sb-Assocchapter-146
  824. Ty-Id, Tm-Id, Ty-Comp, Tm-Compchapter-146
  825. Sb-Wk, Tm-Vzchapter-146
  826. Sb-Emp, Sb-Emp-Uniqchapter-146
  827. Sb-Ext, Ext-Wk, Ext-Vz, Ext-Uniqchapter-146
  828. Sb-Tmchapter-146
  829. Pi-Form, Pi-Intro, Pi-Elim, Pi-Beta, Pi-Eta, Pi-Sb, Lam-Sb, App-Sbchapter-146
  830. 4 inference ruleschapter-154
  831. Box-I, Box-Echapter-160
  832. DBox-F, DBox-I, DBox-Echapter-160
  833. MTT-Varchapter-160
  834. MTT-F, MTT-Ichapter-160
  835. Glue-F, Glue-Syn, Glue-I, Glue-E, Glue-C, Glue-U, Glue-Elt-Synchapter-161
  836. DS-Emp, DS-Cons, Later-F, Later-I, Later-Code, Fixchapter-162
  837. All-F, All-I, All-E, Prevchapter-162
  838. Get, Setchapter-163
  839. S-Inf, S-Var, S-Bound, S-InfInf, S-Off, S-VarInf, S-Weakchapter-165
  840. Mu-I, Nu-Echapter-165
  841. Clause, Clauseschapter-165
  842. Size-F, Size-Z, Size-S, Le-F, Le-Z, Le-S, Le-Refl, Le-Transchapter-166
  843. Ex-F, All-F, Ex-I, Ex-E, All-I, All-Echapter-166
  844. Fix, Fix-βchapter-166
  845. Span, Ap, Spand, Apd, Leg, Refl, Sym, Unspanchapter-167
  846. MkPichapter-167
  847. Unit, Var, InL, InR, Pair, Fold, App, Let, IVar, IFix, ILam, IApp, Clauseschapter-168
  848. Num, Var, Succ, Coinchapter-171
  849. If, Lamchapter-171
  850. App, Fixchapter-171
  851. Det, Coin-0, Coin-1chapter-171
  852. Ctx-App, Ctx-Succ, Ctx-Ifchapter-171
  853. Holechapter-171
  854. Dist, Ret, Bindchapter-172
  855. Ret, Coinchapter-176
  856. Bindchapter-176
  857. Choicechapter-176
  858. Union, Weakenchapter-176
  859. L:Flip, L:Tickchapter-177
  860. L:Prob, L:FlipSchapter-177
  861. ht-rand-exp, ht-rand-errchapter-178
  862. ht-frame, ht-bindchapter-178
  863. F-Val, F-Loop, F-Weakchapter-178
  864. F-Bind, F-Failchapter-178
  865. HD-Fail, HD-Valchapter-179
  866. HD-RandDetchapter-179
  867. HD-Randchapter-179
  868. HD-Ifchapter-179
  869. UAchapter-193
  870. Trunc-F, Trunc-I, Trunc-Sq, Trunc-E, Trunc-Cchapter-195
  871. Trunc_n-F, Trunc_n-I, Trunc_n-T, Trunc_n-E, Trunc_n-Cchapter-195
  872. 1-form, 1-form-, 1-intro_1, 1-intro_2, 1-elim, 1-comp_1, 1-comp_2chapter-198
  873. I-form, I-intro_1, I-intro_2, I-intro_3, I-elim, I-comp_1, I-comp_2, I-comp_3chapter-198
  874. Susp-form, Susp-intro_1, Susp-intro_2, Susp-intro_3, Susp-elim, Susp-comp_1, Susp-comp_2, Susp-comp_3chapter-198
  875. Po-form, Po-intro_1, Po-intro_2, Po-intro_3, Po-elim, Po-comp_1, Po-comp_2, Po-comp_3chapter-198
  876. Tr-form, Tr-intro_1, Tr-intro_2, Tr-elim, Tr-comp_1, Tr-comp_2chapter-198
  877. Tr_0-elim, Tr_0-compchapter-198
  878. Q-form, Q-form-, Q-elim, Q-compchapter-198
  879. Acc-Introchapter-210
  880. Rc-Rat, Rc-Lim, Rc-Eqchapter-212
  881. Cl-RR, Cl-RL, Cl-LR, Cl-LL, Cl-Propchapter-212
  882. Sort-F, Cum, Irrchapter-215
  883. Bot-F, Bot-E, Top-F, Top-I, Ex-F, Ex-I, Ex-E1, Ex-E2, Pi-Prop-Fchapter-215
  884. Obs-F, Obs-I, Transp, Cast, Cast-Reflchapter-215
  885. Obs-Pi, Obs-Sg, Obs-Nat-ZZ, Obs-Nat-SS, Obs-Nat-ZS, Obs-Nat-SZ, Obs-Boolchapter-215
  886. Obs-Prop, Obs-U-Atom, Obs-U-Neq, Obs-U-Pi, Obs-U-Sgchapter-215
  887. Cast-Nat-Z, Cast-Nat-S, Cast-Bool, Cast-U, Cast-Pi, Cast-Sgchapter-215
  888. Quo-F, Quo-I, Obs-Quo, Cast-Quo, Obs-U-Quo, Quo-E-Rel, Quo-C-Rel, Quo-E-Irr, Quo-C-Irrchapter-215
  889. Het-Eq, Coe, Cohchapter-215
  890. Ctx-Dimchapter-217
  891. Path-form, Path-intro, Path-elim, Path-β, Path-_0, Path-_1, Path-ηchapter-217
  892. PathP-form, PathP-intro, PathP-elimchapter-217
  893. Ctx-Restrchapter-217
  894. Sys-form, Sys-intro, Sys-sel, Sys-globchapter-217
  895. Compchapter-217
  896. Glue-form, Glue-form-1, Glue-intro, Glue-intro-1, Glue-elim, Glue-β, Glue-ηchapter-217
  897. -form, -Russellchapter-217
  898. i-zero, i-one, i-varchapter-218
  899. cof-eq, cof-disj, cof-forallchapter-218
  900. cof-refl, cof-reflect, cof-absurd, cof-case, cof-extchapter-218
  901. coe, coe-id, hcom, hcom-cap, hcom-tubechapter-218
  902. v-form, v-intro, v-elimchapter-218
  903. Nat-Z, Nat-S, Tree-Emp, Tree-Nodeappendix-rules-001
  904. Is-Z, Is-S, List-Nil, List-Consappendix-rules-001
  905. Ev-Z, Ev-S, Od-S, Sum-Z, Sum-Sappendix-rules-001
  906. Nat-SS, Ev-Invappendix-rules-001
  907. Hypappendix-rules-001
  908. Num-Z, Num-Sappendix-rules-001
  909. A-Suc, A-Add-L, A-Add-Rappendix-rules-001
  910. A-Add-Z, A-Add-Sappendix-rules-001
  911. M-Refl, M-Step, AB-Z, AB-S, AB-Addappendix-rules-001
  912. V-Lam, V-True, V-False, V-Numappendix-rules-001
  913. E-App-L, E-App-R, E-Betaappendix-rules-001
  914. E-If, E-If-T, E-If-F, E-Sucappendix-rules-001
  915. E-Add-L, E-Add-R, E-Add-Z, E-Add-Sappendix-rules-001
  916. CBV-Reflappendix-rules-001
  917. CBV-Stepappendix-rules-001
  918. B-Val, B-App, B-If-Tappendix-rules-001
  919. B-If-F, B-Suc, B-Addappendix-rules-001
  920. Ty-Atom, Ty-Bool, Ty-Arr, Cx-Emp, Cx-Extappendix-rules-002
  921. Var, True, False, Ifappendix-rules-002
  922. Lam, Appappendix-rules-002
  923. E-AppL, E-AppR, E-Betaappendix-rules-002
  924. E-If, E-True, E-Falseappendix-rules-002
  925. Ty-Prod, Ty-Sum, Ty-Unit, Ty-Emptyappendix-rules-002
  926. Pair, Fst, Snd, Unit-Iappendix-rules-002
  927. Inl, Inr, Case, Empty-Eappendix-rules-002
  928. E-PairL, E-PairR, E-Fst, E-Fst-Pairappendix-rules-002
  929. E-Snd, E-Snd-Pair, E-Inl, E-Inrappendix-rules-002
  930. E-Case, E-Case-L, E-Case-R, E-Abortappendix-rules-002
  931. Hyp, →p I, E, Iappendix-rules-002
  932. E_1, E_2, I, Eappendix-rules-002
  933. I_1, I_2, Eappendix-rules-002
  934. Hyp, Bot-E, And-I, And-E_iappendix-rules-003
  935. Or-I_1, Or-I_2, Or-E, Imp-I, Imp-Eappendix-rules-003
  936. All-I, All-E, Some-I, Some-Eappendix-rules-003
  937. Ax, Cut, W-L, C-L, Bot-Lappendix-rules-003
  938. And-R, And-L_i, Or-R_1, Or-R_2, Or-Lappendix-rules-003
  939. Imp-R, Imp-L, All-R, All-Lappendix-rules-003
  940. Some-R, Some-Lappendix-rules-003
  941. I, E, Iappendix-rules-003
  942. E, Eappendix-rules-003
  943. Var, Inst, Gen, Lam, App, Letappendix-rules-004
  944. N-Z, N-Sappendix-rules-004
  945. C-Var, C-Lam, C-Appappendix-rules-004
  946. S-Var, S-Lam, S-App, S-Letappendix-rules-004
  947. ListNil, ListCons, S-ListNil, S-ListCons, ListCase, S-ListCaseappendix-rules-004
  948. Unit, Ref, Deref, Assignappendix-rules-004
  949. Let-Gen, Let-Monoappendix-rules-004
  950. S-Let-Gen, S-Let-Monoappendix-rules-004
  951. S-Unit, S-Ref, S-Deref, S-Assignappendix-rules-004
  952. Loc, GenΣ, Let-GenΣappendix-rules-004
  953. MM-Fixappendix-rules-005
  954. FO-Var, FO-Abs, FO-App, FO-Let, FO-Fixappendix-rules-005
  955. F-TVar, F-Num, F-Arrowappendix-rules-006
  956. D-Lit, D-Add, D-Mulappendix-rules-006
  957. D-Div, D-Powappendix-rules-006
  958. C-Var, C-Lam, C-App, C-Letappendix-rules-006
  959. C-Lit, C-Add, C-Mulappendix-rules-006
  960. C-Div, C-Pow, C-ArithErrappendix-rules-006
  961. L-Assume, L-Empty, L-Extendappendix-rules-007
  962. Row-Var, Row-Empty, Row-Extappendix-rules-007
  963. Ty-Arrow, Ty-Record, Ty-Variantappendix-rules-007
  964. Q-Var, Q-Const, Q-Lamappendix-rules-007
  965. Q-App, Q-Let, Q-Convappendix-rules-007
  966. Q-Empty, Q-Select, Q-Restrictappendix-rules-007
  967. Q-Extend, Q-Inject, Q-Embedappendix-rules-007
  968. Q-Caseappendix-rules-007
  969. Ev-Assume, Ev-Empty, Ev-Before, Ev-Afterappendix-rules-007
  970. T-Convappendix-rules-007
  971. T-Var, T-Const, T-Inst, T-Ev-Abs, T-Letappendix-rules-007
  972. T-MVar, T-MConst, T-Lam, T-Appappendix-rules-007
  973. T-Empty, T-Lookup, T-Delete, T-Insert, T-Tagappendix-rules-007
  974. T-Widen, T-Splitappendix-rules-007
  975. K-Recappendix-rules-008
  976. R-Record, R-Dotappendix-rules-008
  977. V-Nth, V-IAbs, V-IAppappendix-rules-008
  978. F-Δ-Emp, F-Δ-Ext, F-Γ-Emp, F-Γ-Extappendix-rules-009
  979. F-Ty-Var, F-Ty-Arr, F-Ty-Allappendix-rules-009
  980. F-Var, F-Arr-I, F-Arr-E, F-All-I, F-All-Eappendix-rules-009
  981. P-Var, P-Lam, P-App, P-TLamappendix-rules-009
  982. P-TApp, P-Beta, P-TBetaappendix-rules-009
  983. C-Var, C-Arr-I, C-Arr-E, C-All-I, C-All-Eappendix-rules-009
  984. KCtx-Empty, KCtx-Extappendix-rules-010
  985. K-Var, K-Nat, K-Arr, K-Prod, K-All, K-Some, K-Abs, K-Appappendix-rules-010
  986. TR-Beta, TR-App_1, TR-App_2, TR-Arr_1, TR-Arr_2, TR-Prod_1, TR-Prod_2appendix-rules-010
  987. TR-Abs, TR-All, TR-Someappendix-rules-010
  988. Q-Refl, Q-Sym, Q-Trans, Q-Betaappendix-rules-010
  989. Q-Arr, Q-Prod, Q-All, Q-Some, Q-Abs, Q-Appappendix-rules-010
  990. Ctx-Empty, Ctx-Extappendix-rules-010
  991. T-Var, T-Lam, T-App, T-TLam, T-TApp, T-Pair, T-Prj, T-Zero, T-Suc, T-Convappendix-rules-010
  992. T-Pack, T-Unpackappendix-rules-010
  993. E-Beta, E-TBeta, E-PrjPairappendix-rules-010
  994. E-App_1, E-App_2, E-TApp, E-Pair_1appendix-rules-010
  995. E-Pair_2, E-Prj, E-Sucappendix-rules-010
  996. Rec-F, Rec-I, Rec-E, Q-Recappendix-rules-010
  997. E-Local, E-Instanceappendix-rules-011
  998. Q-Var, Q-Lam, Q-App, Q-Letappendix-rules-011
  999. U-DictLam, U-DictAppappendix-rules-011
  1000. D-Var, D-Lamappendix-rules-011
  1001. D-Appappendix-rules-011
  1002. D-Letappendix-rules-011
  1003. ED-Method, ED-Bind, ED-Dischargeappendix-rules-011
  1004. C-R-Main, C-R-IAbs, C-R-Simpappendix-rules-011
  1005. C-L-Match, C-L-NoMatchappendix-rules-011
  1006. C-M-Simp, C-M-IApp, C-M-TAppappendix-rules-011
  1007. Sing-Kind, Sing-I, Sing-Sub, Sing-Eappendix-rules-012
  1008. B-Sig, Sigma-Sig, Pi-Sigappendix-rules-012
  1009. B-Eq, Sigma-Eq, Pi-Eqappendix-rules-012
  1010. V-Var, V-Basic, V-Hierarchy, V-Functorappendix-rules-012
  1011. P-Var, P-Basic, P-Hierarchy, P-Projectionappendix-rules-012
  1012. Var, Basic, Seal, Subappendix-rules-012
  1013. Let, Hierarchy, First, Secondappendix-rules-012
  1014. Static, Dynamic, Selfappendix-rules-012
  1015. Self-First, Self-Second, Functor, Applyappendix-rules-012
  1016. Sig-Refl, Sig-Trans, Sig-Convertappendix-rules-012
  1017. B-Match, Sigma-Match, Pi-Matchappendix-rules-012
  1018. M-Context, D-Context, Basic-Contextappendix-rules-012
  1019. Mix-Imp, Mix-Defappendix-rules-013
  1020. Mix-Withappendix-rules-013
  1021. Mix-Struct, Mix-Sealappendix-rules-013
  1022. Mix-Completeappendix-rules-013
  1023. Slot-Return, Slot-Get, Slot-Setappendix-rules-013
  1024. Slot-Seq, Slot-Newappendix-rules-013
  1025. Tr-Empty, Tr-Get, Tr-Setappendix-rules-013
  1026. Tr-Seq, Tr-Newappendix-rules-013
  1027. R-Base, R-Functorappendix-rules-014
  1028. T-EvPath, T-EvFunctorappendix-rules-014
  1029. E-Eq, E-Showappendix-rules-014
  1030. Mod-Path, Mod-Functor, Mod-Fieldappendix-rules-014
  1031. MI-Callappendix-rules-014
  1032. SI-Var, SI-Query, SI-ArrI, SI-ArrEappendix-rules-014
  1033. SI-ImpI, SI-ImpE, SI-AllI, SI-AllEappendix-rules-014
  1034. SI-LetEx, SI-LetIm, SI-Stitchappendix-rules-014
  1035. B-Ty-Top, B-Ty-Bot, B-Ty-Unit, B-Ty-Bool, B-Ty-Natappendix-rules-015
  1036. B-Ty-Arr, B-Ty-Prod, B-Ty-Sum, B-Ty-Rcdappendix-rules-015
  1037. S-Refl, S-Trans, S-Top, S-Botappendix-rules-015
  1038. S-Arr, S-Prod, S-Sum, S-Rcdappendix-rules-015
  1039. T-Zero, T-Suc, T-NatRecappendix-rules-015
  1040. T-Sub, T-Rcd, T-Projappendix-rules-015
  1041. E-Suc, E-NatRec, E-NatZero, E-NatSucappendix-rules-015
  1042. E-Rcd, E-Proj, E-ProjCongappendix-rules-015
  1043. C-Empty, C-Term, C-Typeappendix-rules-015
  1044. B-Ty-Var, B-Ty-Allappendix-rules-015
  1045. S-Var, S-AllK, T-TAbs, T-TAppappendix-rules-015
  1046. A-Eq, A-Top, A-Bot, A-Varappendix-rules-015
  1047. A-Arr, A-Prod, A-Sumappendix-rules-015
  1048. A-Rcd, A-AllKappendix-rules-015
  1049. S-AllFappendix-rules-015
  1050. Var-Let, Var-Lam, Absappendix-rules-016
  1051. App, Letappendix-rules-016
  1052. Unit, Bool, If, Subappendix-rules-016
  1053. E-Beta, E-Projappendix-rules-017
  1054. E-Case+, E-Case-appendix-rules-017
  1055. T-Const, T-Var, T-Pairappendix-rules-017
  1056. T-Sub, T-Inter, T-Projappendix-rules-017
  1057. T-Abs, T-Appappendix-rules-017
  1058. T-App-Synappendix-rules-017
  1059. _1, _2appendix-rules-017
  1060. T-Caseappendix-rules-017
  1061. DT-Var, DT-Int, DT-Lam, DT-Appappendix-rules-018
  1062. DT-Pair, DT-Projappendix-rules-018
  1063. S-Int, S-Arr, S-Prodappendix-rules-018
  1064. S-&R, S-&L_1, S-&L_2appendix-rules-018
  1065. WF-&appendix-rules-018
  1066. I-Var, I-Int, I-Pairappendix-rules-018
  1067. I-App, I-Proj, I-Mergeappendix-rules-018
  1068. I-Ann, I-Lam, I-Subappendix-rules-018
  1069. E-Shift, E-Len, E-Getappendix-rules-019
  1070. E-Beta, E-Fixappendix-rules-019
  1071. E-IfT, E-IfFappendix-rules-019
  1072. WF-Empty, WF-Var, WF-Guardappendix-rules-019
  1073. WF-Base, WF-Arrowappendix-rules-019
  1074. S-Base, S-Arrowappendix-rules-019
  1075. D-Var, D-Int, D-Arrayappendix-rules-019
  1076. D-Lam, D-Fixappendix-rules-019
  1077. D-Shift, D-Lengthappendix-rules-019
  1078. D-Get, D-Appappendix-rules-019
  1079. D-Sub, D-Letappendix-rules-019
  1080. D-If, D-Errorappendix-rules-019
  1081. ST-Var, ST-Int, ST-Arrayappendix-rules-019
  1082. ST-Lam, ST-Fixappendix-rules-019
  1083. ST-Shift, ST-Lengthappendix-rules-019
  1084. ST-Get, ST-Appappendix-rules-019
  1085. ST-Atom, ST-Letappendix-rules-019
  1086. ST-If, ST-Errorappendix-rules-019
  1087. C-UnkL, C-UnkR, C-Bool, C-Nat, C-Arrappendix-rules-020
  1088. G-Bool, G-Nat, G-Var, G-Lam, G-Appappendix-rules-020
  1089. T-Bool, T-Nat, T-Var, T-Lam, T-Appappendix-rules-020
  1090. T-Cast, T-Blameappendix-rules-020
  1091. E-Beta, E-IdBase, E-IdUnkappendix-rules-020
  1092. E-Project, E-Mismatchappendix-rules-020
  1093. E-Ground, E-Expandappendix-rules-020
  1094. E-WrapApp, E-Blameappendix-rules-020
  1095. P-Bool, P-Nat, P-Unk, P-Arrappendix-rules-020
  1096. N-Bool, N-Nat, N-Unk, N-GroundUnk, N-Arrappendix-rules-020
  1097. I-Bool, I-Nat, I-Var, I-Lamappendix-rules-020
  1098. I-Appappendix-rules-020
  1099. Pr-Unk, Pr-Bool, Pr-Nat, Pr-Arrappendix-rules-020
  1100. PrCtx-Empty, PrCtx-Extendappendix-rules-020
  1101. PrTm-Bool, PrTm-Nat, PrTm-Var, PrTm-Lam, PrTm-Appappendix-rules-020
  1102. CPr-Bool, CPr-Nat, CPr-Varappendix-rules-020
  1103. CPr-Lam, CPr-Appappendix-rules-020
  1104. CPr-Castappendix-rules-020
  1105. CPr-CastL, CPr-CastR, CPr-Blameappendix-rules-020
  1106. FPr-AppL, FPr-AppRappendix-rules-020
  1107. FPr-Castappendix-rules-020
  1108. FPr-Hole, FPr-Consappendix-rules-020
  1109. Nat-F, T-Nat, Mu-F, T-Fold, T-Unfoldappendix-rules-021
  1110. E-UnfoldFoldappendix-rules-021
  1111. P-Succ, P-Ifz, P-Fixappendix-rules-021
  1112. P-Beta, P-SuccN, P-IfZappendix-rules-021
  1113. P-IfS, P-Unrollappendix-rules-021
  1114. Obs-Zero, Obs-Consappendix-rules-021
  1115. Pr-Fix, Pr-Unrollappendix-rules-021
  1116. T-Object, T-Invoke, T-Overrideappendix-rules-022
  1117. S-Top, S-Object, T-Subappendix-rules-022
  1118. M-Object, M-Overrideappendix-rules-022
  1119. M-Invokeappendix-rules-022
  1120. FT-Arr, FT-Record, FT-Exists, FT-Muappendix-rules-022
  1121. S-Refl, S-Trans, S-Bound, S-Topappendix-rules-022
  1122. S-Arr, S-Rec, S-Exists, S-Amberappendix-rules-022
  1123. F-Var, F-Sub, F-Lam, F-Appappendix-rules-022
  1124. F-Record, F-Projappendix-rules-022
  1125. F-Pack, F-Open, F-Fold, F-Unfoldappendix-rules-022
  1126. F-Letrecappendix-rules-022
  1127. S-Bound, S-Top, S-Arrow, S-Recordappendix-rules-024
  1128. T-Var, T-Const, T-Bool, T-Unitappendix-rules-024
  1129. T-Succ, T-Abs, T-Appappendix-rules-024
  1130. T-If, T-Record, T-Projappendix-rules-024
  1131. T-Fix, T-Subappendix-rules-024
  1132. S-Self, T-PackSelf, T-UseSelfappendix-rules-024
  1133. F-All, F-Intro, F-Elimappendix-rules-024
  1134. S-H-Arrow, S-H-Recordappendix-rules-024
  1135. T-H-Var, T-H-Abs, T-H-Appappendix-rules-024
  1136. T-H-Record, T-H-Proj, T-H-Subappendix-rules-024
  1137. K-OpAbs, K-OpApp, K-Muappendix-rules-024
  1138. S-OpPoint, S-OpApp, S-OpBoundappendix-rules-024
  1139. K-AllOp, T-AllOp-I, T-AllOp-Eappendix-rules-024
  1140. T-Fold, T-Unfoldappendix-rules-024
  1141. T-Match-Var, T-Match-Abs, T-Match-Appappendix-rules-024
  1142. T-Match-I, T-Match-E, T-Match-Projappendix-rules-024
  1143. T-Ref, T-Deref, T-Assign, T-Locappendix-rules-024
  1144. S-Var, S-Const, S-Lam, S-Appappendix-rules-025
  1145. V-Val, V-App, N-Val, N-Appappendix-rules-025
  1146. V-Var, V-Const, V-Thunk, C-Returnappendix-rules-025
  1147. C-To, C-Force, C-Lam, C-Appappendix-rules-025
  1148. V-Thunk^Σ, C-Return^Σ, C-To^Σappendix-rules-025
  1149. C-Force^Σ, C-Lam^Σ, C-App^Σappendix-rules-025
  1150. C-Op, C-Weakenappendix-rules-025
  1151. V-Nextappendix-rules-025
  1152. C-Handleappendix-rules-025
  1153. V-Var, V-Constappendix-rules-028
  1154. V-Lam, C-Returnappendix-rules-028
  1155. C-App, C-To, C-Opappendix-rules-028
  1156. C-Letappendix-rules-028
  1157. C-RowConvappendix-rules-028
  1158. C-Handleappendix-rules-028
  1159. Ex-Without, Ex-Forbidappendix-rules-028
  1160. Ex-Machineappendix-rules-028
  1161. X-Var, X-Constappendix-rules-029
  1162. X-BVar, X-Blockappendix-rules-029
  1163. X-Expr, X-Val, X-Defappendix-rules-029
  1164. X-Callappendix-rules-029
  1165. X-Handleappendix-rules-029
  1166. X-Cap, X-Delimappendix-rules-029
  1167. E-Expr, E-Valappendix-rules-029
  1168. E-Def, E-Callappendix-rules-029
  1169. E-Effect, E-Doappendix-rules-029
  1170. E-Tryappendix-rules-029
  1171. WF-Emp, WF-EVar, WF-Label, WF-HLabelappendix-rules-029
  1172. WF-ESeq, WF-Unit, WF-Int, WF-Funappendix-rules-029
  1173. WF-EAll, WF-HAllappendix-rules-029
  1174. T-Unit, T-Int, T-Varappendix-rules-029
  1175. T-Lam, T-Appappendix-rules-029
  1176. T-Letappendix-rules-029
  1177. S-Unit, S-Int, S-Fun, S-AllEappendix-rules-029
  1178. S-AllH, S-Transappendix-rules-029
  1179. Eff-Sub, T-Subappendix-rules-029
  1180. T-EAbsappendix-rules-029
  1181. T-EApp, T-HAbsappendix-rules-029
  1182. T-HApp, T-HVarappendix-rules-029
  1183. T-Up, T-HDefappendix-rules-029
  1184. T-Downappendix-rules-029
  1185. Loc-Boxappendix-rules-029
  1186. Refl-Up, Refl-Downappendix-rules-029
  1187. E-Empty, E-Var, E-Consappendix-rules-030
  1188. E-EqEmpty, E-EqVar, E-EqCons, E-Includeappendix-rules-030
  1189. K-Sub, K-Var, K-Unitappendix-rules-030
  1190. K-AbsBox, K-ExtBox, K-Arrowappendix-rules-030
  1191. K-Forall, K-AbsMod, K-ExtMod, K-OpSigappendix-rules-030
  1192. Eq-AbsMod, Eq-ExtMod, Eq-Var, Eq-Unitappendix-rules-030
  1193. Eq-Box, Eq-Arrow, Eq-Forallappendix-rules-030
  1194. WF-Empty, WF-Var, WF-Lockappendix-rules-030
  1195. WF-TVar, WF-Labelappendix-rules-030
  1196. M-Unit, M-Abs, M-Appappendix-rules-030
  1197. M-TAbs, M-TAppappendix-rules-030
  1198. M-Aux-Abs, M-Aux-Mod, M-Varappendix-rules-030
  1199. M-Mod, M-LetModappendix-rules-030
  1200. M-Do, M-Localappendix-rules-030
  1201. M-Handleappendix-rules-030
  1202. F-Unit, F-Var, F-TAbsappendix-rules-030
  1203. F-Abs, F-App, F-Returnappendix-rules-030
  1204. F-TApp, F-Let, F-Doappendix-rules-030
  1205. F-Handlerappendix-rules-030
  1206. SC-Unit, SC-Var, SC-Boxappendix-rules-030
  1207. SC-Tracked, SC-Transparent, SC-Unboxappendix-rules-030
  1208. SC-Block, SC-BSubappendix-rules-030
  1209. SC-Return, SC-Callappendix-rules-030
  1210. SC-Let, SC-Defappendix-rules-030
  1211. SC-Sub, SC-Handleappendix-rules-030
  1212. T-Letcc, T-Throwappendix-rules-032
  1213. K-Empty, K-Push, T-Contappendix-rules-032
  1214. S-Eval, S-Retappendix-rules-032
  1215. K-Var, K-Arr, K-Allappendix-rules-032
  1216. K-Nil, K-Consappendix-rules-032
  1217. P-Var, P-Lam, P-Appappendix-rules-032
  1218. P-Gen, P-Instappendix-rules-032
  1219. P-Sub, P-Liftappendix-rules-032
  1220. Sub-Refl, Sub-Arr, Sub-Allappendix-rules-032
  1221. Sub-Nil, Sub-Consappendix-rules-032
  1222. K-DH, Free-DH, DH-Doappendix-rules-032
  1223. DH-Handleappendix-rules-032
  1224. K-S0, Free-S0, S0-Shiftappendix-rules-032
  1225. S0-Resetappendix-rules-032
  1226. K-SH, SH-Doappendix-rules-032
  1227. SH-Handleappendix-rules-032
  1228. K-C0, C0-Controlappendix-rules-032
  1229. C0-Resetappendix-rules-032
  1230. Dep-Bot-F, Dep-Eq-F, Dep-Ex-Fappendix-rules-032
  1231. Dep-Nat, Dep-Var-N, Dep-Var-Pappendix-rules-032
  1232. Dep-Pair, Dep-Wit, Dep-Prfappendix-rules-032
  1233. Dep-Refl, Dep-Substappendix-rules-032
  1234. Dep-Convappendix-rules-032
  1235. Dep-Callcc-P, Dep-Throw-Pappendix-rules-032
  1236. Dep-Callcc-N, Dep-Throw-Nappendix-rules-032
  1237. ML-Var, ML-Const, ML-Abs, ML-Appappendix-rules-032
  1238. ML-Letappendix-rules-032
  1239. val0, val1, fn, argappendix-rules-032
  1240. beta, wrong, bindappendix-rules-032
  1241. sub, seize, jumpappendix-rules-032
  1242. T-UVar, T-LVar, T-OneI, T-OneEappendix-rules-033
  1243. T-LolliI, T-LolliE, T-TensorI, T-TensorEappendix-rules-033
  1244. T-PlusI1, T-PlusI2, T-Caseappendix-rules-033
  1245. T-BangI, T-BangEappendix-rules-033
  1246. E-LinBeta, E-Tensor, E-Oneappendix-rules-033
  1247. E-InL, E-InR, E-Bangappendix-rules-033
  1248. T-Open, T-Read, T-Close, T-Bytesappendix-rules-033
  1249. E-Open, E-Read, E-Closeappendix-rules-033
  1250. W-Aff, C-Relappendix-rules-033
  1251. R-Appappendix-rules-033
  1252. R-Weakappendix-rules-033
  1253. Ctx-Emp, Ctx-Ext, Varappendix-rules-034
  1254. Presup-Ctx, Presup-Ext, Presup-Ty, Presup-Eq-Ty, Presup-Eq-Tmappendix-rules-034
  1255. Ty-Refl, Ty-Sym, Ty-Transappendix-rules-034
  1256. Tm-Refl, Tm-Sym, Tm-Transappendix-rules-034
  1257. Conv, Conv-Eq, Assumappendix-rules-034
  1258. Wk, Substappendix-rules-034
  1259. Ctx-Convappendix-rules-034
  1260. Rename, Exchappendix-rules-034
  1261. Subst-Eq-Ty, Subst-Eq-Tmappendix-rules-034
  1262. Cong-Ty, Cong-Tmappendix-rules-034
  1263. Q-form, Q-form-eqappendix-rules-034
  1264. Π-form, Π-introappendix-rules-035
  1265. Π-elim, Π-β, Π-ηappendix-rules-035
  1266. Π-form-eq, λ-eqappendix-rules-035
  1267. app-eqappendix-rules-035
  1268. Π-evappendix-rules-035
  1269. Σ-form, Σ-introappendix-rules-035
  1270. Σ-elim_1, Σ-elim_2appendix-rules-035
  1271. Σ-β_1, Σ-β_2, Σ-ηappendix-rules-035
  1272. pair-eq, 1-eqappendix-rules-035
  1273. 2-eqappendix-rules-035
  1274. -form, -intro, -ηappendix-rules-035
  1275. -form, -elimappendix-rules-035
  1276. -form, -intro_1, -intro_2appendix-rules-035
  1277. -elim, -comp_1, -comp_2appendix-rules-035
  1278. +-form, +-intro_1, +-intro_2appendix-rules-035
  1279. +-elimappendix-rules-035
  1280. +-comp_1, +-comp_2appendix-rules-035
  1281. -form, -intro_1, -intro_2appendix-rules-035
  1282. -elimappendix-rules-035
  1283. -comp_1, -comp_2appendix-rules-035
  1284. W-form, W-introappendix-rules-035
  1285. W-elimappendix-rules-035
  1286. W-compappendix-rules-035
  1287. Eq-reflectappendix-rules-035
  1288. U-Form, U-Hier, U-El, U-El-Eqappendix-rules-035
  1289. U-Pi, U-Sig, U-Wappendix-rules-035
  1290. U-Sum, U-Void, U-Unit, U-Bool, U-Natappendix-rules-035
  1291. U-Cumulappendix-rules-035
  1292. Lift-U, Lift-El, Lift-Congappendix-rules-035
  1293. Lift-Piappendix-rules-035
  1294. Lift-Sig, Lift-Wappendix-rules-035
  1295. Lift-Sumappendix-rules-035
  1296. Lift-Void, Lift-Unit, Lift-Bool, Lift-Natappendix-rules-035
  1297. Lift-Hierappendix-rules-035
  1298. TU-Form, TU-El, TU-El-Eqappendix-rules-035
  1299. TU-Hier, TU-Hier-Elappendix-rules-035
  1300. TU-Pi, TU-Sig, TU-Wappendix-rules-035
  1301. TU-Pi-El, TU-Sig-El, TU-W-Elappendix-rules-035
  1302. TU-Sum, TU-Sum-Elappendix-rules-035
  1303. TU-Void, TU-Unit, TU-Bool, TU-Natappendix-rules-035
  1304. TU-Void-El, TU-Unit-El, TU-Bool-El, TU-Nat-Elappendix-rules-035
  1305. TU-Congappendix-rules-035
  1306. Id-form, Id-form-, Id-introappendix-rules-035
  1307. Lift-Idappendix-rules-035
  1308. Id-elimappendix-rules-035
  1309. Id-compappendix-rules-035
  1310. Id-form-eqappendix-rules-035
  1311. Id-elim-eqappendix-rules-035
  1312. Id-elim', Id-comp'appendix-rules-035
  1313. Eq-F, Eq-Iappendix-rules-036
  1314. Eq-Form-Uappendix-rules-036
  1315. Eq-Reflect, Eq-Uniqappendix-rules-036
  1316. Eq-F-eq, Eq-I-eqappendix-rules-036
  1317. Tr-F, Tr-I, Tr-Uniqappendix-rules-036
  1318. Tr-F-eq, Tr-I-eqappendix-rules-036
  1319. Tr-Eappendix-rules-036
  1320. Tr-E-eqappendix-rules-036
  1321. UAappendix-rules-037
  1322. 1-form, 1-base, 1-loopappendix-rules-037
  1323. 0–form, 0–point, 0–path_2appendix-rules-038
  1324. Sort-F, Irrappendix-rules-039
  1325. Obs-F, Obs-Iappendix-rules-039
  1326. Ctx-Dim, Ctx-Restrappendix-rules-040
  1327. Path-form, Path-introappendix-rules-040
  1328. Compappendix-rules-040
  1329. Coe, HComappendix-rules-041
  1330. cof-eq, cof-disj, cof-forall, cof-reflect, cof-absurdappendix-rules-042
  1331. coe, coe-id, hcom, hcom-cap, hcom-tubeappendix-rules-042
  1332. Id, W, Cappendix-rules-043
  1333. Top-R, Top-L, I-R, I-Lappendix-rules-043
  1334. And-R, And-L, Or-R_1, Or-R_2appendix-rules-043
  1335. Or-L, Imp-R, Imp-Lappendix-rules-043
  1336. Star-R, Star-L, Wand-R, Wand-Lappendix-rules-043
  1337. Id, Cutappendix-rules-043
  1338. MCutappendix-rules-043
  1339. E-Skip, E-Assign, E-Loadappendix-rules-044
  1340. E-Store, E-Alloc, E-Freeappendix-rules-044
  1341. E-Seq, E-IfT, E-IfFappendix-rules-044
  1342. H-Skip, H-Assign, H-Seq, H-Conseqappendix-rules-044
  1343. H-Existsappendix-rules-044
  1344. H-Load, H-Store, H-Alloc, H-Freeappendix-rules-044
  1345. H-If, H-Frameappendix-rules-044
  1346. Move, Drop, Share-begin, Share-nest, Share-end, Share-return, Ex-begin, Ex-reborrow, Ex-pop, Ex-returnappendix-rules-046
  1347. Read, Write, Seqappendix-rules-046
  1348. Region, Borrowappendix-rules-046
  1349. T-Path-Name, T-LetPropRef, T-VarPropRefappendix-rules-047
  1350. T-LetElemRef, T-VarElemRefappendix-rules-047
  1351. PSS-Name, PSS-Structappendix-rules-047
  1352. PSS-Prop, PSS-Elemappendix-rules-047
  1353. T-Inout, T-Assignappendix-rules-047
  1354. Src-Field, Src-Indexappendix-rules-047
  1355. T-Callappendix-rules-047
  1356. ESS-Callappendix-rules-047
  1357. ESS-Assignappendix-rules-047
  1358. RI-Const, RI-Varappendix-rules-048
  1359. RI-Letappendix-rules-048
  1360. Cap-LetDec, Cap-Haltappendix-rules-048
  1361. Cap-New, Cap-Allocappendix-rules-048
  1362. Cap-Project, Cap-Freeappendix-rules-048
  1363. R-Project, R-Letregionappendix-rules-048
  1364. Cyc-Region-Subappendix-rules-048
  1365. L3-New, L3-Freeappendix-rules-048
  1366. L3-Swapappendix-rules-048
  1367. SC-Star, SC-Set-L, SC-Set-R, SC-Varappendix-rules-049
  1368. Capt, Funappendix-rules-049
  1369. Var-X, TAbs-Cappendix-rules-049
  1370. TApp-C, Sub-Cappendix-rules-049
  1371. TS-Return, TS-Open, TS-Closeappendix-rules-049
  1372. TS-Readappendix-rules-049
  1373. TSO-Open, TSO-Closeappendix-rules-049
  1374. TSO-Read-More, TSO-Read-Eofappendix-rules-049
  1375. TSO-Callappendix-rules-049
  1376. F-Const, F-Var, F-Abs, F-Appappendix-rules-049
  1377. S-Abs, S-Appappendix-rules-049
  1378. L-Var, L-Abs, L-App, L-Weak, L-Der, L-Prom, L-Let, L-Approxappendix-rules-050
  1379. G-Var, G-Weak, G-Approx, G-Abs, G-Appappendix-rules-050
  1380. EC-Ax, EC-Sub, EC-Abs, EC-App, EC-Unit, EC-LetT, EC-Der, EC-Pr, EC-LetD, EC-Dist, EC-Opappendix-rules-050
  1381. RaTT-Var, RaTT-Abs, RaTT-App, RaTT-Delay, RaTT-Adv, RaTT-Box, RaTT-Unbox, RaTT-Progress, RaTT-Promote, RaTT-Fixappendix-rules-050
  1382. TR-Let, TR-Delay, TR-Box, TR-Unboxappendix-rules-050
  1383. Id, Cut, Exch, μltimapR, μltimapL, ⊗R, ⊗L, 1R, 1L, &R, &L_1, &L_2appendix-rules-050
  1384. Soft-Promotion, Multiplexingappendix-rules-050
  1385. Id, Prod-R, Prod-Lappendix-rules-052
  1386. Bslash-R, Bslash-Lappendix-rules-052
  1387. Slash-R, Slash-Lappendix-rules-052
  1388. U-Init, U-BotL, U-TopR, U-OrR1appendix-rules-053
  1389. U-OrR2, U-OrL, U-AndRappendix-rules-053
  1390. U-AndL1, U-AndL2, U-ImpR, U-ImpLappendix-rules-053
  1391. UQ-Nil, UQ-Consappendix-rules-053
  1392. F-DownR, F-OrR1, F-OrR2appendix-rules-053
  1393. F-OnePosR, F-TensorR, F-IdPosappendix-rules-053
  1394. F-DownL, F-ZeroL, F-OrLappendix-rules-053
  1395. F-OnePosL, F-TensorL, F-SuspendPosappendix-rules-053
  1396. F-UpR, F-ImpR, F-OneNegRappendix-rules-053
  1397. F-WithR, F-SuspendNegappendix-rules-053
  1398. F-ReleaseR, F-UpL, F-IdNeg, F-FocusL, F-WithL1, F-ImpL, F-WithL2appendix-rules-053
  1399. SubstPos, SubstNegappendix-rules-053
  1400. Ax, Par, Tensor, Cutappendix-rules-054
  1401. C-Hyp, C-Nat-Suc, C-Π-I, C-Π-E, C-Σ-I, C-Σ-E, C-Eq-I, C-Set-I, C-Set-E_1, C-Set-E_2appendix-rules-057
  1402. Pre-Pi, Pre-Var, Pre-Lam, Pre-Appappendix-rules-057
  1403. Ty-Pi, Ty-Sg, Ty-Id, Ty-1, Ty-, Ty-, Ty-Vec, Ty-Univ, Ty-Elappendix-rules-057
  1404. Syn-Var, Syn-App, Syn-Fst, Syn-Snd, Syn-★, Syn-Zero, Syn-Suc, Syn-True, Syn-False, Syn-Annappendix-rules-057
  1405. Syn-BoolInd, Syn-NatInd, Syn-Jappendix-rules-057
  1406. Syn-VNilappendix-rules-057
  1407. Syn-VConsappendix-rules-057
  1408. Syn-VecIndappendix-rules-057
  1409. Chk-Lam, Chk-Pair, Chk-Refl, Chk-Convappendix-rules-057
  1410. Chk-Code-1, Chk-Code-, Chk-Code-, Chk-Code-Univappendix-rules-057
  1411. Chk-Code-Pi, Chk-Code-Sg, Chk-Code-Id, Chk-Code-Lift, Chk-Code-Vecappendix-rules-057
  1412. Syn-Var-Plain, Syn-Var-Def, Decls-Nil, Decls-Consappendix-rules-057
  1413. ne-var, ne-app, ne-fst, ne-snd, ne-ind-bool, ne-ind-nat, ne-J, ne-vindappendix-rules-057
  1414. nf-lam, nf-pair, nf-star, nf-true, nf-false, nf-zero, nf-suc, nf-refl, nf-vnil, nf-vcons, nf-neappendix-rules-057
  1415. nf-cd-K, nf-cd-univ, nf-cd-pi, nf-cd-sg, nf-cd-id, nf-cd-vec, nf-cd-liftappendix-rules-057
  1416. nf-ty-univ, nf-ty-pi, nf-ty-sg, nf-ty-K, nf-ty-id, nf-ty-vec, nf-ty-neappendix-rules-057
  1417. E-Syn-Var, E-Syn-Atom, E-Chk-Hole, E-Chk-Syn, E-Chk-Lamappendix-rules-057
  1418. E-Chk-Univappendix-rules-057
  1419. E-Syn-Hole, E-Syn-Ann, E-Ty-Holeappendix-rules-057
  1420. E-Ty-Elappendix-rules-057
  1421. E-Ty-Univappendix-rules-057
  1422. E-Ty-Baseappendix-rules-057
  1423. E-Ty-Idappendix-rules-057
  1424. E-Ty-Vecappendix-rules-057
  1425. E-Ty-Piappendix-rules-057
  1426. E-Ty-Sigmaappendix-rules-057
  1427. E-Chk-Pair, E-Syn-Fst, E-Syn-Sndappendix-rules-057
  1428. E-Syn-Appappendix-rules-057
  1429. E-Spine-Doneappendix-rules-057
  1430. E-Spine-Insertappendix-rules-057
  1431. E-Spine-Consumeappendix-rules-057
  1432. E-Syn-Headappendix-rules-057
  1433. E-Head-Doneappendix-rules-057
  1434. E-Head-Inferappendix-rules-057
  1435. E-Head-Writeappendix-rules-057
  1436. P-Var, P-Atom, P-Hole, P-Ann, P-Lam, P-Pairappendix-rules-057
  1437. P-Ty-El, P-Ty-Univ, P-Ty-Baseappendix-rules-057
  1438. P-Ty-Id, P-Ty-Vecappendix-rules-057
  1439. P-Ty-Pi, P-Ty-Sigmaappendix-rules-057
  1440. P-App, P-Spine-Done, P-Spine-Insert, P-Spine-Consumeappendix-rules-057
  1441. P-Headappendix-rules-057
  1442. Share, Subappendix-rules-058
  1443. Ax, Var, Weakappendix-rules-059
  1444. Prod, Lamappendix-rules-059
  1445. App, Convappendix-rules-059
  1446. Zero, Succappendix-rules-060
  1447. LN-Lamappendix-rules-060
  1448. Nom-Var, Nom-App, Nom-Lamappendix-rules-060
  1449. E-Pair, E-Consappendix-rules-061
  1450. E-Let, E-FunAppappendix-rules-061
  1451. T-Cons, T-Letappendix-rules-061
  1452. T-Share, T-Weakappendix-rules-061
  1453. T-FunApp, T-Nilappendix-rules-061
  1454. T-Supertype, T-Subtype, T-Relaxappendix-rules-061
  1455. 1R, 1Lappendix-rules-061
  1456. μltimapR, μltimapLappendix-rules-061
  1457. Cutappendix-rules-061
  1458. ⊕R_1, ⊕R_2, ⊕Lappendix-rules-061
  1459. _1, _2appendix-rules-061
  1460. !R, !L, Copy, Cut!appendix-rules-061
  1461. Eq-Unfold-L, Eq-Unfold-R, T-Rec-Convappendix-rules-061
  1462. I-Step, O-Base, O-Stepappendix-rules-061
  1463. T-Send, T-Queueappendix-rules-061
  1464. Name-Type, New-Type, Nameappendix-rules-062
  1465. Sub-Nameappendix-rules-062
  1466. Name-Etaappendix-rules-062
  1467. Alg-Name, Alg-Concappendix-rules-062
  1468. Alg-New-Extappendix-rules-062
  1469. REFL, TRANS, COMBappendix-rules-062
  1470. ABS, BETA, ASSUME, EQ-MPappendix-rules-062
  1471. DEDUCT-ANTISYM, INST, INST-TYPEappendix-rules-062
  1472. Ty-Abs, Ty-Appappendix-rules-064
  1473. CEK-App, CEK-Arg, CEK-Betaappendix-rules-064
  1474. S-Input, S-Assignappendix-rules-065
  1475. S-If-T, S-If-Fappendix-rules-065
  1476. IF-Assign, IF-Seqappendix-rules-065
  1477. IF-If, IF-Whileappendix-rules-065
  1478. Acc-form, Acc-introappendix-rules-067
  1479. Acc-elimappendix-rules-067
  1480. Acc-βappendix-rules-067
  1481. Lt-zero, Lt-sucappendix-rules-067
  1482. Mendler-form, Mendler-introappendix-rules-067
  1483. Mendler-elimappendix-rules-067
  1484. Mendler-βappendix-rules-067
  1485. Stream-form, Head, Tailappendix-rules-067
  1486. Stream-corecappendix-rules-067
  1487. Sized-Stream-form, Sized-head, Sized-tailappendix-rules-067
  1488. Sized-corecappendix-rules-067
  1489. ITree-Ret, ITree-Tau, ITree-Visappendix-rules-068
  1490. Eutt-Ret, Eutt-Visappendix-rules-068
  1491. Eutt-Tau, Eutt-TauL, Eutt-TauRappendix-rules-068
  1492. CL-Seq-nilappendix-rules-068
  1493. CL-Seq-call, CL-Seq-retappendix-rules-068
  1494. CL-Overlay-call, CL-Overlay-retappendix-rules-068
  1495. CL-Underlay-call, CL-Underlay-retappendix-rules-068
  1496. LHL-Commit-callappendix-rules-068
  1497. LHL-Commit-retappendix-rules-068
  1498. LHL-Returnappendix-rules-068
  1499. LHL-Tauappendix-rules-068
  1500. LHL-Visappendix-rules-068
  1501. LTT–F, LTT–F, LTT–F, LTT–Fappendix-rules-069
  1502. LTT-Hyp, LTT–I, LTT–E, LTT–I, LTT–E, LTT-Classicalappendix-rules-069
  1503. LTT-Set-F, LTT-Set-I, LTT-Set-E, LTT-Set-β, LTT-Set-ηappendix-rules-069
  1504. LTT-Nat-Ind_0appendix-rules-069
  1505. DI-F, DI-I, DI-E_1, DI-E_2appendix-rules-069
  1506. S–F, S–I, S–Eappendix-rules-069
  1507. S-Self-F, S-Self-Gen, S-Self-Instappendix-rules-069
  1508. VDF-F, VDF-I, VDF-Eappendix-rules-069
  1509. VDF-β, VDF-Extappendix-rules-069
  1510. CDLE-Π-F, CDLE–F, CDLE-Isect-F, CDLE-Eq-Fappendix-rules-069
  1511. CDLE-Π-I, CDLE-Π-E, CDLE-Π-β, CDLE–I, CDLE–Eappendix-rules-069
  1512. CDLE-Isect-I, CDLE-Isect-E_1, CDLE-Isect-E_2appendix-rules-069
  1513. CDLE-Eq-I, CDLE-Eq-E, CDLE-φ, CDLE-δ, CDLE-Ascribeappendix-rules-069
  1514. Mod-Var, Mod-Const, Mod-Typeappendix-rules-070
  1515. Mod-Pi, Mod-Lam, Mod-Appappendix-rules-070
  1516. Mod-Conv, Mod-Rewrite, Mod-Betaappendix-rules-070
  1517. LD-μltimap-F, LD-⊗-F, LD-→-F, LD-!-Fappendix-rules-070
  1518. LD-Var, LD-Lam, LD-Appappendix-rules-070
  1519. LD-Pair, LD-Letappendix-rules-070
  1520. LD-Lift, LD-Forceappendix-rules-070
  1521. LD-Param-Lam, LD-Param-App, LD-Param-Forceappendix-rules-070
  1522. LD-Eval-App, LD-Eval-Let, LD-ConvEvalappendix-rules-070
  1523. QTT-Varappendix-rules-070
  1524. QTT-Π-F, QTT-Lam, QTT-Appappendix-rules-070
  1525. QTT-⊗-F, QTT-Pair, QTT-Letappendix-rules-070
  1526. G-Type, G-Varappendix-rules-070
  1527. G-Π-F, G-Lamappendix-rules-070
  1528. G-Appappendix-rules-070
  1529. G-⊗-Fappendix-rules-070
  1530. G-Pairappendix-rules-070
  1531. G-Letappendix-rules-070
  1532. G-Box-F, G-Box-Iappendix-rules-070
  1533. G-Box-Eappendix-rules-070
  1534. U-Var, U-Lam, U-Appappendix-rules-071
  1535. U-Natrecappendix-rules-071
  1536. 2 inference rulesappendix-rules-071
  1537. 2 inference rulesappendix-rules-071
  1538. 2 inference rulesappendix-rules-071
  1539. Return, Thunk, Forceappendix-rules-071
  1540. Bind^-appendix-rules-071
  1541. Bind^+appendix-rules-071
  1542. WP-Return, WP-Bindappendix-rules-071
  1543. WP-Subappendix-rules-071
  1544. Conv-Return, Conv-Stepappendix-rules-071
  1545. Ctx-εappendix-rules-071
  1546. V-Zeroappendix-rules-071
  1547. V-Sucappendix-rules-071
  1548. Ty-Uappendix-rules-071
  1549. Ty-Πappendix-rules-071
  1550. Ty-Σappendix-rules-071
  1551. Code-Nappendix-rules-071
  1552. Code-Emptyappendix-rules-071
  1553. Code-Πappendix-rules-071
  1554. Code-Σappendix-rules-071
  1555. T-Prodrecappendix-rules-071
  1556. T-Emptyrecappendix-rules-071
  1557. T-Natrecappendix-rules-071
  1558. Eq-Tyappendix-rules-071
  1559. Eq-Ty-Reflappendix-rules-071
  1560. Eq-Ty-Symappendix-rules-071
  1561. Eq-Ty-Transappendix-rules-071
  1562. Eq-Πappendix-rules-071
  1563. Eq-Σappendix-rules-071
  1564. Eq-Reflappendix-rules-071
  1565. Eq-Symappendix-rules-071
  1566. Eq-Transappendix-rules-071
  1567. Eq-Convappendix-rules-071
  1568. Eq-Π-Uappendix-rules-071
  1569. Eq-Σ-Uappendix-rules-071
  1570. Eq-Appappendix-rules-071
  1571. Eq-βappendix-rules-071
  1572. Eq-ηappendix-rules-071
  1573. Eq-Fst-βappendix-rules-071
  1574. Eq-Fstappendix-rules-071
  1575. Eq-Snd-βappendix-rules-071
  1576. Eq-Sndappendix-rules-071
  1577. Eq-Σ_&-ηappendix-rules-071
  1578. Eq-Pairappendix-rules-071
  1579. Eq-Prodrec-βappendix-rules-071
  1580. Eq-Prodrecappendix-rules-071
  1581. Eq-Nat-Zeroappendix-rules-071
  1582. Eq-Nat-Sucappendix-rules-071
  1583. Eq-Sucappendix-rules-071
  1584. Eq-Natrecappendix-rules-071
  1585. Eq-Emptyrecappendix-rules-071
  1586. U-Universeappendix-rules-071
  1587. U-Zeroappendix-rules-071
  1588. U-WeakPairappendix-rules-071
  1589. U-StrongPairappendix-rules-071
  1590. U-Fstappendix-rules-071
  1591. U-Sndappendix-rules-071
  1592. U-Sucappendix-rules-071
  1593. U-Prodrecappendix-rules-071
  1594. U-Emptyrecappendix-rules-071
  1595. U-Subappendix-rules-071
  1596. R-Convappendix-rules-071
  1597. R-βappendix-rules-071
  1598. R-Fstappendix-rules-071
  1599. R-Fst-βappendix-rules-071
  1600. R-Sndappendix-rules-071
  1601. R-Snd-βappendix-rules-071
  1602. R-Prodrecappendix-rules-071
  1603. R-Prodrec-βappendix-rules-071
  1604. R-Natrecappendix-rules-071
  1605. R-Nat-Zeroappendix-rules-071
  1606. R-Nat-Sucappendix-rules-071
  1607. R-Emptyrecappendix-rules-071
  1608. E-βappendix-rules-071
  1609. E-Appappendix-rules-071
  1610. E-Fstappendix-rules-071
  1611. E-Fst-βappendix-rules-071
  1612. E-Snd-βappendix-rules-071
  1613. E-Sndappendix-rules-071
  1614. E-Prodrecappendix-rules-071
  1615. E-Prodrec-βappendix-rules-071
  1616. E-Nat-Zeroappendix-rules-071
  1617. E-Natrecappendix-rules-071
  1618. E-Nat-Sucappendix-rules-071
  1619. 1 inference rulesappendix-rules-071
  1620. 1 inference rulesappendix-rules-071
  1621. 1 inference rulesappendix-rules-071
  1622. 1 inference rulesappendix-rules-071
  1623. !Rappendix-rules-071
  1624. !Lappendix-rules-071
  1625. Cut^!appendix-rules-071
  1626. Dep- B-Eappendix-rules-071
  1627. Divergeappendix-rules-071
  1628. Recappendix-rules-071
  1629. Errorappendix-rules-071
  1630. Printappendix-rules-071
  1631. Chooseappendix-rules-071
  1632. Nilappendix-rules-071
  1633. Argappendix-rules-071
  1634. Incl-Writeappendix-rules-071
  1635. Incl-Readappendix-rules-071
  1636. Incl-Printappendix-rules-071
  1637. Incl-Chooseappendix-rules-071
  1638. WP-Runappendix-rules-071
  1639. R-Runappendix-rules-071
  1640. Π-Fappendix-rules-071
  1641. Π-Iappendix-rules-071
  1642. Π-Eappendix-rules-071
  1643. R-Base-Fappendix-rules-071
  1644. R-Π-Fappendix-rules-071
  1645. A-Intappendix-rules-071
  1646. A-Lamappendix-rules-071
  1647. A-Appappendix-rules-071
  1648. A-Checkappendix-rules-071
  1649. DOT-Topappendix-rules-071
  1650. DOT-Botappendix-rules-071
  1651. DOT-Reflappendix-rules-071
  1652. DOT-Transappendix-rules-071
  1653. DOT-And_1-appendix-rules-071
  1654. DOT-And_2-appendix-rules-071
  1655. DOT–Andappendix-rules-071
  1656. DOT-Fld–Fldappendix-rules-071
  1657. DOT-Obj-Iappendix-rules-071
  1658. DOT-Def-Valappendix-rules-071
  1659. DOT-Def-Andappendix-rules-071
  1660. Def-Pathappendix-rules-071
  1661. R-Fldappendix-rules-071
  1662. R-Mem-Lappendix-rules-071
  1663. R-Mem-Uappendix-rules-071
  1664. R-And-Lappendix-rules-071
  1665. R-And-Rappendix-rules-071
  1666. R-All-Domappendix-rules-071
  1667. R-All-Codappendix-rules-071
  1668. R-Recappendix-rules-071
  1669. Lookup-Varappendix-rules-071
  1670. Lookup-Valappendix-rules-071
  1671. Lookup-Pathappendix-rules-071
  1672. -Rappendix-rules-071
  1673. Witappendix-rules-071
  1674. Prfappendix-rules-071
  1675. tpappendix-rules-071
  1676. μ-dappendix-rules-071
  1677. -Lappendix-rules-071
  1678. Π-Subappendix-rules-072
  1679. R-Base-Sub, R-Π-Subappendix-rules-072
  1680. R-Var, R-Int, R-Arrappendix-rules-072
  1681. R-Lam, R-App, R-Subappendix-rules-072
  1682. DOT-Sel-L, DOT-Sel-U, DOT-Type-Mem-Subappendix-rules-072
  1683. DOT-Rec-I, DOT-Rec-E, DOT-Fld-Eappendix-rules-072
  1684. DOT-T-Sel-L, DOT-T-Sel-Uappendix-rules-072
  1685. DOT-Def-Typeappendix-rules-072
  1686. P-Var, P-Fldappendix-rules-072
  1687. Sngl-Trans, Sngl-Eappendix-rules-072
  1688. RP-Here, RP-Fldappendix-rules-072
  1689. R-Sel, R-Snglappendix-rules-072
  1690. Repl-pq, Repl-qpappendix-rules-072
  1691. Def-Newappendix-rules-072
  1692. Cut, μ-R, μ-Lappendix-rules-072
  1693. Π-R, Π-Lappendix-rules-072
  1694. μtp, Cut-dappendix-rules-072
  1695. Ctx-εappendix-rules-072
  1696. V-Zeroappendix-rules-072
  1697. V-Sucappendix-rules-072
  1698. Ty-Uappendix-rules-072
  1699. Ty-Πappendix-rules-072
  1700. Ty-Σappendix-rules-072
  1701. Code-Nappendix-rules-072
  1702. Code-Emptyappendix-rules-072
  1703. Code-Πappendix-rules-072
  1704. Code-Σappendix-rules-072
  1705. T-Prodrecappendix-rules-072
  1706. T-Emptyrecappendix-rules-072
  1707. T-Natrecappendix-rules-072
  1708. Eq-Tyappendix-rules-072
  1709. Eq-Ty-Reflappendix-rules-072
  1710. Eq-Ty-Symappendix-rules-072
  1711. Eq-Ty-Transappendix-rules-072
  1712. Eq-Πappendix-rules-072
  1713. Eq-Σappendix-rules-072
  1714. Eq-Reflappendix-rules-072
  1715. Eq-Symappendix-rules-072
  1716. Eq-Transappendix-rules-072
  1717. Eq-Convappendix-rules-072
  1718. Eq-Π-Uappendix-rules-072
  1719. Eq-Σ-Uappendix-rules-072
  1720. Eq-Appappendix-rules-072
  1721. Eq-βappendix-rules-072
  1722. Eq-ηappendix-rules-072
  1723. Eq-Fst-βappendix-rules-072
  1724. Eq-Fstappendix-rules-072
  1725. Eq-Snd-βappendix-rules-072
  1726. Eq-Sndappendix-rules-072
  1727. Eq-Σ_&-ηappendix-rules-072
  1728. Eq-Pairappendix-rules-072
  1729. Eq-Prodrec-βappendix-rules-072
  1730. Eq-Prodrecappendix-rules-072
  1731. Eq-Nat-Zeroappendix-rules-072
  1732. Eq-Nat-Sucappendix-rules-072
  1733. Eq-Sucappendix-rules-072
  1734. Eq-Natrecappendix-rules-072
  1735. Eq-Emptyrecappendix-rules-072
  1736. U-Universeappendix-rules-072
  1737. U-Zeroappendix-rules-072
  1738. U-WeakPairappendix-rules-072
  1739. U-StrongPairappendix-rules-072
  1740. U-Fstappendix-rules-072
  1741. U-Sndappendix-rules-072
  1742. U-Sucappendix-rules-072
  1743. U-Prodrecappendix-rules-072
  1744. U-Emptyrecappendix-rules-072
  1745. U-Subappendix-rules-072
  1746. R-Convappendix-rules-072
  1747. R-βappendix-rules-072
  1748. R-Fstappendix-rules-072
  1749. R-Fst-βappendix-rules-072
  1750. R-Sndappendix-rules-072
  1751. R-Snd-βappendix-rules-072
  1752. R-Prodrecappendix-rules-072
  1753. R-Prodrec-βappendix-rules-072
  1754. R-Natrecappendix-rules-072
  1755. R-Nat-Zeroappendix-rules-072
  1756. R-Nat-Sucappendix-rules-072
  1757. R-Emptyrecappendix-rules-072
  1758. E-βappendix-rules-072
  1759. E-Appappendix-rules-072
  1760. E-Fstappendix-rules-072
  1761. E-Fst-βappendix-rules-072
  1762. E-Snd-βappendix-rules-072
  1763. E-Sndappendix-rules-072
  1764. E-Prodrecappendix-rules-072
  1765. E-Prodrec-βappendix-rules-072
  1766. E-Nat-Zeroappendix-rules-072
  1767. E-Natrecappendix-rules-072
  1768. E-Nat-Sucappendix-rules-072
  1769. 1 inference rulesappendix-rules-072
  1770. 1 inference rulesappendix-rules-072
  1771. 1 inference rulesappendix-rules-072
  1772. 1 inference rulesappendix-rules-072
  1773. !Rappendix-rules-072
  1774. !Lappendix-rules-072
  1775. Cut^!appendix-rules-072
  1776. Dep- B-Eappendix-rules-072
  1777. Divergeappendix-rules-072
  1778. Recappendix-rules-072
  1779. Errorappendix-rules-072
  1780. Printappendix-rules-072
  1781. Chooseappendix-rules-072
  1782. Nilappendix-rules-072
  1783. Argappendix-rules-072
  1784. Incl-Writeappendix-rules-072
  1785. Incl-Readappendix-rules-072
  1786. Incl-Printappendix-rules-072
  1787. Incl-Chooseappendix-rules-072
  1788. WP-Runappendix-rules-072
  1789. R-Runappendix-rules-072
  1790. Π-Fappendix-rules-072
  1791. Π-Iappendix-rules-072
  1792. Π-Eappendix-rules-072
  1793. R-Base-Fappendix-rules-072
  1794. R-Π-Fappendix-rules-072
  1795. A-Intappendix-rules-072
  1796. A-Lamappendix-rules-072
  1797. A-Appappendix-rules-072
  1798. A-Checkappendix-rules-072
  1799. DOT-Topappendix-rules-072
  1800. DOT-Botappendix-rules-072
  1801. DOT-Reflappendix-rules-072
  1802. DOT-Transappendix-rules-072
  1803. DOT-And_1-appendix-rules-072
  1804. DOT-And_2-appendix-rules-072
  1805. DOT–Andappendix-rules-072
  1806. DOT-Fld–Fldappendix-rules-072
  1807. DOT-Obj-Iappendix-rules-072
  1808. DOT-Def-Valappendix-rules-072
  1809. DOT-Def-Andappendix-rules-072
  1810. Def-Pathappendix-rules-072
  1811. R-Fldappendix-rules-072
  1812. R-Mem-Lappendix-rules-072
  1813. R-Mem-Uappendix-rules-072
  1814. R-And-Lappendix-rules-072
  1815. R-And-Rappendix-rules-072
  1816. R-All-Domappendix-rules-072
  1817. R-All-Codappendix-rules-072
  1818. R-Recappendix-rules-072
  1819. Lookup-Varappendix-rules-072
  1820. Lookup-Valappendix-rules-072
  1821. Lookup-Pathappendix-rules-072
  1822. -Rappendix-rules-072
  1823. Witappendix-rules-072
  1824. Prfappendix-rules-072
  1825. tpappendix-rules-072
  1826. μ-dappendix-rules-072
  1827. -Lappendix-rules-072
  1828. Tac-Or-Left, Tac-Or-Right, Tac-Or-Failappendix-rules-073
  1829. Rw-Root, Rw-Atom, Rw-App, Rw-Lamappendix-rules-073
  1830. Src-Var, Src-Lam, Src-Appappendix-rules-073
  1831. Q-Quote, Q-Splice, Q-Varappendix-rules-073
  1832. Level, L-Zero, L-Suc, L-Join, L-Univappendix-rules-073
  1833. Lift-F, Lift-I, Lift-Eappendix-rules-073
  1834. Same-Sortappendix-rules-073
  1835. DT-Type, DT-Pi, DT-AppTyappendix-rules-073
  1836. Coe-Var, Coe-App, Coe-Lam, Coe-Insertappendix-rules-073
  1837. Rel-Erased, Rel-Var, Rel-Lam-Rappendix-rules-074
  1838. Rel-App-R, Rel-App-Eappendix-rules-074
  1839. S0-Const, S0-Var, S0-Opappendix-rules-075
  1840. S0-If-F, S0-If-Tappendix-rules-075
  1841. S0-Callappendix-rules-075
  1842. PE-Num, PE-Static, PE-Dynamicappendix-rules-075
  1843. PE-Op-S, PE-Op-Dappendix-rules-075
  1844. PE-If-Z, PE-If-Nappendix-rules-075
  1845. PE-If-Dappendix-rules-075
  1846. PE-Call-Hit, PE-Fuelappendix-rules-075
  1847. PE-Call-Newappendix-rules-075
  1848. BT-Const, BT-Var, BT-Op-Sappendix-rules-075
  1849. BT-Op-D, BT-If-Sappendix-rules-075
  1850. BT-If-D, BT-Call-S0appendix-rules-075
  1851. BT-Call-S, BT-Call-Dappendix-rules-075
  1852. BT-Liftappendix-rules-075
  1853. Off-Const, Off-Var-S, Off-Var-Dappendix-rules-075
  1854. Off-Op-S, Off-Op-Dappendix-rules-075
  1855. Off-If-S, Off-If-Dappendix-rules-075
  1856. Off-Call-S, Off-Call-Dappendix-rules-075
  1857. Off-Liftappendix-rules-075
  1858. D-Betaappendix-rules-075
  1859. D-Case-Known, D-Case-Openappendix-rules-075
  1860. Emb-Var, Emb-Num, Emb-Dive, Emb-Coupleappendix-rules-075
  1861. T-Var, T-MVar, T-Abs, T-App, T-Box, T-LetBoxappendix-rules-075
  1862. TS-Beta, TS-BoxBetaappendix-rules-075
  1863. TS-Lam, TS-AppL, TS-AppRappendix-rules-075
  1864. TS-LetL, TS-LetRappendix-rules-075
  1865. 2-Varp, 2-Lamp, 2-Apppappendix-rules-075
  1866. 2-Fixp, 2-Pairp, 2-Projpappendix-rules-075
  1867. 2-Unitp, 2-Zerop, 2-Succpappendix-rules-075
  1868. 2-Casepappendix-rules-075
  1869. 2-Down, 2-Upappendix-rules-075
  1870. I-Var, I-Abs, I-Appappendix-rules-075
  1871. I-Box, I-Unbox1appendix-rules-075
  1872. I-Fix, I-Pair, I-Projappendix-rules-075
  1873. I-Unit, I-Zero, I-Succappendix-rules-075
  1874. I-Caseappendix-rules-075
  1875. MC-Quote, MC-Spliceappendix-rules-075
  1876. MC-CodeGenappendix-rules-075
  1877. TW-Pure, TW-Repappendix-rules-075
  1878. TW-Code, TW-Reflect, TW-LetCappendix-rules-075
  1879. TW-Run-Refappendix-rules-075
  1880. MD-Kind-Star, MD-Kind-Pi, MD-TConstappendix-rules-075
  1881. MD-TApp, MD-TCode, MD-TForallappendix-rules-075
  1882. MD-TCSP, MD-TConv, MD-Piappendix-rules-075
  1883. MD-Const, MD-Var, MD-Abs, MD-App, MD-Convappendix-rules-075
  1884. MD-Quote, MD-Escape, MD-SAbs, MD-SApp, MD-CSPappendix-rules-075
  1885. MD-QK-Pi, MD-QK-CSPappendix-rules-075
  1886. MD-QK-Refl, MD-QK-Sym, MD-QK-Transappendix-rules-075
  1887. MD-QT-Pi, MD-QT-Appappendix-rules-075
  1888. MD-QT-Code, MD-QT-Forall, MD-QT-CSPappendix-rules-075
  1889. MD-QT-Refl, MD-QT-Sym, MD-QT-Transappendix-rules-075
  1890. MD-Q-Abs, MD-Q-Appappendix-rules-075
  1891. MD-Q-Quote, MD-Q-Escapeappendix-rules-075
  1892. MD-Q-SAbs, MD-Q-SApp, MD-Q-CSPappendix-rules-075
  1893. MD-Q-Refl, MD-Q-Sym, MD-Q-Transappendix-rules-075
  1894. MD-Q-Beta, MD-Q-Spliceappendix-rules-075
  1895. MD-Q-StageBeta, MD-Q-Percentappendix-rules-075
  1896. 1 inference rulesappendix-solutions-001
  1897. 3 inference rulesappendix-solutions-001
  1898. 3 inference rulesappendix-solutions-001
  1899. Varappendix-solutions-061
  1900. Wkappendix-solutions-061
  1901. Subst-Eq-Tyappendix-solutions-061
  1902. Substappendix-solutions-061
  1903. Substappendix-solutions-061
  1904. Substappendix-solutions-061
  1905. Ctx-Convappendix-solutions-061
  1906. Ctx-Convappendix-solutions-061
  1907. Subst-Eq-Tmappendix-solutions-061
  1908. Exchappendix-solutions-061
  1909. Varappendix-solutions-061
  1910. Wkappendix-solutions-061
  1911. q-introappendix-solutions-061
  1912. q-congappendix-solutions-061
  1913. q-introappendix-solutions-061
  1914. Substappendix-solutions-061
  1915. Substappendix-solutions-061
  1916. →-form, →-intro, →-elimappendix-solutions-062
  1917. →-β, →-ηappendix-solutions-062
  1918. app-eqappendix-solutions-062
  1919. λ-eqappendix-solutions-062
  1920. Convappendix-solutions-062
  1921. Substappendix-solutions-062
  1922. ×-form, ×-introappendix-solutions-062
  1923. ×-elim_1, ×-elim_2appendix-solutions-062
  1924. ×-β_1, ×-β_2, ×-ηappendix-solutions-062
  1925. Convappendix-solutions-062
  1926. Convappendix-solutions-062
  1927. Tm-Reflappendix-solutions-062
  1928. Substappendix-solutions-062
  1929. List-form, List-intro_1, List-intro_2appendix-solutions-063
  1930. List-elimappendix-solutions-063
  1931. List-comp_1appendix-solutions-063
  1932. List-comp_2appendix-solutions-063
  1933. Eq-Jappendix-solutions-080
  1934. Π-Iappendix-solutions-080
  1935. Pre-Sgappendix-solutions-082
  1936. Pre-Pairappendix-solutions-082
  1937. Pre-Fstappendix-solutions-082
  1938. Pre-Sndappendix-solutions-082
  1939. Ty-Sumappendix-solutions-082
  1940. Chk-Code-Sumappendix-solutions-082
  1941. Chk-Inl, Chk-Inrappendix-solutions-082
  1942. Syn-SumIndappendix-solutions-082

Search the book

Type to search the local edition.