Report #28 — ASCII classification, string views and sequence updates

Toolchain source metadata: not recorded.

Run locally

git clone -- https://github.com/nyuichi/rust-crate-proofs report-28-source-1
git -C report-28-source-1 checkout --detach 64144e62d129617852e3387fbcdcc03f653c0dee
git -C report-28-source-1 submodule update --init --recursive --checkout
cd report-28-source-1/ascii/1.1.0/aeneas/2026-11-05/proofs

lake build +BorrowViewProofs +CharForwardProofs +ErrorDescriptionProofs +ErrorProjectionProofs +GenericErrorProofs +Proofs +SelfBorrowProofs +SliceProofs +StringBorrowViewProofs +StringProofs +VectorIdentityProofs

printf '%s' 'import Lean
import BorrowViewProofs
import CharForwardProofs
import ErrorDescriptionProofs
import ErrorProjectionProofs
import GenericErrorProofs
import Proofs
import SelfBorrowProofs
import SliceProofs
import StringBorrowViewProofs
import StringProofs
import VectorIdentityProofs
open Lean Elab Command

run_cmd do
  let theorem_name := `Proofs.is_ascii_blank_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.is_ascii_blank_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.is_ascii_blank_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.is_ascii_blank_spec"

run_cmd do
  let theorem_name := `Proofs.is_ascii_digit_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.is_ascii_digit_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.is_ascii_digit_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.is_ascii_digit_spec"

run_cmd do
  let theorem_name := `Proofs.is_ascii_whitespace_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.is_ascii_whitespace_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.is_ascii_whitespace_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.is_ascii_whitespace_spec"

run_cmd do
  let theorem_name := `Proofs.is_ascii_control_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.is_ascii_control_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.is_ascii_control_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.is_ascii_control_spec"

run_cmd do
  let theorem_name := `Proofs.is_ascii_alphabetic_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.is_ascii_alphabetic_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.is_ascii_alphabetic_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.is_ascii_alphabetic_spec"

run_cmd do
  let theorem_name := `Proofs.is_ascii_alphanumeric_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.is_ascii_alphanumeric_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.is_ascii_alphanumeric_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.is_ascii_alphanumeric_spec"

run_cmd do
  let theorem_name := `Proofs.is_ascii_graphic_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.is_ascii_graphic_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.is_ascii_graphic_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.is_ascii_graphic_spec"

run_cmd do
  let theorem_name := `Proofs.is_ascii_printable_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.is_ascii_printable_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.is_ascii_printable_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.is_ascii_printable_spec"

run_cmd do
  let theorem_name := `Proofs.is_ascii_lowercase_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.is_ascii_lowercase_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.is_ascii_lowercase_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.is_ascii_lowercase_spec"

run_cmd do
  let theorem_name := `Proofs.is_ascii_uppercase_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.is_ascii_uppercase_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.is_ascii_uppercase_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.is_ascii_uppercase_spec"

run_cmd do
  let theorem_name := `Proofs.is_ascii_hexdigit_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.is_ascii_hexdigit_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.is_ascii_hexdigit_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.is_ascii_hexdigit_spec"

run_cmd do
  let theorem_name := `Proofs.as_byte_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.as_byte_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.as_byte_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.as_byte_spec"

run_cmd do
  let theorem_name := `Proofs.eq_ignore_ascii_case_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.eq_ignore_ascii_case_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.eq_ignore_ascii_case_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.eq_ignore_ascii_case_spec"

run_cmd do
  let theorem_name := `Proofs.to_ascii_char_identity_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.to_ascii_char_identity_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.to_ascii_char_identity_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.to_ascii_char_identity_spec"

run_cmd do
  let theorem_name := `Proofs.to_ascii_char_unchecked_identity_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.to_ascii_char_unchecked_identity_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.to_ascii_char_unchecked_identity_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.to_ascii_char_unchecked_identity_spec"

run_cmd do
  let theorem_name := `Proofs.is_alphabetic_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.is_alphabetic_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.is_alphabetic_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.is_alphabetic_spec"

