1. 1. Intro
2. 2. formality_core: the Formality system
   1. 2.1. Defining your lang
   2. 2.2. Defining terms with the term macro
      1. 2.2.1. Parsing
      2. 2.2.2. Customizing debug
   3. 2.3. Constructors
   4. 2.4. Variables
   5. 2.5. Collections
   6. 2.6. Judgment functions and inference rules
   7. 2.7. FAQ and troubleshooting
3. 3. formality_rust: the Rust model
   1. 3.1. Borrow checking
   2. 3.2. Coherence checking
   3. 3.3. Code generation
4. 4. Coverage report
   1. 4.1. fmt
   2. 4.2. all_even
      1. 4.2.1. all_even / all_even (positive)
   3. 4.3. sum_all
      1. 4.3.1. sum_all / sum (positive)
   4. 4.4. transitive_reachable
      1. 4.4.1. transitive_reachable / base (positive)
      2. 4.4.2. transitive_reachable / transitive (positive)
   5. 4.5. is_zero
   6. 4.6. is_one
   7. 4.7. prove_thing
   8. 4.8. only_one
   9. 4.9. mixed
   10. 4.10. move_place
   11. 4.11. check_adt
       1. 4.11.1. check_adt / check adt (positive)
       2. 4.11.2. check_adt / check adt premise@18 (negative)
       3. 4.11.3. check_adt / check adt premise@21 (negative)
   12. 4.12. borrow_check
       1. 4.12.1. borrow_check / borrow_check (positive)
       2. 4.12.2. borrow_check / borrow_check premise@138 (negative)
   13. 4.13. borrow_check_block
       1. 4.13.1. borrow_check_block / basic block (positive)
       2. 4.13.2. borrow_check_block / basic block premise@169 (negative)
   14. 4.14. borrow_check_statement
       1. 4.14.1. borrow_check_statement / let (positive)
       2. 4.14.2. borrow_check_statement / let premise@189 (negative)
       3. 4.14.3. borrow_check_statement / if (positive)
       4. 4.14.4. borrow_check_statement / if premise@220 (negative)
       5. 4.14.5. borrow_check_statement / if premise@221 (negative)
       6. 4.14.6. borrow_check_statement / expr (positive)
       7. 4.14.7. borrow_check_statement / expr premise@230 (negative)
       8. 4.14.8. borrow_check_statement / loop (positive)
       9. 4.14.9. borrow_check_statement / loop premise@247 (negative)
       10. 4.14.10. borrow_check_statement / break (positive)
       11. 4.14.11. borrow_check_statement / break premise@258 (negative)
       12. 4.14.12. borrow_check_statement / continue (positive)
       13. 4.14.13. borrow_check_statement / continue premise@269 (negative)
       14. 4.14.14. borrow_check_statement / continue premise@271 (negative)
       15. 4.14.15. borrow_check_statement / return (positive)
       16. 4.14.16. borrow_check_statement / return premise@280 (negative)
       17. 4.14.17. borrow_check_statement / return premise@282 (negative)
       18. 4.14.18. borrow_check_statement / block (positive)
       19. 4.14.19. borrow_check_statement / block premise@290 (negative)
       20. 4.14.20. borrow_check_statement / exists (positive)
       21. 4.14.21. borrow_check_statement / exists premise@300 (negative)
       22. 4.14.22. borrow_check_statement / exists (positive)
       23. 4.14.23. borrow_check_statement / exists premise@311 (negative)
       24. 4.14.24. borrow_check_statement / exists premise@315 (negative)
       25. 4.14.25. borrow_check_statement / exists (positive)
       26. 4.14.26. borrow_check_statement / exists premise@327 (negative)
       27. 4.14.27. borrow_check_statement / exists premise@330 (negative)
       28. 4.14.28. borrow_check_statement / print (positive)
   15. 4.15. borrow_check_expr_has_ty
       1. 4.15.1. borrow_check_expr_has_ty / block (positive)
       2. 4.15.2. borrow_check_expr_has_ty / block premise@364 (negative)
       3. 4.15.3. borrow_check_expr_has_ty / block premise@365 (negative)
   16. 4.16. borrow_check_expr
       1. 4.16.1. borrow_check_expr / assign (positive)
       2. 4.16.2. borrow_check_expr / assign premise@394 (negative)
       3. 4.16.3. borrow_check_expr / assign premise@402 (negative)
       4. 4.16.4. borrow_check_expr / assign premise@404 (negative)
       5. 4.16.5. borrow_check_expr / call (positive)
       6. 4.16.6. borrow_check_expr / call premise@420 (negative)
       7. 4.16.7. borrow_check_expr / call premise@440 (negative)
       8. 4.16.8. borrow_check_expr / call premise@445 (negative)
       9. 4.16.9. borrow_check_expr / literal (positive)
       10. 4.16.10. borrow_check_expr / true (positive)
       11. 4.16.11. borrow_check_expr / false (positive)
       12. 4.16.12. borrow_check_expr / ref (positive)
       13. 4.16.13. borrow_check_expr / ref premise@478 (negative)
       14. 4.16.14. borrow_check_expr / ref premise@495 (negative)
       15. 4.16.15. borrow_check_expr / place (positive)
       16. 4.16.16. borrow_check_expr / place premise@502 (negative)
       17. 4.16.17. borrow_check_expr / place premise@504 (negative)
       18. 4.16.18. borrow_check_expr / place premise@506 (negative)
       19. 4.16.19. borrow_check_expr / fn-name (positive)
       20. 4.16.20. borrow_check_expr / fn-name premise@516 (negative)
       21. 4.16.21. borrow_check_expr / fn-name premise@517 (negative)
       22. 4.16.22. borrow_check_expr / turbofish (positive)
       23. 4.16.23. borrow_check_expr / turbofish premise@527 (negative)
       24. 4.16.24. borrow_check_expr / struct (positive)
       25. 4.16.25. borrow_check_expr / struct premise@551 (negative)
   17. 4.17. borrow_check_loop
       1. 4.17.1. borrow_check_loop / loop (positive)
       2. 4.17.2. borrow_check_loop / loop premise@587 (negative)
       3. 4.17.3. borrow_check_loop / loop premise@589 (negative)
       4. 4.17.4. borrow_check_loop / fixed-point (positive)
       5. 4.17.5. borrow_check_loop / fixed-point premise@595 (negative)
       6. 4.17.6. borrow_check_loop / fixed-point premise@596 (negative)
   18. 4.18. borrow_check_place_expr
       1. 4.18.1. borrow_check_place_expr / local (positive)
       2. 4.18.2. borrow_check_place_expr / local premise@614 (negative)
       3. 4.18.3. borrow_check_place_expr / struct field (positive)
       4. 4.18.4. borrow_check_place_expr / struct field premise@624 (negative)
       5. 4.18.5. borrow_check_place_expr / struct field premise@629 (negative)
       6. 4.18.6. borrow_check_place_expr / parens (positive)
       7. 4.18.7. borrow_check_place_expr / deref-ref (positive)
   19. 4.19. drop_places
       1. 4.19.1. drop_places / drop_places (positive)
   20. 4.20. access_permitted
       1. 4.20.1. access_permitted / access_permitted (positive)
       2. 4.20.2. access_permitted / access_permitted premise@809 (negative)
       3. 4.20.3. access_permitted / access_permitted premise@813 (negative)
   21. 4.21. access_permitted_by_loans
       1. 4.21.1. access_permitted_by_loans / access_permitted_by_loans (positive)
   22. 4.22. access_permitted_by_loan
       1. 4.22.1. access_permitted_by_loan / borrow of disjoint places (positive)
       2. 4.22.2. access_permitted_by_loan / borrow of disjoint places premise@855 (negative)
       3. 4.22.3. access_permitted_by_loan / write-indirect (positive)
       4. 4.22.4. access_permitted_by_loan / write-indirect premise@882 (negative)
       5. 4.22.5. access_permitted_by_loan / write-indirect premise@884 (negative)
       6. 4.22.6. access_permitted_by_loan / loan is dead (positive)
       7. 4.22.7. access_permitted_by_loan / loan is dead premise@902 (negative)
   23. 4.23. access_kind_for_place_use
       1. 4.23.1. access_kind_for_place_use / move (positive)
   24. 4.24. prove_ty_is_copy
       1. 4.24.1. prove_ty_is_copy / trait (positive)
       2. 4.24.2. prove_ty_is_copy / trait premise@968 (negative)
   25. 4.25. prove_place_is_movable
       1. 4.25.1. prove_place_is_movable / local (positive)
       2. 4.25.2. prove_place_is_movable / field (positive)
       3. 4.25.3. prove_place_is_movable / field premise@1001 (negative)
       4. 4.25.4. prove_place_is_movable / copy (positive)
       5. 4.25.5. prove_place_is_movable / copy premise@1013 (negative)
   26. 4.26. prove_ty_is_ref
       1. 4.26.1. prove_ty_is_ref / ref (positive)
   27. 4.27. prove_ty_is_rigid
       1. 4.27.1. prove_ty_is_rigid / rigid (positive)
       2. 4.27.2. prove_ty_is_rigid / normalize (positive)
   28. 4.28. prove_assignable
       1. 4.28.1. prove_assignable / subtype (positive)
       2. 4.28.2. prove_assignable / subtype premise@1085 (negative)
   29. 4.29. loan_cannot_outlive_universal_regions
       1. 4.29.1. loan_cannot_outlive_universal_regions / loan_not_required_by_universal_regions (positive)
       2. 4.29.2. loan_cannot_outlive_universal_regions / loan_not_required_by_universal_regions premise@1197 (negative)
   30. 4.30. loan_not_required_by_live_places
       1. 4.30.1. loan_not_required_by_live_places / loan_not_required_by_live_places (positive)
   31. 4.31. loan_not_required_by_live_place
       1. 4.31.1. loan_not_required_by_live_place / loan is not required by type (positive)
       2. 4.31.2. loan_not_required_by_live_place / loan is not required by type premise@1278 (negative)
   32. 4.32. loan_not_required_by_live_place_prefix
       1. 4.32.1. loan_not_required_by_live_place_prefix / no prefix (positive)
       2. 4.32.2. loan_not_required_by_live_place_prefix / prefix (positive)
   33. 4.33. loan_not_required_by_parameter
       1. 4.33.1. loan_not_required_by_parameter / rigid-ty (positive)
       2. 4.33.2. loan_not_required_by_parameter / rigid-ty premise@1346 (negative)
       3. 4.33.3. loan_not_required_by_parameter / alias-ty RFC 1214 (positive)
       4. 4.33.4. loan_not_required_by_parameter / alias-ty RFC 1214 premise@1362 (negative)
       5. 4.33.5. loan_not_required_by_parameter / universal-variable premise@1420 (negative)
       6. 4.33.6. loan_not_required_by_parameter / lifetime (positive)
       7. 4.33.7. loan_not_required_by_parameter / lifetime premise@1436 (negative)
   34. 4.34. loan_cannot_outlive
       1. 4.34.1. loan_cannot_outlive / loan_cannot_outlive (positive)
       2. 4.34.2. loan_cannot_outlive / loan_cannot_outlive premise@1456 (negative)
   35. 4.35. loan_not_required_by_parameters
       1. 4.35.1. loan_not_required_by_parameters / loan_not_required_by_parameters (positive)
   36. 4.36. verify_universal_outlives
       1. 4.36.1. verify_universal_outlives / verify_universal_outlives (positive)
   37. 4.37. only_assumed_outlives
       1. 4.37.1. only_assumed_outlives / existential (positive)
       2. 4.37.2. only_assumed_outlives / universal lifetime (positive)
   38. 4.38. can_outlive
       1. 4.38.1. can_outlive / existential target (positive)
       2. 4.38.2. can_outlive / universal target (positive)
       3. 4.38.3. can_outlive / universal target premise@81 (negative)
   39. 4.39. check_coherence
       1. 4.39.1. check_coherence / check_coherence (positive)
   40. 4.40. orphan_check
       1. 4.40.1. orphan_check / orphan_check (positive)
       2. 4.40.2. orphan_check / orphan_check premise@38 (negative)
   41. 4.41. orphan_check_neg
       1. 4.41.1. orphan_check_neg / orphan_check_neg (positive)
       2. 4.41.2. orphan_check_neg / orphan_check_neg premise@58 (negative)
   42. 4.42. check_free_fn
       1. 4.42.1. check_free_fn / check free fn (positive)
       2. 4.42.2. check_free_fn / check free fn premise@24 (negative)
   43. 4.43. check_fn
       1. 4.43.1. check_fn / check fn (positive)
       2. 4.43.2. check_fn / check fn premise@55 (negative)
   44. 4.44. check_fn_body
       1. 4.44.1. check_fn_body / no fn body (positive)
       2. 4.44.2. check_fn_body / trusted fn body (positive)
       3. 4.44.3. check_fn_body / expr fn body (positive)
       4. 4.44.4. check_fn_body / expr fn body premise@90 (negative)
   45. 4.45. check_trait_impl
       1. 4.45.1. check_trait_impl / check_trait_impl (positive)
       2. 4.45.2. check_trait_impl / check_trait_impl premise@27 (negative)
       3. 4.45.3. check_trait_impl / check_trait_impl premise@28 (negative)
       4. 4.45.4. check_trait_impl / check_trait_impl premise@32 (negative)
       5. 4.45.5. check_trait_impl / check_trait_impl premise@37 (negative)
   46. 4.46. check_neg_trait_impl
       1. 4.46.1. check_neg_trait_impl / check_neg_trait_impl (positive)
       2. 4.46.2. check_neg_trait_impl / check_neg_trait_impl premise@53 (negative)
       3. 4.46.3. check_neg_trait_impl / check_neg_trait_impl (positive)
   47. 4.47. check_safety_matches
       1. 4.47.1. check_safety_matches / safety matches (positive)
       2. 4.47.2. check_safety_matches / safety matches premise@78 (negative)
   48. 4.48. check_trait_impl_item
       1. 4.48.1. check_trait_impl_item / associated ty value (positive)
   49. 4.49. check_fn_in_impl
   50. 4.50. check_associated_ty_value
       1. 4.50.1. check_associated_ty_value / check_associated_ty_value (positive)
   51. 4.51. check_drop_impl_always_applicable
       1. 4.51.1. check_drop_impl_always_applicable / not a Drop impl (positive)
       2. 4.51.2. check_drop_impl_always_applicable / Drop impl is always applicable (positive)
       3. 4.51.3. check_drop_impl_always_applicable / Drop impl is always applicable premise@320 (negative)
       4. 4.51.4. check_drop_impl_always_applicable / Drop impl is always applicable premise@322 (negative)
       5. 4.51.5. check_drop_impl_always_applicable / Drop impl is always applicable premise@331 (negative)
   52. 4.52. check_all_crates
       1. 4.52.1. check_all_crates / check all prefixes (positive)
   53. 4.53. check_crate
       1. 4.53.1. check_crate / check crate (positive)
       2. 4.53.2. check_crate / check crate premise@70 (negative)
       3. 4.53.3. check_crate / check crate premise@71 (negative)
       4. 4.53.4. check_crate / check crate premise@74 (negative)
   54. 4.54. check_crate_item
       1. 4.54.1. check_crate_item / trait (positive)
       2. 4.54.2. check_crate_item / trait premise@187 (negative)
       3. 4.54.3. check_crate_item / trait impl (positive)
       4. 4.54.4. check_crate_item / trait impl premise@193 (negative)
       5. 4.54.5. check_crate_item / trait impl premise@194 (negative)
       6. 4.54.6. check_crate_item / adt (positive)
       7. 4.54.7. check_crate_item / adt premise@200 (negative)
       8. 4.54.8. check_crate_item / free fn (positive)
       9. 4.54.9. check_crate_item / free fn premise@206 (negative)
       10. 4.54.10. check_crate_item / neg trait impl (positive)
       11. 4.54.11. check_crate_item / neg trait impl premise@212 (negative)
       12. 4.54.12. check_crate_item / feature gate (positive)
   55. 4.55. check_trait
       1. 4.55.1. check_trait / check trait (positive)
       2. 4.55.2. check_trait / check trait premise@22 (negative)
       3. 4.55.3. check_trait / check trait premise@23 (negative)
   56. 4.56. check_trait_item
       1. 4.56.1. check_trait_item / fn in trait (positive)
       2. 4.56.2. check_trait_item / associated ty in trait (positive)
   57. 4.57. check_fn_in_trait
       1. 4.57.1. check_fn_in_trait / check fn in trait (positive)
   58. 4.58. check_associated_ty
       1. 4.58.1. check_associated_ty / check associated ty (positive)
   59. 4.59. codegen_function
   60. 4.60. codegen_block
   61. 4.61. codegen_stmt
   62. 4.62. codegen_expr_into
   63. 4.63. resolve_place
   64. 4.64. resolve_rigid
   65. 4.65. type_expr
   66. 4.66. may_be_remote
   67. 4.67. may_be_downstream_trait_ref
   68. 4.68. may_be_downstream_parameter
   69. 4.69. may_contain_downstream_type
   70. 4.70. normalizes_to_not_downstream
   71. 4.71. is_local_trait_ref
       1. 4.71.1. is_local_trait_ref / local trait (positive)
       2. 4.71.2. is_local_trait_ref / local trait premise@207 (negative)
       3. 4.71.3. is_local_trait_ref / local parameter (positive)
       4. 4.71.4. is_local_trait_ref / local parameter premise@215 (negative)
       5. 4.71.5. is_local_trait_ref / local parameter premise@220 (negative)
   72. 4.72. is_not_downstream
       1. 4.72.1. is_not_downstream / rigid (positive)
       2. 4.72.2. is_not_downstream / via normalize (positive)
       3. 4.72.3. is_not_downstream / via normalize premise@258 (negative)
   73. 4.73. is_local_parameter
       1. 4.73.1. is_local_parameter / local parameter (positive)
       2. 4.73.2. is_local_parameter / local parameter premise@287 (negative)
       3. 4.73.3. is_local_parameter / local parameter premise@289 (negative)
       4. 4.73.4. is_local_parameter / fundamental rigid type premise@296 (negative)
       5. 4.73.5. is_local_parameter / local rigid type (positive)
       6. 4.73.6. is_local_parameter / local rigid type premise@304 (negative)
       7. 4.73.7. is_local_parameter / existential variable (positive)
   74. 4.74. prove_after
       1. 4.74.1. prove_after / prove_after (positive)
       2. 4.74.2. prove_after / prove_after premise@19 (negative)
   75. 4.75. prove_const_has_type
       1. 4.75.1. prove_const_has_type / rigid constant (positive)
   76. 4.76. prove_eq
       1. 4.76.1. prove_eq / symmetric (positive)
       2. 4.76.2. prove_eq / symmetric premise@38 (negative)
       3. 4.76.3. prove_eq / rigid (positive)
       4. 4.76.4. prove_eq / rigid premise@47 (negative)
       5. 4.76.5. prove_eq / alias (positive)
       6. 4.76.6. prove_eq / alias premise@56 (negative)
       7. 4.76.7. prove_eq / existential (positive)
       8. 4.76.8. prove_eq / existential premise@62 (negative)
       9. 4.76.9. prove_eq / normalize-l (positive)
       10. 4.76.10. prove_eq / normalize-l premise@68 (negative)
       11. 4.76.11. prove_eq / normalize-l premise@69 (negative)
   77. 4.77. prove_existential_var_eq
       1. 4.77.1. prove_existential_var_eq / existential-nonvar (positive)
       2. 4.77.2. prove_existential_var_eq / existential-nonvar premise@94 (negative)
       3. 4.77.3. prove_existential_var_eq / existential-nonvar premise@95 (negative)
       4. 4.77.4. prove_existential_var_eq / existential-existential (positive)
       5. 4.77.5. prove_existential_var_eq / existential-universal (positive)
       6. 4.77.6. prove_existential_var_eq / existential-universal premise@140 (negative)
   78. 4.78. prove_normalize
       1. 4.78.1. prove_normalize / normalize-via-assumption (positive)
       2. 4.78.2. prove_normalize / normalize-via-assumption premise@32 (negative)
       3. 4.78.3. prove_normalize / normalize-via-impl (positive)
       4. 4.78.4. prove_normalize / normalize-via-impl premise@38 (negative)
   79. 4.79. prove_normalize_via
       1. 4.79.1. prove_normalize_via / axiom-l (positive)
       2. 4.79.2. prove_normalize_via / axiom-l premise@95 (negative)
   80. 4.80. prove_syntactically_eq
       1. 4.80.1. prove_syntactically_eq / symmetric (positive)
       2. 4.80.2. prove_syntactically_eq / symmetric premise@145 (negative)
       3. 4.80.3. prove_syntactically_eq / alias (positive)
       4. 4.80.4. prove_syntactically_eq / alias premise@163 (negative)
       5. 4.80.5. prove_syntactically_eq / existential-nonvar (positive)
       6. 4.80.6. prove_syntactically_eq / existential-nonvar premise@169 (negative)
   81. 4.81. main
   82. 4.82. prove_sub
       1. 4.82.1. prove_sub / normalize-l (positive)
       2. 4.82.2. prove_sub / normalize-l premise@27 (negative)
       3. 4.82.3. prove_sub / normalize-r (positive)
       4. 4.82.4. prove_sub / normalize-r premise@34 (negative)
       5. 4.82.5. prove_sub / rigid (positive)
       6. 4.82.6. prove_sub / lifetime => outlives (positive)
   83. 4.83. prove_via
       1. 4.83.1. prove_via / predicate-congruence-axiom (positive)
       2. 4.83.2. prove_via / predicate-congruence-axiom premise@30 (negative)
       3. 4.83.3. prove_via / relation-axiom (positive)
       4. 4.83.4. prove_via / forall (positive)
       5. 4.83.5. prove_via / forall premise@49 (negative)
   84. 4.84. prove_wc
       1. 4.84.1. prove_wc / forall (positive)
       2. 4.84.2. prove_wc / forall premise@35 (negative)
       3. 4.84.3. prove_wc / implies (positive)
       4. 4.84.4. prove_wc / implies premise@41 (negative)
       5. 4.84.5. prove_wc / assumption - predicate (positive)
       6. 4.84.6. prove_wc / assumption - predicate premise@48 (negative)
       7. 4.84.7. prove_wc / assumption - relation (positive)
       8. 4.84.8. prove_wc / assumption - relation premise@54 (negative)
       9. 4.84.9. prove_wc / positive impl (positive)
       10. 4.84.10. prove_wc / positive impl premise@79 (negative)
       11. 4.84.11. prove_wc / positive impl premise@80 (negative)
       12. 4.84.12. prove_wc / positive impl premise@86 (negative)
       13. 4.84.13. prove_wc / negative impl (positive)
       14. 4.84.14. prove_wc / alias eq (positive)
       15. 4.84.15. prove_wc / trait implied bound (positive)
       16. 4.84.16. prove_wc / trait implied bound premise@115 (negative)
       17. 4.84.17. prove_wc / trait implied bound premise@118 (negative)
       18. 4.84.18. prove_wc / trait implied bound premise@119 (negative)
       19. 4.84.19. prove_wc / eq (positive)
       20. 4.84.20. prove_wc / eq premise@125 (negative)
       21. 4.84.21. prove_wc / subtype (positive)
       22. 4.84.22. prove_wc / subtype premise@131 (negative)
       23. 4.84.23. prove_wc / trait well formed (positive)
       24. 4.84.24. prove_wc / trait well formed premise@137 (negative)
       25. 4.84.25. prove_wc / trait well formed premise@140 (negative)
       26. 4.84.26. prove_wc / trait ref is local (positive)
       27. 4.84.27. prove_wc / trait ref is local premise@146 (negative)
       28. 4.84.28. prove_wc / outlives (positive)
       29. 4.84.29. prove_wc / outlives premise@152 (negative)
       30. 4.84.30. prove_wc / parameter well formed (positive)
       31. 4.84.31. prove_wc / parameter well formed premise@159 (negative)
       32. 4.84.32. prove_wc / const has ty (positive)
       33. 4.84.33. prove_wc / const has ty premise@165 (negative)
       34. 4.84.34. prove_wc / const has ty premise@166 (negative)
   85. 4.85. prove_wc_list
       1. 4.85.1. prove_wc_list / none (positive)
       2. 4.85.2. prove_wc_list / some (positive)
       3. 4.85.3. prove_wc_list / some premise@26 (negative)
       4. 4.85.4. prove_wc_list / some premise@27 (negative)
   86. 4.86. prove_wf
       1. 4.86.1. prove_wf / universal variables (positive)
       2. 4.86.2. prove_wf / references (positive)
       3. 4.86.3. prove_wf / references premise@34 (negative)
       4. 4.86.4. prove_wf / tuples (positive)
       5. 4.86.5. prove_wf / integers and booleans (positive)
       6. 4.86.6. prove_wf / ADT (positive)
       7. 4.86.7. prove_wf / ADT premise@64 (negative)
       8. 4.86.8. prove_wf / static lifetime (positive)
       9. 4.86.9. prove_wf / scalar constants are always wf (positive)
       10. 4.86.10. prove_wf / aliases (positive)