run_cmd do
  let theorem_name := `Proofs.is_alphanumeric_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.is_alphanumeric_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.is_alphanumeric_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.is_alphanumeric_spec"

run_cmd do
  let theorem_name := `Proofs.is_lowercase_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.is_lowercase_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.is_lowercase_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.is_lowercase_spec"

run_cmd do
  let theorem_name := `Proofs.is_uppercase_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.is_uppercase_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.is_uppercase_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.is_uppercase_spec"

run_cmd do
  let theorem_name := `Proofs.is_whitespace_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.is_whitespace_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.is_whitespace_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.is_whitespace_spec"

run_cmd do
  let theorem_name := `Proofs.is_digit_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.is_digit_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.is_digit_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.is_digit_spec"

run_cmd do
  let theorem_name := `Proofs.is_ascii_punctuation_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.is_ascii_punctuation_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.is_ascii_punctuation_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.is_ascii_punctuation_spec"

run_cmd do
  let theorem_name := `Proofs.default_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.default_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.default_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.default_spec"

run_cmd do
  let theorem_name := `Proofs.valid_up_to_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: Proofs.valid_up_to_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in Proofs.valid_up_to_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:Proofs.valid_up_to_spec"

run_cmd do
  let theorem_name := `StringProofs.new_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: StringProofs.new_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in StringProofs.new_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:StringProofs.new_spec"

run_cmd do
  let theorem_name := `StringProofs.len_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: StringProofs.len_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in StringProofs.len_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:StringProofs.len_spec"

run_cmd do
  let theorem_name := `StringProofs.is_empty_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: StringProofs.is_empty_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in StringProofs.is_empty_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:StringProofs.is_empty_spec"

run_cmd do
  let theorem_name := `StringProofs.push_full_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: StringProofs.push_full_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in StringProofs.push_full_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:StringProofs.push_full_spec"

run_cmd do
  let theorem_name := `SliceProofs.as_slice_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: SliceProofs.as_slice_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in SliceProofs.as_slice_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:SliceProofs.as_slice_spec"

run_cmd do
  let theorem_name := `SliceProofs.as_mut_slice_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: SliceProofs.as_mut_slice_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in SliceProofs.as_mut_slice_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:SliceProofs.as_mut_slice_spec"

run_cmd do
  let theorem_name := `SliceProofs.len_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: SliceProofs.len_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in SliceProofs.len_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:SliceProofs.len_spec"

run_cmd do
  let theorem_name := `SliceProofs.is_empty_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: SliceProofs.is_empty_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in SliceProofs.is_empty_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:SliceProofs.is_empty_spec"

run_cmd do
  let theorem_name := `SliceProofs.as_ascii_str_identity_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: SliceProofs.as_ascii_str_identity_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in SliceProofs.as_ascii_str_identity_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:SliceProofs.as_ascii_str_identity_spec"

run_cmd do
  let theorem_name := `SliceProofs.as_ascii_str_unchecked_identity_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: SliceProofs.as_ascii_str_unchecked_identity_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in SliceProofs.as_ascii_str_unchecked_identity_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:SliceProofs.as_ascii_str_unchecked_identity_spec"

run_cmd do
  let theorem_name := `SliceProofs.as_mut_ascii_str_unchecked_identity_spec
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: SliceProofs.as_mut_ascii_str_unchecked_identity_spec"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in SliceProofs.as_mut_ascii_str_unchecked_identity_spec: {ax}"
  liftIO <| IO.println "proofs.rs:checked:SliceProofs.as_mut_ascii_str_unchecked_identity_spec"

run_cmd do
  let theorem_name := `ErrorProjectionProofs.ascii_error_exact
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: ErrorProjectionProofs.ascii_error_exact"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in ErrorProjectionProofs.ascii_error_exact: {ax}"
  liftIO <| IO.println "proofs.rs:checked:ErrorProjectionProofs.ascii_error_exact"