5. 5. Coverage by test
   1. 5.1. local_can_be_moved (test_explicit_fail.rs:39)
   2. 5.2. deref_explicit_failure_message (test_explicit_fail.rs:44)
   3. 5.3. is_equal_22 (test_fallible.rs:58)
   4. 5.4. is_equal_44 (test_fallible.rs:63)
   5. 5.5. is_not_equal (test_fallible.rs:68)
   6. 5.6. judgment (test_filtered.rs:51)
   7. 5.7. judgment (test_filtered.rs:55)
   8. 5.8. test_for_all_success (test_for_all.rs:37)
   9. 5.9. test_for_all_failure (test_for_all.rs:43)
   10. 5.10. test_for_all_empty (test_for_all.rs:51)
   11. 5.11. test_for_all_with_accumulator (test_for_all.rs:74)
   12. 5.12. test_for_all_with_accumulator_empty (test_for_all.rs:80)
   13. 5.13. judgment (test_reachable.rs:51)
   14. 5.14. well_formed_adt (adt_wf.rs:30)
   15. 5.15. not_well_formed_adt (adt_wf.rs:44)
   16. 5.16. test_a (eq_assumptions.rs:15)
   17. 5.17. test_b (eq_assumptions.rs:24)
   18. 5.18. test_normalize_assoc_ty (eq_assumptions.rs:33)
   19. 5.19. test_normalize_assoc_ty_existential0 (eq_assumptions.rs:41)
   20. 5.20. test_normalize_assoc_ty_existential1 (eq_assumptions.rs:126)
   21. 5.21. eq_implies_partial_eq (eq_partial_eq.rs:25)
   22. 5.22. not_partial_eq_implies_eq (eq_partial_eq.rs:33)
   23. 5.23. universals_not_eq (eq_partial_eq.rs:44)
   24. 5.24. exists_u_for_t (exists_constraints.rs:24)
   25. 5.25. expanding (expanding.rs:23)
   26. 5.26. test_forall_not_local (is_local.rs:11)
   27. 5.27. test_exists_not_local (is_local.rs:26)
   28. 5.28. all_t_not_magic (magic_copy.rs:25)
   29. 5.29. all_t_not_copy (magic_copy.rs:40)
   30. 5.30. direct_cycle (occurs_check.rs:24)
   31. 5.31. eq_variable_to_rigid (occurs_check.rs:36)
   32. 5.32. eq_rigid_to_variable (occurs_check.rs:42)
   33. 5.33. indirect_cycle_1 (occurs_check.rs:48)
   34. 5.34. indirect_cycle_2 (occurs_check.rs:60)
   35. 5.35. vec_u32_debug (simple_impl.rs:24)
   36. 5.36. vec_vec_u32_debug (simple_impl.rs:30)
   37. 5.37. exists_u_for_t (universes.rs:14)
   38. 5.38. for_t_exists_u (universes.rs:37)
   39. 5.39. test_mirror_normalizes_u32_to_u32 (associated_type_normalization.rs:19)
   40. 5.40. hello_world_fail (basic_tests.rs:34)
   41. 5.41. hello_world (basic_tests.rs:58)
   42. 5.42. basic_where_clauses_pass (basic_tests.rs:74)
   43. 5.43. basic_where_clauses_fail (basic_tests.rs:85)
   44. 5.44. basic_where_clauses_without_lifetime_binders_feature_flag_fail (basic_tests.rs:103)
   45. 5.45. foo (basic_tests.rs:121)
   46. 5.46. foo (basic_tests.rs:133)
   47. 5.47. non_lifetime_binder_in_trait_impl_where_clause_pass (basic_tests.rs:149)
   48. 5.48. non_lifetime_binder_in_trait_impl_where_clause_fail (basic_tests.rs:161)
   49. 5.49. non_lifetime_binder_in_neg_trait_impl_where_clause_pass (basic_tests.rs:179)
   50. 5.50. non_lifetime_binder_in_neg_trait_impl_where_clause_fail (basic_tests.rs:191)
   51. 5.51. non_lifetime_binder_in_enum_where_clause_pass (basic_tests.rs:209)
   52. 5.52. non_lifetime_binder_in_enum_where_clause_fail (basic_tests.rs:221)
   53. 5.53. non_lifetime_binder_in_struct_where_clause_pass (basic_tests.rs:239)
   54. 5.54. non_lifetime_binder_in_struct_where_clause_fail (basic_tests.rs:251)
   55. 5.55. lifetime_binder_in_where_clause_without_feature_pass (basic_tests.rs:266)
   56. 5.56. basic_adt_variant_dup (basic_tests.rs:277)
   57. 5.57. basic_adt_field_dup (basic_tests.rs:290)
   58. 5.58. basic_tests.rs:303
   59. 5.59. trait_items_with_duplicate_associated_type_names (basic_tests.rs:316)
   60. 5.60. crate_with_duplicate_item_names (basic_tests.rs:328)
   61. 5.61. crate_with_duplicate_item_names (basic_tests.rs:337)
   62. 5.62. a (basic_tests.rs:346)
   63. 5.63. a (basic_tests.rs:356)
   64. 5.64. basic_impl_dup (basic_tests.rs:367)
   65. 5.65. basic_neg_impl_dup (basic_tests.rs:380)
   66. 5.66. basic_tests.rs:394
   67. 5.67. basic_tests.rs:411
   68. 5.68. basic_tests.rs:426
   69. 5.69. foo (borrowck.rs:44)
   70. 5.70. foo (borrowck.rs:89)
   71. 5.71. foo (borrowck.rs:128)
   72. 5.72. foo (borrowck.rs:154)
   73. 5.73. foo (borrowck.rs:201)
   74. 5.74. foo (borrowck.rs:227)
   75. 5.75. foo (borrowck.rs:253)
   76. 5.76. foo (borrowck.rs:304)
   77. 5.77. reborrow (borrowck.rs:331)
   78. 5.78. foo (borrowck.rs:357)
   79. 5.79. foo (borrowck.rs:400)
   80. 5.80. foo (borrowck.rs:434)
   81. 5.81. foo (borrowck.rs:476)
   82. 5.82. foo (borrowck.rs:518)
   83. 5.83. foo (borrowck.rs:557)
   84. 5.84. foo (borrowck.rs:603)
   85. 5.85. foo (borrowck.rs:1262)
   86. 5.86. foo (borrowck.rs:1922)
   87. 5.87. foo (borrowck.rs:1988)
   88. 5.88. foo (borrowck.rs:2031)
   89. 5.89. foo (borrowck.rs:2069)
   90. 5.90. min_problem_case_3 (borrowck.rs:2119)
   91. 5.91. min_problem_case_3 (borrowck.rs:2155)
   92. 5.92. min_problem_case_3 (borrowck.rs:2162)
   93. 5.93. foo (borrowck.rs:2191)
   94. 5.94. foo (borrowck.rs:2235)
   95. 5.95. foo (borrowck.rs:2263)
   96. 5.96. foo (borrowck.rs:2305)
   97. 5.97. min_problem_case_3 (borrowck.rs:2350)
   98. 5.98. foo (borrowck.rs:2364)
   99. 5.99. foo (borrowck.rs:2386)
   100. 5.100. foo (borrowck.rs:2412)
   101. 5.101. foo (borrowck.rs:2429)
   102. 5.102. foo (borrowck.rs:2443)
   103. 5.103. min_problem_case_4 (borrowck.rs:2471)
   104. 5.104. foo (borrowck.rs:2604)
   105. 5.105. foo (borrowck.rs:2624)
   106. 5.106. foo (borrowck.rs:2671)
   107. 5.107. foo (borrowck.rs:2738)
   108. 5.108. foo (borrowck.rs:2794)
   109. 5.109. foo (borrowck.rs:2822)
   110. 5.110. foo (borrowck.rs:2865)
   111. 5.111. if_false_borrowck (borrowck.rs:2928)
   112. 5.112. if_false_borrowck (borrowck.rs:2961)
   113. 5.113. if_false_borrowck (borrowck.rs:2968)
   114. 5.114. foo (borrowck.rs:3000)
   115. 5.115. foo (borrowck.rs:3041)
   116. 5.116. bar (borrowck.rs:3063)
   117. 5.117. foo (borrowck.rs:3091)
   118. 5.118. foo (borrowck.rs:3116)
   119. 5.119. foo (borrowck.rs:3136)
   120. 5.120. bar (borrowck.rs:3157)
   121. 5.121. bar (borrowck.rs:3179)
   122. 5.122. foo (borrowck.rs:3211)
   123. 5.123. foo (borrowck.rs:3227)
   124. 5.124. foo (borrowck.rs:3261)
   125. 5.125. foo (borrowck.rs:3298)
   126. 5.126. reborrow (borrowck.rs:3330)
   127. 5.127. outlive_before_return_does_not_affect_merged_paths (borrowck.rs:3360)
   128. 5.128. outlive_before_return_does_not_affect_merged_paths (borrowck.rs:3396)
   129. 5.129. outlive_before_return_does_not_affect_merged_paths (borrowck.rs:3403)
   130. 5.130. reborrow (borrowck.rs:3420)
   131. 5.131. reborrow (borrowck.rs:3440)
   132. 5.132. foo (borrowck.rs:3468)
   133. 5.133. foo (borrowck.rs:3508)
   134. 5.134. foo (borrowck.rs:3528)
   135. 5.135. foo (borrowck.rs:3632)
   136. 5.136. foo (borrowck.rs:3657)
   137. 5.137. foo (borrowck.rs:3670)
   138. 5.138. issue_63908_remove_last_node_recursive (borrowck.rs:3813)
   139. 5.139. issue_63908_remove_last_node_recursive (borrowck.rs:3821)
   140. 5.140. issue_63908_remove_last_node_recursive (borrowck.rs:3829)
   141. 5.141. issue_63908_remove_last_node_iterative (borrowck.rs:3881)
   142. 5.142. issue_63908_remove_last_node_iterative (borrowck.rs:3906)
   143. 5.143. issue_63908_remove_last_node_iterative (borrowck.rs:3931)
   144. 5.144. issue_57165_no_control_flow (borrowck.rs:3979)
   145. 5.145. issue_57165_no_control_flow (borrowck.rs:3987)
   146. 5.146. issue_57165_no_control_flow (borrowck.rs:3995)
   147. 5.147. issue_57165_conditional (borrowck.rs:4047)
   148. 5.148. issue_57165_conditional (borrowck.rs:4094)
   149. 5.149. issue_57165_conditional (borrowck.rs:4141)
   150. 5.150. issue_57165_conditional_with_indirection (borrowck.rs:4196)
   151. 5.151. issue_57165_conditional_with_indirection (borrowck.rs:4204)
   152. 5.152. issue_57165_conditional_with_indirection (borrowck.rs:4212)
   153. 5.153. issue_46859_to_refs (borrowck.rs:4267)
   154. 5.154. issue_46859_to_refs (borrowck.rs:4275)
   155. 5.155. issue_46859_to_refs (borrowck.rs:4283)
   156. 5.156. issue_46859_to_refs2 (borrowck.rs:4321)
   157. 5.157. issue_46859_to_refs2 (borrowck.rs:4329)
   158. 5.158. issue_46859_to_refs2 (borrowck.rs:4337)
   159. 5.159. issue_46859_to_refs3 (borrowck.rs:4386)
   160. 5.160. issue_46859_to_refs3 (borrowck.rs:4393)
   161. 5.161. issue_46859_to_refs3 (borrowck.rs:4400)
   162. 5.162. issue_46859_decoder_next (borrowck.rs:4446)
   163. 5.163. issue_46859_decoder_next (borrowck.rs:4524)
   164. 5.164. issue_46859_decoder_next (borrowck.rs:4532)
   165. 5.165. issue_92985_filtering_lending_iterator (borrowck.rs:4588)
   166. 5.166. issue_92985_filtering_lending_iterator (borrowck.rs:4666)
   167. 5.167. issue_92985_filtering_lending_iterator (borrowck.rs:4674)
   168. 5.168. flow_sensitive_invariance_use_it (borrowck.rs:4726)
   169. 5.169. flow_sensitive_invariance_use_it (borrowck.rs:4737)
   170. 5.170. flow_sensitive_invariance_use_it (borrowck.rs:4748)
   171. 5.171. flow_sensitive_invariance_use_both (borrowck.rs:4781)
   172. 5.172. flow_sensitive_invariance_use_both (borrowck.rs:4791)
   173. 5.173. flow_sensitive_invariance_use_both (borrowck.rs:4801)
   174. 5.174. flow_sensitive_invariance_same_region (borrowck.rs:4841)
   175. 5.175. flow_sensitive_invariance_same_region (borrowck.rs:4849)
   176. 5.176. flow_sensitive_invariance_same_region (borrowck.rs:4857)
   177. 5.177. main (codegen.rs:11)
   178. 5.178. main (codegen.rs:24)
   179. 5.179. main (codegen.rs:36)
   180. 5.180. main (codegen.rs:49)
   181. 5.181. main (codegen.rs:64)
   182. 5.182. main (codegen.rs:79)
   183. 5.183. main (codegen.rs:95)
   184. 5.184. main (codegen.rs:110)
   185. 5.185. main (codegen.rs:127)
   186. 5.186. main (codegen.rs:141)
   187. 5.187. main (codegen.rs:171)
   188. 5.188. main (codegen.rs:188)
   189. 5.189. main (codegen.rs:201)
   190. 5.190. main (codegen.rs:218)
   191. 5.191. main (codegen.rs:238)
   192. 5.192. main (codegen.rs:251)
   193. 5.193. main (codegen.rs:264)
   194. 5.194. main (codegen.rs:318)
   195. 5.195. main (codegen.rs:336)
   196. 5.196. main (codegen.rs:356)
   197. 5.197. main (codegen.rs:377)
   198. 5.198. main (codegen.rs:443)
   199. 5.199. main (codegen.rs:461)
   200. 5.200. main (codegen.rs:477)
   201. 5.201. neg_CoreTrait_for_CoreStruct_in_Foo (coherence_orphan.rs:12)
   202. 5.202. mirror_CoreStruct (coherence_orphan.rs:47)
   203. 5.203. mirror_FooStruct (coherence_orphan.rs:84)
   204. 5.204. covered_VecT (coherence_orphan.rs:98)
   205. 5.205. raw_pointer_is_not_fundamental (coherence_orphan.rs:111)
   206. 5.206. uncovered_T (coherence_orphan.rs:133)
   207. 5.207. alias_to_unit (coherence_orphan.rs:160)
   208. 5.208. CoreTrait_for_CoreStruct_in_Foo (coherence_orphan.rs:182)
   209. 5.209. CoreTraitLocal_for_AliasToKnown_in_Foo (coherence_orphan.rs:220)
   210. 5.210. u32_not_u32_impls (coherence_overlap.rs:129)
   211. 5.211. neg_CoreTrait_for_CoreStruct_implies_no_overlap (coherence_overlap.rs:147)
   212. 5.212. foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait (coherence_overlap.rs:161)
   213. 5.213. T_where_Foo_not_u32_impls (coherence_overlap.rs:174)
   214. 5.214. u32_T_where_T_Is_impls (coherence_overlap.rs:189)
   215. 5.215. u32_T_where_T_Not_impls (coherence_overlap.rs:206)
   216. 5.216. u32_u32_impls (coherence_overlap.rs:216)
   217. 5.217. u32_i32_impls (coherence_overlap.rs:229)
   218. 5.218. u32_T_impls (coherence_overlap.rs:239)
   219. 5.219. T_and_T_bar (coherence_overlap.rs:257)
   220. 5.220. T_and_Local_Bar_T (coherence_overlap.rs:277)
   221. 5.221. is_local_unknowable_trait_ref (coherence_overlap.rs:307)
   222. 5.222. is_local_with_unconstrained_self_ty_blanket_impl (coherence_overlap.rs:333)
   223. 5.223. parse_minirust_22 (const_generics_rv_tsv_parse.rs:11)
   224. 5.224. nonsense_rigid_const_bound (consts.rs:11)
   225. 5.225. ok (consts.rs:23)
   226. 5.226. mismatch (consts.rs:32)
   227. 5.227. holds (consts.rs:49)
   228. 5.228. rigid_const_bound (consts.rs:58)
   229. 5.229. generic_mismatch (consts.rs:68)
   230. 5.230. generic_match (consts.rs:92)
   231. 5.231. multiple_type_of_const (consts.rs:101)
   232. 5.232. unsafe_trait (decl_safety.rs:12)
   233. 5.233. safe_trait (decl_safety.rs:22)
   234. 5.234. unsafe_trait_negative_impl (decl_safety.rs:32)
   235. 5.235. unsafe_trait_negative_impl_mismatch (decl_safety.rs:41)
   236. 5.236. safe_trait_negative_impl_mismatch (decl_safety.rs:52)
   237. 5.237. unsafe_trait_mismatch (decl_safety.rs:63)
   238. 5.238. safe_trait_mismatch (decl_safety.rs:74)
   239. 5.239. drop_impl_simple_struct (drop.rs:20)
   240. 5.240. drop_impl_generic_struct (drop.rs:38)
   241. 5.241. drop_impl_generic_no_where_clauses (drop.rs:54)
   242. 5.242. drop_impl_subset_where_clauses (drop.rs:78)
   243. 5.243. drop_impl_enum (drop.rs:94)
   244. 5.244. drop_impl_cross_crate_local (drop.rs:111)
   245. 5.245. drop_impl_extra_where_clause (drop.rs:132)
   246. 5.246. drop_impl_concrete_type_param (drop.rs:154)
   247. 5.247. drop_impl_enum_extra_where_clause (drop.rs:191)
   248. 5.248. drop_impl_foreign_adt (drop.rs:214)
   249. 5.249. drop_impl_for_non_adt (drop.rs:227)
   250. 5.250. test (field_projections.rs:17)
   251. 5.251. functions.rs:24
   252. 5.252. functions.rs:37
   253. 5.253. test (cyclic_judgment.rs:73)
   254. 5.254. test1 (cyclic_judgment.rs:133)
   255. 5.255. foo (mir_typeck.rs:13)
   256. 5.256. foo (mir_typeck.rs:35)
   257. 5.257. foo (mir_typeck.rs:89)
   258. 5.258. foo (mir_typeck.rs:105)
   259. 5.259. foo (mir_typeck.rs:117)
   260. 5.260. foo (mir_typeck.rs:133)
   261. 5.261. foo (mir_typeck.rs:147)
   262. 5.262. bar (mir_typeck.rs:171)
   263. 5.263. foo (mir_typeck.rs:191)
   264. 5.264. foo (mir_typeck.rs:234)
   265. 5.265. foo (mir_typeck.rs:250)
   266. 5.266. foo (mir_typeck.rs:266)
   267. 5.267. bar (mir_typeck.rs:280)
   268. 5.268. bar (mir_typeck.rs:300)
   269. 5.269. bar (mir_typeck.rs:323)
   270. 5.270. bar (mir_typeck.rs:345)
   271. 5.271. bar (mir_typeck.rs:360)
   272. 5.272. bar (mir_typeck.rs:383)
   273. 5.273. bar (mir_typeck.rs:401)
   274. 5.274. foo (mir_typeck.rs:421)
   275. 5.275. foo (mir_typeck.rs:595)
   276. 5.276. foo (mir_typeck.rs:613)
   277. 5.277. foo (mir_typeck.rs:630)
   278. 5.278. foo (mir_typeck.rs:648)
   279. 5.279. foo (mir_typeck.rs:670)
   280. 5.280. foo (mir_typeck.rs:693)
   281. 5.281. foo (mir_typeck.rs:710)
   282. 5.282. foo (mir_typeck.rs:729)
   283. 5.283. foo (mir_typeck.rs:755)
   284. 5.284. foo (mir_typeck.rs:776)
   285. 5.285. foo (mir_typeck.rs:802)
   286. 5.286. foo (mir_typeck.rs:825)
   287. 5.287. foo (mir_typeck.rs:857)
   288. 5.288. foo (mir_typeck.rs:882)
   289. 5.289. normalize_basic (projection.rs:25)
   290. 5.290. normalize_basic (projection.rs:31)
   291. 5.291. normalize_basic (projection.rs:36)
   292. 5.292. normalize_basic (projection.rs:44)
   293. 5.293. normalize_basic (projection.rs:50)
   294. 5.294. normalize_basic (projection.rs:55)
   295. 5.295. normalize_into_iterator (projection.rs:89)
   296. 5.296. projection_equality (projection.rs:112)
   297. 5.297. projection_equality (projection.rs:115)
   298. 5.298. references.rs:13
   299. 5.299. references.rs:36
   300. 5.300. foo (return_validation.rs:31)
   301. 5.301. foo (return_validation.rs:48)
   302. 5.302. foo (return_validation.rs:79)
   303. 5.303. foo (return_validation.rs:111)
   304. 5.304. foo (return_validation.rs:124)
   305. 5.305. traits.rs:13
   306. 5.306. trait_with_valid_associated_type (traits.rs:26)
   307. 5.307. main (well_formed_struct.rs:17)
   308. 5.308. dependent_where_clause (well_formed_trait_ref.rs:19)
   309. 5.309. missing_dependent_where_clause (well_formed_trait_ref.rs:37)
   310. 5.310. lifetime_param (well_formed_trait_ref.rs:56)
   311. 5.311. static_lifetime_param (well_formed_trait_ref.rs:71)
   312. 5.312. const_param (well_formed_trait_ref.rs:86)