run_cmd do
  let theorem_name := `ErrorProjectionProofs.into_source_exact
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: ErrorProjectionProofs.into_source_exact"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in ErrorProjectionProofs.into_source_exact: {ax}"
  liftIO <| IO.println "proofs.rs:checked:ErrorProjectionProofs.into_source_exact"

run_cmd do
  let theorem_name := `VectorIdentityProofs.from_vector_exact
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: VectorIdentityProofs.from_vector_exact"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in VectorIdentityProofs.from_vector_exact: {ax}"
  liftIO <| IO.println "proofs.rs:checked:VectorIdentityProofs.from_vector_exact"

run_cmd do
  let theorem_name := `VectorIdentityProofs.into_vector_exact
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: VectorIdentityProofs.into_vector_exact"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in VectorIdentityProofs.into_vector_exact: {ax}"
  liftIO <| IO.println "proofs.rs:checked:VectorIdentityProofs.into_vector_exact"

run_cmd do
  let theorem_name := `VectorIdentityProofs.checked_exact
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: VectorIdentityProofs.checked_exact"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in VectorIdentityProofs.checked_exact: {ax}"
  liftIO <| IO.println "proofs.rs:checked:VectorIdentityProofs.checked_exact"

run_cmd do
  let theorem_name := `VectorIdentityProofs.unchecked_exact
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: VectorIdentityProofs.unchecked_exact"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in VectorIdentityProofs.unchecked_exact: {ax}"
  liftIO <| IO.println "proofs.rs:checked:VectorIdentityProofs.unchecked_exact"

run_cmd do
  let theorem_name := `BorrowViewProofs.as_ref_slice_exact
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: BorrowViewProofs.as_ref_slice_exact"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in BorrowViewProofs.as_ref_slice_exact: {ax}"
  liftIO <| IO.println "proofs.rs:checked:BorrowViewProofs.as_ref_slice_exact"

run_cmd do
  let theorem_name := `BorrowViewProofs.as_mut_slice_contract
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: BorrowViewProofs.as_mut_slice_contract"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in BorrowViewProofs.as_mut_slice_contract: {ax}"
  liftIO <| IO.println "proofs.rs:checked:BorrowViewProofs.as_mut_slice_contract"

run_cmd do
  let theorem_name := `BorrowViewProofs.as_ref_self_exact
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: BorrowViewProofs.as_ref_self_exact"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in BorrowViewProofs.as_ref_self_exact: {ax}"
  liftIO <| IO.println "proofs.rs:checked:BorrowViewProofs.as_ref_self_exact"

run_cmd do
  let theorem_name := `StringBorrowViewProofs.as_ref_slice_exact
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: StringBorrowViewProofs.as_ref_slice_exact"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in StringBorrowViewProofs.as_ref_slice_exact: {ax}"
  liftIO <| IO.println "proofs.rs:checked:StringBorrowViewProofs.as_ref_slice_exact"

run_cmd do
  let theorem_name := `StringBorrowViewProofs.as_mut_slice_contract
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: StringBorrowViewProofs.as_mut_slice_contract"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in StringBorrowViewProofs.as_mut_slice_contract: {ax}"
  liftIO <| IO.println "proofs.rs:checked:StringBorrowViewProofs.as_mut_slice_contract"

run_cmd do
  let theorem_name := `SelfBorrowProofs.as_mut_self_exact
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: SelfBorrowProofs.as_mut_self_exact"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in SelfBorrowProofs.as_mut_self_exact: {ax}"
  liftIO <| IO.println "proofs.rs:checked:SelfBorrowProofs.as_mut_self_exact"

run_cmd do
  let theorem_name := `ErrorDescriptionProofs.char_description_exact
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: ErrorDescriptionProofs.char_description_exact"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in ErrorDescriptionProofs.char_description_exact: {ax}"
  liftIO <| IO.println "proofs.rs:checked:ErrorDescriptionProofs.char_description_exact"

run_cmd do
  let theorem_name := `ErrorDescriptionProofs.str_description_exact
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: ErrorDescriptionProofs.str_description_exact"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in ErrorDescriptionProofs.str_description_exact: {ax}"
  liftIO <| IO.println "proofs.rs:checked:ErrorDescriptionProofs.str_description_exact"

run_cmd do
  let theorem_name := `CharForwardProofs.from_ascii_exact
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: CharForwardProofs.from_ascii_exact"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in CharForwardProofs.from_ascii_exact: {ax}"
  liftIO <| IO.println "proofs.rs:checked:CharForwardProofs.from_ascii_exact"

run_cmd do
  let theorem_name := `GenericErrorProofs.description_exact
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: GenericErrorProofs.description_exact"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in GenericErrorProofs.description_exact: {ax}"
  liftIO <| IO.println "proofs.rs:checked:GenericErrorProofs.description_exact"
' | lake env lean --stdin

Checks out the recorded source commit from GitHub. Install the report’s tool version before running.

Source on GitHub · SARIF with logs (.json)

Recorded run

Completed · 51 checks passed · 0 failed

2026-11-05T17:23:49.674808434+00:00 · 197.7 seconds · Exit code 0

Recorded on the author’s machine.

=== stdout ===
⚠ [2/57] Ran aeneas:extraDep
warning: building from source; failed to fetch GitHub release (run with '-v' for details)
✔ [3/178] Built AeneasMeta.Simp.RegisterCommand (40s)
✔ [123/397] Built AeneasMeta.BvEnumToBitVec (40s)
✔ [343/712] Built Aeneas.Std.Global (40s)
✔ [344/712] Built AeneasMeta.UtilsCore (40s)
✔ [1575/1809] Built AeneasMeta.OptionConfig (41s)
✔ [1797/1809] Built Generated.Ascii (2.9s)
ℹ [1798/1809] Built SelfBorrowProofs (3.1s)
info: SelfBorrowProofs.lean:14:0: 'SelfBorrowProofs.as_mut_self_exact' depends on axioms: [propext, Quot.sound]
info: SelfBorrowProofs.lean:15:0: 'SelfBorrowProofs.same_length_writeback' depends on axioms: [propext, Quot.sound]
⚠ [1799/1809] Built VectorIdentityProofs (3.2s)
warning: VectorIdentityProofs.lean:8:178: This simp argument is unused:
  bind_tc_ok

Hint: Omit it from the simp argument list.
  [apply] simp [ascii.alloc.vec.VecAsciiChar.Insts.AsciiAscii_stringIntoAsciiString.into_ascii_string,
    ascii.ascii_string.AsciiString.Insts.CoreConvertFromVecAsciiChar.from, Std.bind_ok]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: VectorIdentityProofs.lean:13:0: 'VectorIdentityProofs.from_vector_exact' depends on axioms: [propext, Quot.sound]
info: VectorIdentityProofs.lean:14:0: 'VectorIdentityProofs.checked_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
info: VectorIdentityProofs.lean:15:0: 'VectorIdentityProofs.unchecked_exact' depends on axioms: [propext, Quot.sound]
info: VectorIdentityProofs.lean:17:0: 'VectorIdentityProofs.into_vector_exact' depends on axioms: [propext, Quot.sound]
⚠ [1800/1809] Built StringProofs (3.5s)
warning: StringProofs.lean:16:37: Local variable 'c' resembles constructor 'ascii.ascii_char.AsciiChar.c' - write '.c' (with a dot) or 'ascii.ascii_char.AsciiChar.c' to use the constructor.

Note: This linter can be disabled with `set_option linter.constructorNameAsVariable false`
warning: StringProofs.lean:22:45: Local variable 'c' resembles constructor 'ascii.ascii_char.AsciiChar.c' - write '.c' (with a dot) or 'ascii.ascii_char.AsciiChar.c' to use the constructor.

Note: This linter can be disabled with `set_option linter.constructorNameAsVariable false`
warning: StringProofs.lean:27:20: Unused tactic linter: `<;>` should be replaced with `;` or be removed.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: StringProofs.lean:27:20: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: StringProofs.lean:28:42: Local variable 'c' resembles constructor 'ascii.ascii_char.AsciiChar.c' - write '.c' (with a dot) or 'ascii.ascii_char.AsciiChar.c' to use the constructor.

Note: This linter can be disabled with `set_option linter.constructorNameAsVariable false`
info: StringProofs.lean:37:0: 'StringProofs.new_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: StringProofs.lean:38:0: 'StringProofs.len_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: StringProofs.lean:39:0: 'StringProofs.is_empty_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: StringProofs.lean:40:0: 'StringProofs.push_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: StringProofs.lean:41:0: 'StringProofs.push_maximum_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: StringProofs.lean:43:0: 'StringProofs.push_full_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1801/1809] Built StringBorrowViewProofs (3.8s)
info: StringBorrowViewProofs.lean:25:0: 'StringBorrowViewProofs.as_ref_slice_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
info: StringBorrowViewProofs.lean:26:0: 'StringBorrowViewProofs.as_mut_slice_contract' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1802/1809] Built GenericErrorProofs (3.8s)
info: GenericErrorProofs.lean:10:0: 'GenericErrorProofs.description_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1803/1809] Built SliceProofs (3.9s)
info: SliceProofs.lean:33:0: 'SliceProofs.as_slice_spec' depends on axioms: [propext, Quot.sound]
info: SliceProofs.lean:34:0: 'SliceProofs.as_mut_slice_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SliceProofs.lean:35:0: 'SliceProofs.len_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SliceProofs.lean:36:0: 'SliceProofs.is_empty_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: SliceProofs.lean:38:0: 'SliceProofs.as_ascii_str_identity_spec' depends on axioms: [propext, Quot.sound]
info: SliceProofs.lean:39:0: 'SliceProofs.as_ascii_str_unchecked_identity_spec' depends on axioms: [propext, Quot.sound]
info: SliceProofs.lean:40:0: 'SliceProofs.as_mut_ascii_str_unchecked_identity_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1804/1809] Built ErrorDescriptionProofs (3.3s)
info: ErrorDescriptionProofs.lean:14:0: 'ErrorDescriptionProofs.char_description_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
info: ErrorDescriptionProofs.lean:15:0: 'ErrorDescriptionProofs.str_description_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [1805/1809] Built ErrorProjectionProofs (5.0s)
info: ErrorProjectionProofs.lean:12:0: 'ErrorProjectionProofs.ascii_error_exact' depends on axioms: [propext, Quot.sound]
info: ErrorProjectionProofs.lean:13:0: 'ErrorProjectionProofs.into_source_exact' depends on axioms: [propext, Quot.sound]
ℹ [1806/1809] Built CharForwardProofs (2.8s)
info: CharForwardProofs.lean:9:0: 'CharForwardProofs.from_ascii_exact' depends on axioms: [propext, Quot.sound]
info: CharForwardProofs.lean:10:0: 'CharForwardProofs.from_ascii_return' depends on axioms: [propext, Quot.sound]
ℹ [1807/1809] Built BorrowViewProofs (3.1s)
info: BorrowViewProofs.lean:23:0: 'BorrowViewProofs.as_ref_slice_exact' depends on axioms: [propext, Quot.sound]
info: BorrowViewProofs.lean:24:0: 'BorrowViewProofs.as_ref_self_exact' depends on axioms: [propext, Quot.sound]
info: BorrowViewProofs.lean:25:0: 'BorrowViewProofs.as_mut_slice_contract' depends on axioms: [propext, Quot.sound]
⚠ [1808/1809] Built DigitProofs (47s)
warning: DigitProofs.lean:145:16: Local variable 'c' resembles constructor 'ascii.ascii_char.AsciiChar.c' - write '.c' (with a dot) or 'ascii.ascii_char.AsciiChar.c' to use the constructor.

Note: This linter can be disabled with `set_option linter.constructorNameAsVariable false`
warning: DigitProofs.lean:152:18: Local variable 'c' resembles constructor 'ascii.ascii_char.AsciiChar.c' - write '.c' (with a dot) or 'ascii.ascii_char.AsciiChar.c' to use the constructor.

Note: This linter can be disabled with `set_option linter.constructorNameAsVariable false`
warning: DigitProofs.lean:157:31: Local variable 'c' resembles constructor 'ascii.ascii_char.AsciiChar.c' - write '.c' (with a dot) or 'ascii.ascii_char.AsciiChar.c' to use the constructor.

Note: This linter can be disabled with `set_option linter.constructorNameAsVariable false`
warning: DigitProofs.lean:165:39: Unused tactic linter: `<;>` should be replaced with `;` or be removed.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: DigitProofs.lean:165:43: Unused tactic linter: `scalar_tac` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: DigitProofs.lean:165:43: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: DigitProofs.lean:167:29: Local variable 'c' resembles constructor 'ascii.ascii_char.AsciiChar.c' - write '.c' (with a dot) or 'ascii.ascii_char.AsciiChar.c' to use the constructor.

Note: This linter can be disabled with `set_option linter.constructorNameAsVariable false`
info: DigitProofs.lean:175:0: 'DigitProofs.is_digit_success_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: DigitProofs.lean:176:0: 'DigitProofs.is_digit_panic_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [1809/1809] Built Proofs (53s)
warning: Proofs.lean:142:629: Unused tactic linter: `<;>` should be replaced with `;` or be removed.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:142:633: Unused tactic linter: `(simp only [UScalar.val, UScalarTy.U8_numBits_eq] <;> decide)` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:142:633: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Proofs.lean:144:629: Unused tactic linter: `<;>` should be replaced with `;` or be removed.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:144:633: Unused tactic linter: `(simp only [UScalar.val, UScalarTy.U8_numBits_eq] <;> decide)` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:144:633: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Proofs.lean:146:629: Unused tactic linter: `<;>` should be replaced with `;` or be removed.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:146:633: Unused tactic linter: `(simp only [UScalar.val, UScalarTy.U8_numBits_eq] <;> decide)` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:146:633: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Proofs.lean:148:629: Unused tactic linter: `<;>` should be replaced with `;` or be removed.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:148:633: Unused tactic linter: `(simp only [UScalar.val, UScalarTy.U8_numBits_eq] <;> decide)` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:148:633: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Proofs.lean:150:629: Unused tactic linter: `<;>` should be replaced with `;` or be removed.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:150:633: Unused tactic linter: `(simp only [UScalar.val, UScalarTy.U8_numBits_eq] <;> decide)` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:150:633: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Proofs.lean:152:629: Unused tactic linter: `<;>` should be replaced with `;` or be removed.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:152:633: Unused tactic linter: `(simp only [UScalar.val, UScalarTy.U8_numBits_eq] <;> decide)` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:152:633: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Proofs.lean:154:629: Unused tactic linter: `<;>` should be replaced with `;` or be removed.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:154:633: Unused tactic linter: `(simp only [UScalar.val, UScalarTy.U8_numBits_eq] <;> decide)` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:154:633: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Proofs.lean:159:33: Unused tactic linter: `<;>` should be replaced with `;` or be removed.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:159:37: Unused tactic linter: `(simp only [UScalar.val, UScalarTy.U8_numBits_eq] <;> decide)` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:159:37: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Proofs.lean:161:629: Unused tactic linter: `<;>` should be replaced with `;` or be removed.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:161:633: Unused tactic linter: `(simp only [UScalar.val, UScalarTy.U8_numBits_eq] <;> decide)` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:161:633: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Proofs.lean:163:629: Unused tactic linter: `<;>` should be replaced with `;` or be removed.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:163:633: Unused tactic linter: `(simp only [UScalar.val, UScalarTy.U8_numBits_eq] <;> decide)` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:163:633: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Proofs.lean:165:629: Unused tactic linter: `<;>` should be replaced with `;` or be removed.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:165:633: Unused tactic linter: `(simp only [UScalar.val, UScalarTy.U8_numBits_eq] <;> decide)` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:165:633: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Proofs.lean:167:629: Unused tactic linter: `<;>` should be replaced with `;` or be removed.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:167:633: Unused tactic linter: `(simp only [UScalar.val, UScalarTy.U8_numBits_eq] <;> decide)` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Proofs.lean:167:633: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Proofs.lean:190:3: Unused tactic linter: `exact hprop` does nothing.

Note: This linter can be disabled with `set_option linter.unusedTactic false`
info: Proofs.lean:227:0: 'Proofs.as_byte_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:228:0: 'Proofs.is_ascii_blank_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:229:0: 'Proofs.is_ascii_digit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:230:0: 'Proofs.is_ascii_whitespace_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:231:0: 'Proofs.is_ascii_control_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:232:0: 'Proofs.is_ascii_alphabetic_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:233:0: 'Proofs.is_ascii_alphanumeric_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:234:0: 'Proofs.is_ascii_graphic_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:235:0: 'Proofs.is_ascii_printable_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:236:0: 'Proofs.is_ascii_lowercase_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:237:0: 'Proofs.is_ascii_uppercase_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:238:0: 'Proofs.is_ascii_hexdigit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:239:0: 'Proofs.eq_ignore_ascii_case_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:240:0: 'Proofs.to_ascii_char_identity_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:241:0: 'Proofs.to_ascii_char_unchecked_identity_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:242:0: 'Proofs.caseEqBits' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:243:0: 'Proofs.is_alphabetic_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:244:0: 'Proofs.is_alphanumeric_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:245:0: 'Proofs.is_lowercase_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:246:0: 'Proofs.is_uppercase_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:247:0: 'Proofs.is_whitespace_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:249:0: 'Proofs.is_digit_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:251:0: 'Proofs.is_ascii_punctuation_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:252:0: 'Proofs.default_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:253:0: 'Proofs.valid_up_to_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:255:0: 'StringProofs.new_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:256:0: 'StringProofs.len_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:257:0: 'StringProofs.is_empty_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:258:0: 'StringProofs.push_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:259:0: 'StringProofs.push_maximum_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:260:0: 'StringProofs.push_full_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:262:0: 'SliceProofs.as_slice_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:263:0: 'SliceProofs.as_mut_slice_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:264:0: 'SliceProofs.len_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:265:0: 'SliceProofs.is_empty_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Proofs.lean:267:0: 'SliceProofs.as_ascii_str_identity_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:268:0: 'SliceProofs.as_ascii_str_unchecked_identity_spec' depends on axioms: [propext, Quot.sound]
info: Proofs.lean:269:0: 'SliceProofs.as_mut_ascii_str_unchecked_identity_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
Build completed successfully (1809 jobs).

$ lake env lean --stdin (proofs.rs theorem/axiom audit)
proofs.rs:checked:Proofs.is_ascii_blank_spec
proofs.rs:checked:Proofs.is_ascii_digit_spec
proofs.rs:checked:Proofs.is_ascii_whitespace_spec
proofs.rs:checked:Proofs.is_ascii_control_spec
proofs.rs:checked:Proofs.is_ascii_alphabetic_spec
proofs.rs:checked:Proofs.is_ascii_alphanumeric_spec
proofs.rs:checked:Proofs.is_ascii_graphic_spec
proofs.rs:checked:Proofs.is_ascii_printable_spec
proofs.rs:checked:Proofs.is_ascii_lowercase_spec
proofs.rs:checked:Proofs.is_ascii_uppercase_spec
proofs.rs:checked:Proofs.is_ascii_hexdigit_spec
proofs.rs:checked:Proofs.as_byte_spec
proofs.rs:checked:Proofs.eq_ignore_ascii_case_spec
proofs.rs:checked:Proofs.to_ascii_char_identity_spec
proofs.rs:checked:Proofs.to_ascii_char_unchecked_identity_spec
proofs.rs:checked:Proofs.is_alphabetic_spec
proofs.rs:checked:Proofs.is_alphanumeric_spec
proofs.rs:checked:Proofs.is_lowercase_spec
proofs.rs:checked:Proofs.is_uppercase_spec
proofs.rs:checked:Proofs.is_whitespace_spec
proofs.rs:checked:Proofs.is_digit_spec
proofs.rs:checked:Proofs.is_ascii_punctuation_spec
proofs.rs:checked:Proofs.default_spec
proofs.rs:checked:Proofs.valid_up_to_spec
proofs.rs:checked:StringProofs.new_spec
proofs.rs:checked:StringProofs.len_spec
proofs.rs:checked:StringProofs.is_empty_spec
proofs.rs:checked:StringProofs.push_full_spec
proofs.rs:checked:SliceProofs.as_slice_spec
proofs.rs:checked:SliceProofs.as_mut_slice_spec
proofs.rs:checked:SliceProofs.len_spec
proofs.rs:checked:SliceProofs.is_empty_spec
proofs.rs:checked:SliceProofs.as_ascii_str_identity_spec
proofs.rs:checked:SliceProofs.as_ascii_str_unchecked_identity_spec
proofs.rs:checked:SliceProofs.as_mut_ascii_str_unchecked_identity_spec
proofs.rs:checked:ErrorProjectionProofs.ascii_error_exact
proofs.rs:checked:ErrorProjectionProofs.into_source_exact
proofs.rs:checked:VectorIdentityProofs.from_vector_exact
proofs.rs:checked:VectorIdentityProofs.into_vector_exact
proofs.rs:checked:VectorIdentityProofs.checked_exact
proofs.rs:checked:VectorIdentityProofs.unchecked_exact
proofs.rs:checked:BorrowViewProofs.as_ref_slice_exact
proofs.rs:checked:BorrowViewProofs.as_mut_slice_contract
proofs.rs:checked:BorrowViewProofs.as_ref_self_exact
proofs.rs:checked:StringBorrowViewProofs.as_ref_slice_exact
proofs.rs:checked:StringBorrowViewProofs.as_mut_slice_contract
proofs.rs:checked:SelfBorrowProofs.as_mut_self_exact
proofs.rs:checked:ErrorDescriptionProofs.char_description_exact
proofs.rs:checked:ErrorDescriptionProofs.str_description_exact
proofs.rs:checked:CharForwardProofs.from_ascii_exact
proofs.rs:checked:GenericErrorProofs.description_exact

=== stderr ===
info: aeneas: materializing new dependency
info: aeneas: fetching revision 'be86ab0f1989d04944292b345b24c435be3ad10a' from https://github.com/AeneasVerif/aeneas
info: aeneas: checking out revision 'be86ab0f1989d04944292b345b24c435be3ad10a'
info: mathlib: materializing new dependency
info: mathlib: fetching revision '56a005855ea17e0b0958f73ec801ae140b0a1679' from https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision '56a005855ea17e0b0958f73ec801ae140b0a1679'
info: plausible: materializing new dependency
info: plausible: fetching revision 'dfa4f38190d07c37e315953e08b90fe2d95b3c24' from https://github.com/leanprover-community/plausible
info: plausible: checking out revision 'dfa4f38190d07c37e315953e08b90fe2d95b3c24'
info: LeanSearchClient: materializing new dependency
info: LeanSearchClient: fetching revision 'd6b4c7be5be75ec4917c873ac50c756dc1436372' from https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision 'd6b4c7be5be75ec4917c873ac50c756dc1436372'
info: importGraph: materializing new dependency
info: importGraph: fetching revision 'a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93' from https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision 'a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93'
info: proofwidgets: materializing new dependency
info: proofwidgets: fetching revision 'df72b022e558978a1c50264cfc4d7fec86fa8e04' from https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision 'df72b022e558978a1c50264cfc4d7fec86fa8e04'
info: aesop: materializing new dependency
info: aesop: fetching revision '4a174c490d8707121c4a9290800489f105d85e07' from https://github.com/leanprover-community/aesop
info: aesop: checking out revision '4a174c490d8707121c4a9290800489f105d85e07'
info: Qq: materializing new dependency
info: Qq: fetching revision 'dce0ad79c486cb1fb504af04f953c3466b0c6db8' from https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'dce0ad79c486cb1fb504af04f953c3466b0c6db8'
info: batteries: materializing new dependency
info: batteries: fetching revision '66e469188fe07963e5cf666c7d4433f45b8131c5' from https://github.com/leanprover-community/batteries
info: batteries: checking out revision '66e469188fe07963e5cf666c7d4433f45b8131c5'
info: Cli: materializing new dependency
info: Cli: fetching revision 'c24fe6078c630e89b489bffe59b3e20ac30d12c8' from https://github.com/leanprover/lean4-cli
info: Cli: checking out revision 'c24fe6078c630e89b489bffe59b3e20ac30d12c8'