Run locally
git clone -- https://github.com/keiichiw/crate-proofs report-11-source-1
git -C report-11-source-1 checkout --detach d0358890f8bdc8e72a376d225667ac162f89e3b8
git -C report-11-source-1 submodule update --init --recursive --checkout
cd report-11-source-1/crc/3.4.0/aeneas/profiles/default/proofs
lake build +CrcProofs.Table +CrcProofs.TableCloneFrom
printf '%s' 'import Aeneas
import CrcProofs.Table
import CrcProofs.TableCloneFrom
set_option pp.all true
set_option pp.universes true
set_option pp.explicit true
set_option pp.fullNames true
set_option pp.notation false
set_option pp.proofs true
set_option pp.deepTerms true
set_option pp.maxSteps 10000000
-- proofs.rs adapter for Lean 4.35.0 / Aeneas be86ab0f.
-- Uses Lean'\''s environment, Meta telescope and pretty-printer, never source parsing.
open Lean Meta Elab Command
namespace ProofsProbe
meta def moduleOf (env : Environment) (n : Name) : String :=
match env.getModuleIdxFor? n with
| some idx => env.header.moduleNames[idx.toNat]!.toString
| none => ""
meta def pretty (e : Expr) : MetaM String := do
let s := (← ppExpr e).pretty
if s.contains '\''⋯'\'' then
throwError "Lean display contains an omission marker (or literal ⋯); refusing an incomplete proposition"
if s.utf8ByteSize > 1000000 then throwError "Proposition exceeds 1,000,000-byte recording limit"
return s
-- The full statement stays explicit; the inspection view uses Lean notation.
meta def readable (e : Expr) : MetaM String :=
withOptions (fun o =>
let o := o.setBool `pp.all false
let o := o.setBool `pp.explicit false
let o := o.setBool `pp.universes false
o.setBool `pp.notation true) (pretty e)
-- Only a constant'\''s own tag grants a link; names in plain text are never guessed.
partial def segments (code : Widget.CodeWithInfos) (ref : Option Name := none) : Array Json :=
match code with
| .text text => #[Json.mkObj (([("text", toJson text)]) ++
(ref.toList.map fun n => ("ref", toJson n.toString)))]
| .append parts => parts.foldl (fun acc part => acc ++ segments part ref) #[]
| .tag info part =>
let ref := match info.info.val.info with
| .ofTermInfo ti => ti.expr.constName?
| _ => none
segments part ref
meta def readableFields (key : String) (e : Expr) : MetaM (List (String × Json)) := do
let text ← readable e
let base := [(key, toJson text)]
try
let code ← withOptions (fun o =>
let o := o.setBool `pp.all false
let o := o.setBool `pp.explicit false
let o := o.setBool `pp.universes false
let o := o.setBool `pp.notation true
o.setBool `pp.tagAppFns true) (Widget.ppExprTagged e)
let parts := segments code
let joined := String.join (parts.toList.map fun j =>
(j.getObjValAs? String "text").toOption.getD "")
if joined != text || parts.size > 10000 || joined.utf8ByteSize > 1000000 then
return base
return base ++ [(key ++ "_segments", toJson parts)]
catch _ => return base
meta def inspect (n : Name) (ty : Expr) (manual : Bool) : MetaM (Option Json) := do
let env ← getEnv
forallTelescope ty fun xs conclusion => do
let programExpr ← try
let normalized ← Aeneas.Utils.normalizeLetBindings conclusion
let (expr, _) ← Aeneas.Step.getStepSpecFunArgsExpr normalized
pure (some expr)
catch _ => pure none
if programExpr.isNone && !manual then return none
let full ← pretty ty
let program ← match programExpr with
| some expr => pure (toJson (← readable expr))
| none => pure Json.null
let head := toJson (programExpr.bind (·.getAppFn.constName?) |>.map Name.toString)
let mut binders := #[]
for x in xs do
let d ← x.fvarId!.getDecl
let prop ← isProp d.type
binders := binders.push (Json.mkObj ((← readableFields "type" d.type) ++ [
("name", toJson d.userName.toString),
("kind", toJson (if d.binderInfo.isInstImplicit then "instance" else if prop then "hypothesis" else "variable")),
("binder", toJson (if d.binderInfo.isInstImplicit then "instance" else if d.binderInfo.isExplicit then "explicit" else "implicit"))]))
if binders.size > 1000 then throwError "More than 1000 binders"
let some ranges ← findDeclarationRanges? n | throwError "Missing theorem source range: {n}"
let axioms ← Lean.collectAxioms n
let constants := ty.getUsedConstants
let mut definitions := #[]
for nm in constants.extract 0 100 do
let ranges ← findDeclarationRanges? nm
definitions := definitions.push (Json.mkObj [
("name", toJson nm.toString), ("module", toJson (moduleOf env nm)),
("source", match ranges with
| some r => Json.mkObj [("first_line", toJson r.range.pos.line), ("last_line", toJson r.range.endPos.line)]
| none => Json.null)])
return some (Json.mkObj ((← readableFields "conclusion" conclusion) ++ [
("version", toJson (1 : Nat)), ("theorem", toJson n.toString),
("module", toJson (moduleOf env n)), ("statement", toJson full),
("binders", toJson binders),
("program", program), ("program_head", head),
("axioms", toJson (axioms.map Name.toString)),
("first_line", toJson ranges.range.pos.line), ("last_line", toJson ranges.range.endPos.line),
("definitions", toJson definitions), ("definitions_truncated", toJson (decide (constants.size > 100))),
("translation_rerun", toJson false)]))
end ProofsProbe
run_cmd do
let manual : Array Name := #[`CrcProofs.table_u8_l0_spec, `CrcProofs.table_u8_l1_spec, `CrcProofs.table_u8_l16_spec, `CrcProofs.table_u16_l0_spec, `CrcProofs.table_u16_l1_spec, `CrcProofs.table_u16_l16_spec, `CrcProofs.table_u32_l0_spec, `CrcProofs.table_u32_l1_spec, `CrcProofs.table_u32_l16_spec, `CrcProofs.table_u64_l0_spec, `CrcProofs.table_u64_l1_spec, `CrcProofs.table_u64_l16_spec, `CrcProofs.table_u128_l0_spec, `CrcProofs.table_u128_l1_spec, `CrcProofs.table_u128_l16_spec, `CrcProofs.table_clone_l0_spec, `CrcProofs.table_clone_from_l0_spec, `CrcProofs.table_clone_l1_spec, `CrcProofs.table_clone_from_l1_spec, `CrcProofs.table_clone_l16_spec, `CrcProofs.table_clone_from_l16_spec]
let localModules : Array String := #[]
let roots : Array Name := #[]
let env ← getEnv
let mut closure : Array Name := #[]
let mut pending := roots.toList
while !pending.isEmpty do
let m := pending.head!
pending := pending.tail!
if !closure.contains m then
closure := closure.push m
if let some idx := env.header.moduleNames.findIdx? (· == m) then
pending := (env.header.moduleData[idx]!.imports.toList.map (·.module)) ++ pending
let scope := closure.filter (fun m => localModules.contains m.toString)
for n in manual do
match env.find? n with
| some (.thmInfo _) => pure ()
| _ => throwError "Expected a theorem: {n}"
for (n, ci) in env.constants.toList do
let explicit := manual.contains n
if explicit || scope.contains (ProofsProbe.moduleOf env n).toName then
if let .thmInfo th := ci then
let result ← liftTermElabM <| ProofsProbe.inspect n th.type explicit
if let some value := result then
liftIO <| IO.println ("proofs.rs:formal:" ++ value.compress)
run_cmd do
let theorem_name := `CrcProofs.table_u128_l0_spec
match (← getEnv).find? theorem_name with
| some (.thmInfo _) => pure ()
| _ => throwError "Expected a theorem: CrcProofs.table_u128_l0_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 CrcProofs.table_u128_l0_spec: {ax}"
liftIO <| IO.println "proofs.rs:checked:CrcProofs.table_u128_l0_spec"
run_cmd do
let theorem_name := `CrcProofs.table_u128_l16_spec
match (← getEnv).find? theorem_name with
| some (.thmInfo _) => pure ()
| _ => throwError "Expected a theorem: CrcProofs.table_u128_l16_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 CrcProofs.table_u128_l16_spec: {ax}"
liftIO <| IO.println "proofs.rs:checked:CrcProofs.table_u128_l16_spec"
run_cmd do
let theorem_name := `CrcProofs.table_u128_l1_spec
match (← getEnv).find? theorem_name with
| some (.thmInfo _) => pure ()
| _ => throwError "Expected a theorem: CrcProofs.table_u128_l1_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 CrcProofs.table_u128_l1_spec: {ax}"
liftIO <| IO.println "proofs.rs:checked:CrcProofs.table_u128_l1_spec"
run_cmd do
let theorem_name := `CrcProofs.table_u16_l0_spec
match (← getEnv).find? theorem_name with
| some (.thmInfo _) => pure ()
| _ => throwError "Expected a theorem: CrcProofs.table_u16_l0_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 CrcProofs.table_u16_l0_spec: {ax}"
liftIO <| IO.println "proofs.rs:checked:CrcProofs.table_u16_l0_spec"
run_cmd do
let theorem_name := `CrcProofs.table_u16_l16_spec
match (← getEnv).find? theorem_name with
| some (.thmInfo _) => pure ()
| _ => throwError "Expected a theorem: CrcProofs.table_u16_l16_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 CrcProofs.table_u16_l16_spec: {ax}"
liftIO <| IO.println "proofs.rs:checked:CrcProofs.table_u16_l16_spec"
run_cmd do
let theorem_name := `CrcProofs.table_u16_l1_spec
match (← getEnv).find? theorem_name with
| some (.thmInfo _) => pure ()
| _ => throwError "Expected a theorem: CrcProofs.table_u16_l1_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 CrcProofs.table_u16_l1_spec: {ax}"
liftIO <| IO.println "proofs.rs:checked:CrcProofs.table_u16_l1_spec"
run_cmd do
let theorem_name := `CrcProofs.table_u32_l0_spec
match (← getEnv).find? theorem_name with
| some (.thmInfo _) => pure ()
| _ => throwError "Expected a theorem: CrcProofs.table_u32_l0_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 CrcProofs.table_u32_l0_spec: {ax}"
liftIO <| IO.println "proofs.rs:checked:CrcProofs.table_u32_l0_spec"
run_cmd do
let theorem_name := `CrcProofs.table_u32_l16_spec
match (← getEnv).find? theorem_name with
| some (.thmInfo _) => pure ()
| _ => throwError "Expected a theorem: CrcProofs.table_u32_l16_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 CrcProofs.table_u32_l16_spec: {ax}"
liftIO <| IO.println "proofs.rs:checked:CrcProofs.table_u32_l16_spec"
run_cmd do
let theorem_name := `CrcProofs.table_u32_l1_spec
match (← getEnv).find? theorem_name with
| some (.thmInfo _) => pure ()
| _ => throwError "Expected a theorem: CrcProofs.table_u32_l1_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 CrcProofs.table_u32_l1_spec: {ax}"
liftIO <| IO.println "proofs.rs:checked:CrcProofs.table_u32_l1_spec"
run_cmd do
let theorem_name := `CrcProofs.table_u64_l0_spec
match (← getEnv).find? theorem_name with
| some (.thmInfo _) => pure ()
| _ => throwError "Expected a theorem: CrcProofs.table_u64_l0_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 CrcProofs.table_u64_l0_spec: {ax}"
liftIO <| IO.println "proofs.rs:checked:CrcProofs.table_u64_l0_spec"
run_cmd do
let theorem_name := `CrcProofs.table_u64_l16_spec
match (← getEnv).find? theorem_name with
| some (.thmInfo _) => pure ()
| _ => throwError "Expected a theorem: CrcProofs.table_u64_l16_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 CrcProofs.table_u64_l16_spec: {ax}"
liftIO <| IO.println "proofs.rs:checked:CrcProofs.table_u64_l16_spec"
run_cmd do
let theorem_name := `CrcProofs.table_u64_l1_spec
match (← getEnv).find? theorem_name with
| some (.thmInfo _) => pure ()
| _ => throwError "Expected a theorem: CrcProofs.table_u64_l1_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 CrcProofs.table_u64_l1_spec: {ax}"
liftIO <| IO.println "proofs.rs:checked:CrcProofs.table_u64_l1_spec"
run_cmd do
let theorem_name := `CrcProofs.table_u8_l0_spec
match (← getEnv).find? theorem_name with
| some (.thmInfo _) => pure ()
| _ => throwError "Expected a theorem: CrcProofs.table_u8_l0_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 CrcProofs.table_u8_l0_spec: {ax}"
liftIO <| IO.println "proofs.rs:checked:CrcProofs.table_u8_l0_spec"
run_cmd do
let theorem_name := `CrcProofs.table_u8_l16_spec
match (← getEnv).find? theorem_name with
| some (.thmInfo _) => pure ()
| _ => throwError "Expected a theorem: CrcProofs.table_u8_l16_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 CrcProofs.table_u8_l16_spec: {ax}"
liftIO <| IO.println "proofs.rs:checked:CrcProofs.table_u8_l16_spec"
run_cmd do
let theorem_name := `CrcProofs.table_u8_l1_spec
match (← getEnv).find? theorem_name with
| some (.thmInfo _) => pure ()
| _ => throwError "Expected a theorem: CrcProofs.table_u8_l1_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 CrcProofs.table_u8_l1_spec: {ax}"
liftIO <| IO.println "proofs.rs:checked:CrcProofs.table_u8_l1_spec"
run_cmd do
let theorem_name := `CrcProofs.table_clone_l0_spec
match (← getEnv).find? theorem_name with
| some (.thmInfo _) => pure ()
| _ => throwError "Expected a theorem: CrcProofs.table_clone_l0_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 CrcProofs.table_clone_l0_spec: {ax}"
liftIO <| IO.println "proofs.rs:checked:CrcProofs.table_clone_l0_spec"
run_cmd do
let theorem_name := `CrcProofs.table_clone_from_l0_spec
match (← getEnv).find? theorem_name with
| some (.thmInfo _) => pure ()
| _ => throwError "Expected a theorem: CrcProofs.table_clone_from_l0_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 CrcProofs.table_clone_from_l0_spec: {ax}"
liftIO <| IO.println "proofs.rs:checked:CrcProofs.table_clone_from_l0_spec"
run_cmd do
let theorem_name := `CrcProofs.table_clone_l16_spec
match (← getEnv).find? theorem_name with
| some (.thmInfo _) => pure ()
| _ => throwError "Expected a theorem: CrcProofs.table_clone_l16_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 CrcProofs.table_clone_l16_spec: {ax}"
liftIO <| IO.println "proofs.rs:checked:CrcProofs.table_clone_l16_spec"
run_cmd do
let theorem_name := `CrcProofs.table_clone_from_l16_spec
match (← getEnv).find? theorem_name with
| some (.thmInfo _) => pure ()
| _ => throwError "Expected a theorem: CrcProofs.table_clone_from_l16_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 CrcProofs.table_clone_from_l16_spec: {ax}"
liftIO <| IO.println "proofs.rs:checked:CrcProofs.table_clone_from_l16_spec"
run_cmd do
let theorem_name := `CrcProofs.table_clone_l1_spec
match (← getEnv).find? theorem_name with
| some (.thmInfo _) => pure ()
| _ => throwError "Expected a theorem: CrcProofs.table_clone_l1_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 CrcProofs.table_clone_l1_spec: {ax}"
liftIO <| IO.println "proofs.rs:checked:CrcProofs.table_clone_l1_spec"
run_cmd do
let theorem_name := `CrcProofs.table_clone_from_l1_spec
match (← getEnv).find? theorem_name with
| some (.thmInfo _) => pure ()
| _ => throwError "Expected a theorem: CrcProofs.table_clone_from_l1_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 CrcProofs.table_clone_from_l1_spec: {ax}"
liftIO <| IO.println "proofs.rs:checked:CrcProofs.table_clone_from_l1_spec"
' | lake env lean --stdinSource on GitHub · SARIF with logs (.json)
Recorded run
Completed · 21 checks passed · 0 failed
| Check | Result | Claim |
|---|---|---|
| Lean checked theorem CrcProofs.table_u128_l0_spec; axioms limited to propext, Classical.choice, Quot.sound | Passed | Claim #1 |
| Lean checked theorem CrcProofs.table_u128_l16_spec; axioms limited to propext, Classical.choice, Quot.sound | Passed | Claim #2 |
| Lean checked theorem CrcProofs.table_u128_l1_spec; axioms limited to propext, Classical.choice, Quot.sound | Passed | Claim #3 |
| Lean checked theorem CrcProofs.table_u16_l0_spec; axioms limited to propext, Classical.choice, Quot.sound | Passed | Claim #4 |
| Lean checked theorem CrcProofs.table_u16_l16_spec; axioms limited to propext, Classical.choice, Quot.sound | Passed | Claim #5 |
| Lean checked theorem CrcProofs.table_u16_l1_spec; axioms limited to propext, Classical.choice, Quot.sound | Passed | Claim #6 |
| Lean checked theorem CrcProofs.table_u32_l0_spec; axioms limited to propext, Classical.choice, Quot.sound | Passed | Claim #7 |
| Lean checked theorem CrcProofs.table_u32_l16_spec; axioms limited to propext, Classical.choice, Quot.sound | Passed | Claim #8 |
| Lean checked theorem CrcProofs.table_u32_l1_spec; axioms limited to propext, Classical.choice, Quot.sound | Passed | Claim #9 |
| Lean checked theorem CrcProofs.table_u64_l0_spec; axioms limited to propext, Classical.choice, Quot.sound | Passed | Claim #10 |
| Lean checked theorem CrcProofs.table_u64_l16_spec; axioms limited to propext, Classical.choice, Quot.sound | Passed | Claim #11 |
| Lean checked theorem CrcProofs.table_u64_l1_spec; axioms limited to propext, Classical.choice, Quot.sound | Passed | Claim #12 |
| Lean checked theorem CrcProofs.table_u8_l0_spec; axioms limited to propext, Classical.choice, Quot.sound | Passed | Claim #13 |
| Lean checked theorem CrcProofs.table_u8_l16_spec; axioms limited to propext, Classical.choice, Quot.sound | Passed | Claim #14 |
| Lean checked theorem CrcProofs.table_u8_l1_spec; axioms limited to propext, Classical.choice, Quot.sound | Passed | Claim #15 |
| Lean checked theorem CrcProofs.table_clone_l0_spec; axioms limited to propext, Classical.choice, Quot.sound | Passed | Claim #16 |
| Lean checked theorem CrcProofs.table_clone_from_l0_spec; axioms limited to propext, Classical.choice, Quot.sound | Passed | Claim #17 |
| Lean checked theorem CrcProofs.table_clone_l16_spec; axioms limited to propext, Classical.choice, Quot.sound | Passed | Claim #18 |
| Lean checked theorem CrcProofs.table_clone_from_l16_spec; axioms limited to propext, Classical.choice, Quot.sound | Passed | Claim #19 |
| Lean checked theorem CrcProofs.table_clone_l1_spec; axioms limited to propext, Classical.choice, Quot.sound | Passed | Claim #20 |
| Lean checked theorem CrcProofs.table_clone_from_l1_spec; axioms limited to propext, Classical.choice, Quot.sound | Passed | Claim #21 |
Execution details
- Started
- 2026-10-31T04:43:58.274671+00:00
- Finished
- 2026-10-31T04:57:57.563524+00:00
- Platform
- macos aarch64
- Rust compiler
- rustc 1.91.1 (ed61e7d7e 2025-11-07) binary: rustc commit-hash: ed61e7d7e242494fb7057f2657300d9e77bb4fcb commit-date: 2025-11-07 host: aarch64-apple-darwin release: 1.91.1 LLVM version: 21.1.2
- Working directory
- crc/3.4.0/aeneas/profiles/default/proofs
- Environment overrides
- None recorded
- Git repository
- https://github.com/keiichiw/crate-proofs
- Git commit
- d0358890f8bdc8e72a376d225667ac162f89e3b8
Diagnostics & logs
=== stdout ===
⚠ [2/11] Ran aeneas:extraDep
warning: building from source; failed to fetch GitHub release (run with '-v' for details)
✔ [4/67] Built AeneasMeta.Simp.RegisterCommand (1.0s)
✔ [5/69] Built Aeneas.Data.Coinductive.Effect (917ms)
✔ [8/73] Built AeneasMeta.BvEnumToBitVec (1.3s)
✔ [9/73] Built Aeneas.Tactic.Solver.Grind.Attribute (1.0s)
✔ [10/74] Built AeneasMeta.Simp.RegisterCommand:c.o (479ms)
✔ [11/75] Built AeneasMeta.Simp.RegisterCommand:dynlib (235ms)
✔ [12/79] Built AeneasMeta.BvEnumToBitVec:c.o (532ms)
✔ [13/79] Built Qq.ForLean.ToExpr (701ms)
✔ [14/83] Built Qq.ForLean.ReduceEval (749ms)
✔ [15/83] Built Qq.Typ (708ms)
✔ [16/83] Built AeneasMeta.BvEnumToBitVec:dynlib (244ms)
✔ [17/83] Built AeneasMeta.OptionConfig (2.3s)
✔ [18/87] Built Qq.ForLean.Do (674ms)
✔ [19/87] Built Qq.SortLocalDecls (590ms)
✔ [24/95] Built Aeneas.Std.Global (3.2s)
✔ [25/95] Built AeneasMeta.UtilsCore (3.2s)
✔ [26/95] Built AeneasMeta.UtilsCore:c.o (141ms)
✔ [27/95] Built Batteries.Util.LibraryNote (732ms)
✔ [28/98] Built AeneasMeta.UtilsCore:dynlib (137ms)
✔ [29/98] Built Batteries.Tactic.Lint.Basic (927ms)
✔ [30/98] Built ImportGraph.Lean.Syntax (534ms)
✔ [31/101] Built Aeneas.Tactic.Solver.Grind.Init (2.2s)
✔ [32/101] Built Batteries.CodeAction.Deprecated (1.1s)
✔ [33/101] Built ImportGraph.Lean.MessageData (541ms)
✔ [34/101] Built ImportGraph.Shake.Core (682ms)
✔ [35/102] Built ImportGraph.Lean.EnvExtension (588ms)
✔ [36/102] Built AeneasMeta.OptionConfig:c.o (1.0s)
✔ [37/105] Built Batteries.Tactic.Lint.Misc (911ms)
✔ [38/105] Built AeneasMeta.OptionConfig:dynlib (150ms)
✔ [39/105] Built Aeneas.Data.Coinductive.CoInd (4.6s)
✔ [40/112] Built Batteries.Tactic.HelpCmd (1.7s)
✔ [41/112] Built ImportGraph.Shake.EnvExtension (636ms)
✔ [42/112] Built ImportGraph.Lean.Json (722ms)
✔ [43/116] Built ImportGraph.Imports.Pretty (1.5s)
✔ [44/117] Built ImportGraph.Shake.Basic (1.1s)
✔ [45/117] Built ImportGraph.Util.Modules (619ms)
✔ [46/119] Built Batteries.Tactic.Alias (1.7s)
✔ [47/119] Built ImportGraph.Imports.ImportGraph (582ms)
✔ [48/119] Built ImportGraph.Lean.Environment (561ms)
✔ [49/120] Built ImportGraph.Graph.TransitiveClosure (569ms)
✔ [50/120] Built Qq.Macro (4.0s)
✔ [51/120] Built ImportGraph.WorkspaceModel.Base (913ms)
✔ [52/120] Built ImportGraph.Widget.Collapsible (922ms)
✔ [53/122] Built Aeneas.Data.Coinductive.ITree (1.4s)
✔ [54/122] Built ImportGraph.Shake.Algebra (793ms)
✔ [55/122] Built ImportGraph.Widget.Copy (817ms)
✔ [56/122] Built ImportGraph.Widget.GoToModule (918ms)
✔ [57/125] Built ImportGraph.Imports.RequiredModules (764ms)
✔ [58/130] Built ImportGraph.Tools.ImportDiff (860ms)
✔ [59/133] Built ImportGraph.WorkspaceModel.Summary.Core (639ms)
✔ [60/133] Built ImportGraph.Imports.Redundant (526ms)
✔ [61/134] Built Qq.Commands (1.0s)
✔ [62/134] Built ImportGraph.Imports.FromSource (580ms)
✔ [63/134] Built Qq.Delab (1.2s)
✔ [64/149] Built ImportGraph.WorkspaceModel.Model (1.1s)
✔ [65/152] Built ImportGraph.WorkspaceModel.Summary.Cache (519ms)
✔ [66/152] Built Batteries.Util.ProofWanted (2.9s)
✔ [67/160] Built ImportGraph.Tools.RedundantImports (747ms)
✔ [68/160] Built Batteries.Lean.Position (512ms)
✔ [69/171] Built ImportGraph.Tools.MinImports (798ms)
✔ [70/172] Built Mathlib.Tactic.Linter.DirectoryDependency (1.1s)
✔ [71/174] Built ImportGraph.Shake.DeclNeeds (2.9s)
✔ [72/176] Built Qq.MetaM (887ms)
✔ [73/176] Built ImportGraph.WorkspaceModel.Summary.Get (589ms)
✔ [74/176] Built Batteries.Tactic.Lint.TypeClass (722ms)
✔ [75/180] Built Batteries.Tactic.Lint.Simp (1.3s)
✔ [76/180] Built Batteries.Tactic.Unreachable (795ms)
✔ [77/180] Built Batteries.Lean.Meta.Inaccessible (647ms)
✔ [78/180] Built ImportGraph.WorkspaceModel.Summary (548ms)
✔ [79/180] Built Qq.Simp (652ms)
✔ [80/180] Built Qq.MatchImpl (852ms)
✔ [81/180] Built Aeneas.Data.Coinductive.ITreeWP.EffectWP (477ms)
✔ [82/181] Built AeneasMeta.Utils (5.9s)
✔ [83/181] Built Batteries.Tactic.Lint.Frontend (1.5s)
✔ [84/184] Built Qq.AssertInstancesCommute (1.2s)
✔ [85/187] Built Mathlib.Tactic.Linter.Header (1.5s)
✔ [86/187] Built ImportGraph.WorkspaceModel.Build (936ms)
✔ [87/187] Built ImportGraph.Shake.Environment (1.5s)
✔ [88/187] Built Batteries.Tactic.Lint (663ms)
✔ [89/187] Built Aeneas.Tactic.Step.Trace (1.3s)
✔ [90/187] Built Batteries.Logic (803ms)
✔ [91/187] Built Batteries.Lean.NameMapAttribute (684ms)
✔ [92/187] Built Mathlib.Tactic.TypeStar (776ms)
✔ [93/187] Built Mathlib.Util.ParseCommand (775ms)
✔ [94/187] Built Mathlib.Util.CodeActions.BinderPlicity (1.0s)
✔ [95/187] Built Mathlib.Lean.Elab.Tactic.Meta (798ms)
✔ [96/187] Built Mathlib.Tactic.Linter.UnusedTacticExtension (689ms)
✔ [97/187] Built Mathlib.Tactic.MinImports (1.1s)
✔ [98/187] Built Mathlib.Tactic.Linter.PrivateModule (703ms)
✔ [99/187] Built Mathlib.Tactic.Linter.TacticDocumentation (770ms)
✔ [100/187] Built Mathlib.Tactic.Linter.Whitespace (1.2s)
✔ [101/187] Built Mathlib.Tactic.Linter.OldObtain (856ms)
✔ [102/187] Built Batteries.Tactic.Trans (2.0s)
✔ [103/187] Built Mathlib.Tactic.DeclarationNames (730ms)
✔ [104/187] Built Mathlib.Tactic.Linter.Multigoal (863ms)
✔ [105/187] Built Mathlib.Tactic.Linter.InternalConstructor (837ms)
✔ [106/187] Built Mathlib.Tactic.Linter.HaveILetI (895ms)
✔ [107/187] Built Mathlib.Tactic.Linter.HashCommandLinter (1000ms)
✔ [108/187] Built Qq.Match (3.3s)
✔ [109/187] Built Mathlib.Tactic.Linter.EmptyLine (1.1s)
✔ [110/187] Built Mathlib.Tactic.Linter.DocString (1.4s)
✔ [111/187] Built Mathlib.Tactic.Linter.DeprecatedSyntaxLinter (1.3s)
✔ [112/189] Built Mathlib.Lean.Environment (987ms)
✔ [113/189] Built Mathlib.Tactic.Linter.DocPrime (1.7s)
✔ [114/189] Built Mathlib.Tactic.Linter.AuxLemma (1.0s)
✔ [115/189] Built Mathlib.Lean.Expr.Basic (1.4s)
✔ [116/189] Built Mathlib.Lean.Linter (698ms)
✔ [117/189] Built Mathlib.Tactic.Lemma (1.1s)
✔ [118/189] Built Mathlib.Tactic.AdaptationNote (1.2s)
✔ [119/189] Built Mathlib.Tactic.Linter.FlexibleLinter (2.3s)
✔ [120/190] Built ImportGraph.Tools.NormImports (923ms)
✔ [121/219] Built Mathlib.Util.CodeActions (776ms)
✔ [122/221] Built Mathlib.Lean.ContextInfo (1.0s)
✔ [123/223] Built Qq (777ms)
✔ [124/238] Built Mathlib.Tactic.Linter.Lint (1.0s)
✔ [125/250] Built Mathlib.Tactic.Linter.UnusedTactic (1.3s)
✔ [126/251] Built ImportGraph.Shake.Workspace (1.8s)
✔ [127/260] Built Mathlib.Lean.Elab.InfoTree (1.2s)
✔ [128/260] Built Mathlib.Tactic.ExtractGoal (1.7s)
✔ [129/260] Built Batteries.Lean.Syntax (544ms)
✔ [130/260] Built Mathlib.Tactic.TacticAnalysis (1.3s)
✔ [131/260] Built Batteries.Tactic.Init (1.6s)
✔ [132/260] Built Batteries.Util.ExtendedBinder (1.1s)
✔ [133/260] Built Batteries.Lean.Expr (947ms)
✔ [136/267] Built Mathlib.Tactic.Linter.Style (2.3s)
✔ [137/267] Built Batteries.Linter.UnreachableTactic (999ms)
✔ [138/273] Built Mathlib.Tactic.Linter.UnusedInstancesInType (1.0s)
✔ [139/273] Built Aesop.Script.Tactic (549ms)
✔ [140/275] Built Batteries.Control.Lemmas (553ms)
✔ [141/275] Built Aesop.Script.GoalWithMVars (638ms)
✔ [142/281] Built Aesop.Nanos (679ms)
✔ [143/284] Built Aesop.Index.DiscrTreeConfig (650ms)
✔ [144/286] Built ImportGraph.Tools.FindHome (1.8s)
✔ [145/286] Built Batteries.Lean.MonadBacktrack (474ms)
✔ [146/286] Built Batteries.Control.AlternativeMonad (767ms)
✔ [147/293] Built Batteries.Tactic.PermuteGoals (1.1s)
✔ [148/293] Built Aesop.Check (643ms)
✔ [149/296] Built Batteries.Data.Array.Merge (1.4s)
✔ [150/296] Built ImportGraph.Tools (734ms)
✔ [151/296] Built Aesop.Rule.Name (812ms)
✔ [152/296] Built Aesop.Options.Public (724ms)
✔ [153/296] Built Batteries.Lean.Meta.Basic (631ms)
✔ [154/300] Built AeneasMeta.Utils:c.o (8.7s)
✔ [155/300] Built Aesop.Script.OptimizeSyntax (849ms)
✔ [156/300] Built Aesop.Forward.LevelIndex (649ms)
✔ [157/300] Built Aesop.Forward.PremiseIndex (641ms)
✔ [158/300] Built Aesop.Percent (486ms)
✔ [159/302] Built Mathlib.Tactic.Linter.OverlappingInstances (1.8s)
✔ [160/302] Built Mathlib.Tactic.TacticAnalysis.Declarations (2.5s)
✔ [161/302] Built Aesop.Util.UnorderedArraySet (639ms)
✔ [162/302] Built Aesop.Options.Internal (474ms)
✔ [163/303] Built AeneasMeta.Utils:dynlib (287ms)
✔ [164/311] Built Aesop.Script.TacticState (648ms)
✔ [165/311] Built Batteries.Lean.Meta.SavedState (728ms)
✔ [166/311] Built Aesop.Forward.SlotIndex (497ms)
✔ [167/322] Built Mathlib.Tactic.Linter.DeclType (747ms)
✔ [168/322] Built Aesop.Util.UnionFind (603ms)
✔ [169/323] Built Batteries.Lean.TagAttribute (564ms)
✔ [170/325] Built Aesop.RuleTac.RuleTerm (749ms)
✔ [171/329] Built Batteries.Tactic.SeqFocus (1.2s)
✔ [172/332] Built Aesop.ElabM (926ms)
✔ [173/334] Built Aesop.Util.EqualUpToIds (2.2s)
✔ [174/334] Built Batteries.Lean.AttributeExtra (878ms)
✔ [175/338] Built Aesop.Util.Basic (2.0s)
✔ [176/338] Built Aesop.Util.Tactic (701ms)
✔ [177/338] Built Mathlib.Init (1.5s)
✔ [178/338] Built Aesop.Util.Unfold (874ms)
✔ [179/338] Built Batteries.Lean.Meta.UnusedNames (736ms)
✔ [180/338] Built Aesop.Constants (669ms)
✔ [181/338] Built Aesop.RuleTac.ElabRuleTerm (1.1s)
✔ [182/338] Built AeneasMeta.Extensions (2.7s)
✔ [183/338] Built Aesop.RuleTac.Forward.Basic (1.0s)
✔ [184/338] Built AeneasMeta.Async.Async (2.9s)
✔ [185/338] Built Aesop.Script.CtorNames (1.1s)
✔ [186/338] Built Batteries.Linter.UnnecessarySeqFocus (1.5s)
✔ [187/338] Built AeneasMeta.Simp.Simp (3.3s)
✔ [188/338] Built Aesop.Script.Util (989ms)
✔ [189/338] Built Aesop.Tracing (1.4s)
✔ [190/338] Built Aesop.Forward.Substitution (1.5s)
✔ [191/338] Built Aesop.EMap (1.2s)
✔ [192/338] Built Mathlib.Lean.Elab.Term (1.1s)
✔ [193/338] Built Mathlib.Util.WithWeakNamespace (1.2s)
✔ [194/338] Built Mathlib.Tactic.Core (1.6s)
✔ [195/338] Built Mathlib.Tactic.ExtendDoc (1.2s)
✔ [196/338] Built Mathlib.Tactic.Inhabit (1.2s)
✔ [197/338] Built Mathlib.Tactic.SimpRw (1.5s)
✔ [198/338] Built Mathlib.Tactic.Use (1.8s)
✔ [199/338] Built Mathlib.Basic.Nonempty (1.1s)
✔ [200/338] Built Mathlib.Lean.PrettyPrinter.Delaborator (1.2s)
✔ [201/338] Built Mathlib.Basic.IsEmpty.Defs (1.1s)
✔ [202/338] Built Mathlib.Basic.ExistsUnique (1.3s)
✔ [203/338] Built Mathlib.Tactic.OfNat (1.0s)
✔ [204/338] Built Mathlib.Data.Int.Notation (1.1s)
✔ [205/338] Built Mathlib.Tactic.Simproc.ExistsAndEq (2.1s)
✔ [206/338] Built Mathlib.Tactic.Attr.Register (1.5s)
✔ [207/338] Built Mathlib.Data.Nat.Notation (1.2s)
✔ [208/338] Built Mathlib.Tactic.Push.Attr (1.4s)
✔ [209/338] Built Mathlib.Data.Nat.BinaryRec (1.5s)
✔ [210/338] Built Mathlib.Tactic.CrossRefAttribute (1.9s)
✔ [211/338] Built Mathlib.Lean.Meta (1.2s)
✔ [212/338] Built Mathlib.Tactic.Simps.NotationClass (1.5s)
✔ [213/338] Built Mathlib.Data.String.Defs (1.1s)
✔ [214/338] Built AeneasMeta.Extensions:c.o (377ms)
✔ [215/338] Built Mathlib.Util.AddRelatedDecl (2.0s)
✔ [216/338] Built Mathlib.Tactic.Eqns (1.2s)
✔ [217/338] Built Mathlib.Tactic.Translate.Attributes (1.1s)
✔ [218/338] Built AeneasMeta.Extensions:dynlib (219ms)
✔ [219/338] Built Mathlib.Lean.Name (1.3s)
✔ [220/338] Built Aesop.Util.Tactic.Unfold (1.1s)
✔ [221/338] Built Mathlib.Tactic.Translate.UnfoldBoundary (2.1s)
✔ [222/338] Built AeneasMeta.Async.Async:c.o (1.1s)
✔ [223/338] Built Mathlib.Lean.Meta.Simp (1.7s)
✔ [224/338] Built Aesop.RulePattern.Cache (900ms)
✔ [225/338] Built Batteries.Linter (1.0s)
✔ [226/338] Built Aesop.Index.Basic (1.3s)
✔ [227/339] Built AeneasMeta.Simp.Simp:c.o (1.8s)
✔ [228/339] Built Aesop.Util.Tactic.Ext (1.3s)
✔ [229/339] Built AeneasMeta.Simp.Simp:dynlib (170ms)
✔ [230/339] Built AeneasMeta.Async.Async:dynlib (191ms)
✔ [231/339] Built Aesop.Script.Step (1.5s)
✔ [232/339] Built Mathlib.Tactic.Translate.Reorder (3.5s)
✔ [233/339] Built Aesop.Stats.Basic (1.7s)
✔ [234/340] Built Mathlib.Basic.Nontrivial.Defs (1.5s)
✔ [235/340] Built Mathlib.Tactic.SplitIfs (1.7s)
✔ [236/340] Built Mathlib.Logic.Function.Defs (1.8s)
✔ [237/340] Built Mathlib.Tactic.Translate.GuessName (1.8s)
✔ [238/340] Built Aesop.Util.OrderedHashSet (818ms)
✔ [239/340] Built Batteries.Tactic.Basic (1.1s)
✔ [240/343] Built Mathlib.Tactic.ScopedNS (2.8s)
✔ [241/343] Built Aesop.Script.SScript (1.3s)
✔ [242/344] Built Mathlib.Tactic.MkIffOfInductiveProp (2.4s)
✔ [243/344] Built Aesop.Script.UScript (1.0s)
✔ [244/344] Built Batteries.Lean.Meta.Expr (910ms)
✔ [245/344] Built Aesop.BaseM (1.4s)
✔ [246/344] Built Mathlib.Basic.Logic.Basic (2.0s)
✔ [247/346] Built Batteries.Lean.PersistentHashMap (943ms)
✔ [248/346] Built Mathlib.Logic.Relator (1.9s)
✔ [249/347] Built AeneasMeta.Simp.SimpAllAssumptions (3.1s)
✔ [250/347] Built Batteries.Classes.Order (1.4s)
✔ [251/347] Built Aesop.Script.Check (819ms)
✔ [252/347] Built Batteries.Lean.Meta.InstantiateMVars (741ms)
✔ [253/347] Built AeneasMeta.Saturate.Attribute (4.6s)
✔ [254/347] Built Mathlib.Tactic.SetNotationForOrder (2.7s)
✔ [255/347] Built Aesop.Script.ScriptM (874ms)
✔ [256/349] Built Aesop.Script.UScriptToSScript (1.8s)
✔ [257/349] Built Batteries.Lean.PersistentHashSet (672ms)
✔ [258/349] Built Batteries.Lean.Meta.DiscrTree (625ms)
✔ [259/351] Built Mathlib.Tactic.Translate.Expr (3.4s)
✔ [260/351] Built Mathlib.Tactic.Simps.Basic (5.5s)
✔ [261/351] Built Aesop.RuleTac.GoalDiff (1.4s)
✔ [262/351] Built Aesop.RulePattern (2.0s)
✔ [263/355] Built Batteries.Data.UInt (1.2s)
✔ [264/355] Built AeneasMeta.Simp.SimpAllAssumptions:c.o (1.4s)
✔ [265/355] Built Aesop.RuleSet.Name (676ms)
✔ [266/355] Built Aesop.RuleTac.Basic (893ms)
✔ [267/355] Built AeneasMeta.Simp.SimpAllAssumptions:dynlib (168ms)
✔ [268/358] Built Aesop.Script.StructureStatic (1.3s)
✔ [269/359] Built Aesop.Script.StructureDynamic (1.9s)
✔ [270/359] Built Aesop.Index.RulePattern (1.5s)
✔ [271/366] Built Mathlib.Tactic.Simps (1.7s)
✔ [272/369] Built Aesop.Script.SpecificTactics (2.7s)
✔ [273/369] Built Batteries.Lean.HashSet (824ms)
✔ [274/369] Built Aesop.RuleSet.Filter (1.2s)
✔ [275/370] Built AeneasMeta.Saturate.Attribute:c.o (3.4s)
✔ [276/374] Built Aesop.Script.Main (1.3s)
✔ [277/374] Built Aesop.RuleTac.Preprocess (1.0s)
✔ [278/374] Built Aesop.Search.Expansion.Basic (1.1s)
✔ [279/374] Built Aesop.Search.Expansion.Simp (1.1s)
✔ [280/388] Built AeneasMeta.Saturate.Attribute:dynlib (271ms)
✔ [281/388] Built Aesop.RuleTac.Tactic (1.4s)
✔ [282/397] Built AeneasMeta.Simp (2.4s)
✔ [283/400] Built AeneasMeta.Simp:c.o (208ms)
✔ [284/400] Built AeneasMeta.Simp:dynlib (188ms)
✔ [285/400] Built Aesop.RuleTac.Cases (1.3s)
✔ [286/402] Built Aesop.Exception (763ms)
✔ [287/402] Built Batteries.Control.ForInStep.Basic (672ms)
✔ [288/421] Built Aesop.RuleTac.Apply (1.1s)
✔ [289/421] Built Batteries.Data.Array.Basic (3.9s)
✔ [290/421] Built Aesop.Stats.Extension (969ms)
✔ [291/436] Built Aesop.Stats.File (893ms)
✔ [292/436] Built Aesop.Frontend.Basic (719ms)
✔ [293/442] Built Mathlib.Util.Notation3 (7.8s)
✔ [294/443] Built Aesop.Stats.Report (1.3s)
✔ [295/446] Built Aesop.Forward.RuleInfo (1.7s)
✔ [296/446] Built Mathlib.Tactic.Attr.Core (1.5s)
✔ [297/451] Built Mathlib.Tactic.Spread (1.8s)
✔ [298/451] Built Mathlib.Tactic.Conv (1.0s)
✔ [299/451] Built AeneasMeta.Async.TestTactics (3.1s)
✔ [300/454] Built Aesop.Rule.Forward (807ms)
✔ [301/454] Built Mathlib.Tactic.Lift (1.5s)
✔ [302/454] Built AeneasMeta.Async.TestTactics:c.o (579ms)
✔ [303/454] Built AeneasMeta.Async.TestTactics:dynlib (233ms)
✔ [304/454] Built Mathlib.Tactic.Subsingleton (1.7s)
✔ [305/459] Built Mathlib.Tactic.Translate.Core (7.0s)
✔ [306/462] Built Aesop.Forward.Match.Types (984ms)
✔ [307/462] Built Mathlib.Tactic.DepRewrite (3.9s)
✔ [308/462] Built Mathlib.Util.AtLocation (1.7s)
✔ [309/463] Built Batteries.Data.BinomialHeap.Basic (5.8s)
✔ [310/463] Built Mathlib.Util.CompileInductive (2.0s)
✔ [311/463] Built Mathlib.Tactic.Relation.Rfl (1.9s)
✔ [312/468] Built Mathlib.Lean.Meta.CongrTheorems (2.9s)
✔ [313/468] Built Mathlib.Control.Combinators (1.7s)
✔ [314/468] Built Mathlib.Tactic.Translate.ToAdditive (2.0s)
✔ [315/468] Built Mathlib.Tactic.Translate.TagUnfoldBoundary (2.3s)
✔ [316/468] Built Aesop.RuleTac.Descr (898ms)
✔ [317/468] Built AeneasMeta.Saturate.Tactic (7.4s)
✔ [318/468] Built Mathlib.Data.Int.Init (2.7s)
✔ [319/468] Built Mathlib.Data.Option.Defs (1.3s)
✔ [320/468] Built Aesop.Index.Forward (1.2s)
✔ [321/473] Built Mathlib.Tactic.Coe (1.5s)
✔ [322/473] Built Aesop.Rule.Basic (1.3s)
✔ [323/473] Built Mathlib.Tactic.ToAdditive (1.8s)
✔ [324/475] Built Mathlib.Tactic.Push (3.2s)
✔ [325/475] Built Mathlib.Data.Ordering.Basic (1.9s)
✔ [326/476] Built Mathlib.Tactic.CongrExclamation (3.6s)
✔ [327/476] Built Aesop.Rule (1.2s)
✔ [328/478] Built Mathlib.Tactic.Translate.ToDual (2.9s)
✔ [329/478] Built Aesop.Index (1.7s)
✔ [330/478] Built Mathlib.Tactic.TermCongr (4.3s)
✔ [331/478] Built Mathlib.Tactic.FastInstance (2.7s)
✔ [332/478] Built Batteries.Data.Except (740ms)
✔ [333/478] Built Mathlib.Algebra.Regular.Defs (1.6s)
✔ [334/478] Built Mathlib.Algebra.Notation.Defs (2.0s)
✔ [335/480] Built Aesop.Tree.UnsafeQueue (923ms)
✔ [336/480] Built Mathlib.Tactic.Contrapose (1.7s)
✔ [337/480] Built Mathlib.Tactic.GCongr.ForwardAttr (1.5s)
✔ [338/480] Built Aesop.RuleSet.Member (1.2s)
✔ [339/487] Built Batteries.Tactic.Exact (926ms)
✔ [340/487] Built Batteries.Lean.Except (873ms)
✔ [341/489] Built Aesop.Forward.Match (2.1s)
✔ [342/490] Built Mathlib.Tactic.ToDual (1.9s)
✔ [343/490] Built Aesop.Builder.Basic (1.1s)
✔ [344/491] Built Mathlib.Tactic.Convert (3.2s)
✔ [345/491] Built Batteries.Data.MLList.Basic (1.5s)
✔ [346/491] Built Mathlib.Algebra.Notation.Pi.Defs (2.2s)
✔ [347/491] Built Aesop.Tree.Data.ForwardRuleMatches (1.2s)
✔ [348/491] Built Mathlib.Tactic.PPWithUniv (1.7s)
✔ [349/491] Built Mathlib.Algebra.Group.Semigroup (2.9s)
✔ [350/491] Built Mathlib.Logic.Function.ULift (1.5s)
✔ [351/493] Built Aesop.RuleTac.Forward (2.3s)
✔ [352/493] Built Mathlib.Order.Defs.Prop (1.6s)
✔ [353/493] Built Mathlib.Order.Notation (2.6s)
✔ [354/493] Built Aesop.Builder.Unfold (1.2s)
✔ [355/493] Built Mathlib.Data.Set.Defs (2.3s)
✔ [356/493] Built Mathlib.Tactic.ByCases (1.6s)
✔ [357/493] Built Mathlib.Order.Defs.PartialOrder (2.5s)
✔ [358/493] Built Aesop.Builder.Apply (1.2s)
✔ [359/493] Built Aesop.Builder.Tactic (1.1s)
✔ [360/493] Built Aesop.Builder.Constructors (1.1s)
✔ [361/493] Built Aesop.Builder.NormSimp (1.2s)
✔ [362/493] Built Aesop.Builder.Forward (2.2s)
✔ [363/494] Built Aesop.Builder.Cases (1.2s)
✔ [364/494] Built Batteries.Control.Nondet.Basic (1.2s)
✔ [365/495] Built Aesop.RuleTac (982ms)
✔ [366/495] Built Mathlib.Tactic.Basic (2.6s)
✔ [367/499] Built Aesop.Builder.Default (1.7s)
✔ [368/505] Built Mathlib.Tactic.Basify.Attr (2.9s)
✔ [369/505] Built Mathlib.Order.Defs.Unbundled (3.1s)
✔ [370/505] Built Mathlib.Order.Defs.LinearOrder (3.2s)
✔ [371/505] Built Aesop.Forward.State (7.6s)
✔ [372/505] Built Batteries.Data.Nat.Basic (714ms)
✔ [373/505] Built Aesop.RuleSet (4.3s)
✔ [374/505] Built Mathlib.Tactic.Hint (1.7s)
✔ [375/508] Built Mathlib.Algebra.Group.Monoid (4.4s)
✔ [376/511] Built Mathlib.Data.Int.Order.Basic (1.8s)
✔ [377/511] Built Batteries.Data.Nat.Lemmas (1.2s)
✔ [378/511] Built Aesop.Frontend.RuleExpr (3.3s)
✔ [379/511] Built Mathlib.Data.Bool.Basic (2.2s)
✔ [380/511] Built Mathlib.Logic.Relation (3.3s)
✔ [381/511] Built Aesop.Tree.Data (2.6s)
✔ [382/511] Built Aesop.Forward.State.Initial (1.3s)
✔ [383/513] Built Mathlib.Logic.Function.Basic (3.3s)
✔ [384/513] Built Aesop.Frontend.Extension.Init (902ms)
✔ [385/513] Built Aesop.Forward.State.ApplyGoalDiff (1.4s)
✔ [386/520] Built AeneasMeta.Saturate.Tactic:c.o (17s)
✔ [387/520] Built Mathlib.Tactic.ToExpr (1.4s)
✔ [388/520] Built Aesop.Search.Queue.Class (880ms)
✔ [389/520] Built Aesop.Tree.RunMetaM (1.1s)
✔ [390/520] Built Aesop.Tree.Traversal (1.1s)
✔ [391/520] Built Mathlib.Data.Set.CoeSort (1.4s)
✔ [392/520] Built Aesop.Tree.TreeM (939ms)
✔ [393/522] Built Mathlib.Algebra.Group.DivInvMonoid (2.1s)
✔ [394/522] Built Aesop.Frontend.Extension (994ms)
✔ [395/522] Built Mathlib.Tactic.GCongr.Core (5.5s)
✔ [396/522] Built AeneasMeta.Saturate.Tactic:dynlib (195ms)
✔ [397/522] Built Mathlib.Data.Nat.Init (2.2s)
✔ [398/522] Built Mathlib.Basic.IsEmpty.Basic (1.3s)
✔ [399/522] Built Mathlib.Logic.Pairwise (1.4s)
✔ [400/522] Built Mathlib.Algebra.Notation.Pi.Basic (1.7s)
✔ [402/522] Built Mathlib.Data.Sigma.Basic (1.7s)
✔ [403/522] Built Mathlib.Data.Sum.Basic (1.7s)
✔ [404/522] Built Mathlib.Basic.Unique (1.6s)
✔ [405/522] Built Mathlib.Logic.Function.Conjugate (1.8s)
✔ [406/522] Built Mathlib.Data.Subtype (1.8s)
✔ [407/522] Built Aesop.Search.Queue (1.5s)
✔ [408/522] Built Aesop.Tree.State (1.1s)
✔ [409/522] Built Aesop.Search.SearchM (1.4s)
✔ [410/522] Built Aesop.Tree.Tracing (1.9s)
✔ [411/522] Built Aesop.Tree.Free (1.1s)
✔ [412/522] Built Aesop.Tree.Stats (1.2s)
✔ [413/522] Built Mathlib.Tactic.Choose (2.8s)
✔ [414/522] Built Aesop.Saturate (4.8s)
✔ [415/522] Built Mathlib.Tactic.FBinop (2.7s)
✔ [416/522] Built Aesop.Forward.State.UpdateGoal (974ms)
✔ [417/522] Built Aesop.Tree.ExtractProof (1.5s)
✔ [418/522] Built Aesop.Tree.ExtractScript (1.9s)
✔ [420/522] Built Aesop.Frontend.Tactic (1.7s)
✔ [421/522] Built Aesop.Frontend.Attribute (1.3s)
✔ [422/522] Built Aesop.Tree.AddRapp (2.1s)
✔ [423/522] Built Mathlib.Tactic.GCongr (1.2s)
✔ [424/522] Built Mathlib.Algebra.Group.Defs (2.2s)
✔ [425/522] Built Aesop.Frontend.Command (2.1s)
✔ [426/523] Built Mathlib.Basic.FunLike.Basic (1.3s)
✔ [427/523] Built Mathlib.Logic.Function.Iterate (1.5s)
✔ [428/523] Built Aesop.Search.RuleSelection (921ms)
✔ [429/523] Built AeneasMeta.Saturate (2.4s)
✔ [430/523] Built Aesop.Tree.Check (1.4s)
✔ [431/523] Built Mathlib.Data.Quot (2.4s)
✔ [432/523] Built Mathlib.Basic.SProd (1.3s)
✔ [433/523] Built Aesop.Frontend.Saturate (1.5s)
✔ [434/523] Built Aesop.BuiltinRules.Subst (1.0s)
✔ [435/523] Built Aesop.BuiltinRules.Rfl (954ms)
✔ [436/523] Built Aesop.BuiltinRules.Split (1.0s)
✔ [437/523] Built Aesop.BuiltinRules.Ext (1.0s)
✔ [438/523] Built Aesop.BuiltinRules.Intros (1.0s)
✔ [439/523] Built Mathlib.Tactic.GRewrite.Core (3.9s)
✔ [440/523] Built Aesop.BuiltinRules.ApplyHyps (1.0s)
✔ [441/524] Built AeneasMeta.Saturate:c.o (176ms)
✔ [442/524] Built Aesop.BuiltinRules.DestructProducts (1.2s)
✔ [443/524] Built Aesop.BuiltinRules.Assumption (1.2s)
✔ [444/524] Built Plausible.Random (817ms)
✔ [445/524] Built Mathlib.Data.Nat.Basic (1.6s)
✔ [446/524] Built Mathlib.Basic.FunLike.Embedding (1.4s)
✔ [447/524] Built Mathlib.Algebra.Group.Semiconj.Defs (1.6s)
✔ [448/525] Built AeneasMeta.Saturate:dynlib (161ms)
✔ [449/525] Built Aesop.Frontend (839ms)
✔ [450/525] Built Mathlib.Algebra.Group.Pi.Basic (2.5s)
✔ [451/527] Built Aesop.BuiltinRules (1.1s)
✔ [452/528] Built Mathlib.Data.Prod.Basic (1.8s)
✔ [453/528] Built Mathlib.Algebra.Group.InjSurj (3.4s)
✔ [454/528] Built Plausible.Gen (1.1s)
✔ [455/529] Built Aesop.Search.Expansion.Norm (2.9s)
✔ [456/529] Built Mathlib.Tactic.GRewrite.Elab (2.1s)
✔ [457/530] Built Plausible.Shrinkable (608ms)
✔ [458/531] Built Mathlib.Basic.FunLike.Equiv (1.3s)
✔ [459/531] Built Mathlib.Order.Basic (4.3s)
✔ [460/533] Built Mathlib.Tactic.Finiteness.Attr (1.2s)
✔ [461/535] Built Plausible.Arbitrary (909ms)
✔ [462/536] Built Mathlib.Algebra.Group.Commute.Defs (1.6s)
✔ [463/536] Built Plausible.Attr (646ms)
✔ [464/537] Built Plausible.ArbitraryFueled (626ms)
✔ [465/537] Built Mathlib.Algebra.Notation.Prod (1.8s)
✔ [466/537] Built Mathlib.Tactic.GRewrite (1.3s)
✔ [467/537] Built Plausible.Sampleable (1.2s)
✔ [468/538] Built Aesop.Search.Expansion (2.2s)
✔ [469/539] Built Mathlib.Order.ULift (1.8s)
✔ [470/539] Built Mathlib.Algebra.Group.Hom.Defs (6.3s)
✔ [471/539] Built Batteries.Tactic.Case (2.0s)
✔ [472/539] Built Plausible.DeriveShrinkable (2.6s)
✔ [473/545] Built Plausible.Functions (1.3s)
✔ [474/545] Built Plausible.DeriveArbitrary (2.0s)
✔ [477/549] Built Mathlib.Logic.Equiv.Defs (4.1s)
✔ [478/550] Built Batteries.CodeAction.Attr (1.1s)
✔ [479/550] Built Mathlib.Order.Defs.Lattice (2.5s)
✔ [480/550] Built Aesop.Search.ExpandSafePrefix (1.3s)
✔ [481/550] Built LeanSearchClient.Basic (671ms)
✔ [482/550] Built Batteries.Tactic.GeneralizeProofs (3.5s)
✔ [483/550] Built Plausible.Testable (2.0s)
✔ [484/550] Built Mathlib.Algebra.Group.Units.Defs (4.3s)
✔ [485/550] Built Mathlib.Control.EquivFunctor (1.6s)
✔ [486/550] Built Batteries.CodeAction.Basic (1.3s)
✔ [487/552] Built Mathlib.Order.OrderDual (2.2s)
✔ [488/553] Built Mathlib.Algebra.Opposites (2.4s)
✔ [489/553] Built Mathlib.Tactic.ApplyCongr (1.6s)
✔ [490/553] Built Batteries.Data.List.Basic (3.3s)
✔ [491/553] Built Batteries.CodeAction.Misc (2.5s)
✔ [492/554] Built Mathlib.Logic.Equiv.Prod (2.0s)
✔ [493/555] Built Plausible.Tactic (1.2s)
✔ [494/555] Built Mathlib.Algebra.Group.Equiv.Defs (3.9s)
✔ [495/555] Built Mathlib.Order.Compare (1.5s)
✔ [496/556] Built Aesop.Search.Main (2.2s)
✔ [497/556] Built LeanSearchClient.Syntax (2.0s)
✔ [498/557] Built Mathlib.Lean.Meta.Basic (1.4s)
✔ [499/557] Built Mathlib.Tactic.ApplyWith (1.2s)
✔ [500/557] Built Mathlib.Order.RelClasses (2.3s)
✔ [501/558] Built Mathlib.Order.Max (2.1s)
✔ [502/558] Built Plausible (754ms)
✔ [503/558] Built Batteries.CodeAction.Match (1.4s)
✔ [504/559] Built Mathlib.Tactic.ByContra (1.4s)
✔ [505/559] Built Aesop.Main (1.5s)
✔ [506/559] Built LeanSearchClient.LoogleSyntax (1.6s)
✔ [507/559] Built Mathlib.Tactic.CasesM (1.8s)
✔ [508/559] Built Mathlib.Tactic.ClearExclamation (1.1s)
✔ [509/560] Built Mathlib.Tactic.ApplyAt (1.3s)
✔ [510/561] Built Mathlib.Logic.Equiv.Sum (2.2s)
✔ [511/561] Built Mathlib.Tactic.Check (1.6s)
✔ [512/562] Built Mathlib.Tactic.ClearExcept (1.2s)
✔ [513/564] Built Batteries.CodeAction (902ms)
✔ [514/567] Built LeanSearchClient (922ms)
✔ [515/576] Built Aesop (1.2s)
✔ [516/576] Built Mathlib.Tactic.Clear_ (1.3s)
✔ [521/576] Built Mathlib.Lean.GoalsLocation (1.1s)
✔ [523/579] Built Mathlib.Lean.Meta.KAbstractPositions (1.2s)
✔ [527/589] Built Mathlib.Order.BoundedOrder.Basic (2.6s)
✔ [528/599] Built Mathlib.Lean.FoldEnvironment (1.4s)
✔ [529/599] Built Mathlib.Data.Set.Operations (2.3s)
✔ [530/601] Built Mathlib.Lean.Meta.RefinedDiscrTree.Basic (1.7s)
✔ [531/601] Built ProofWidgets.Compat (883ms)
✔ [532/602] Built ProofWidgets.Util (968ms)
✔ [533/602] Built Mathlib.Tactic.NthRewrite (1.6s)
✔ [534/602] Built Mathlib.Data.Option.Basic (1.8s)
✔ [535/602] Built Mathlib.Control.Basic (1.5s)
✔ [536/603] Built Mathlib.Tactic.CongrM (1.5s)
✔ [537/604] Built Mathlib.Tactic.Constructor (1.2s)
✔ [538/604] Built ProofWidgets.Component.Basic (1.3s)
✔ [539/605] Built Mathlib.Lean.Meta.RefinedDiscrTree.Encode (1.8s)
✔ [540/605] Built Mathlib.Lean.MessageData.Trace (1.4s)
✔ [541/605] Built ProofWidgets.Cancellable (1.5s)
✔ [542/605] Built Mathlib.Lean.Meta.RefinedDiscrTree.Initialize (2.3s)
✔ [543/606] Built Mathlib.Order.Monotone.Defs (2.9s)
✔ [544/607] Built Mathlib.Logic.Equiv.Option (2.3s)
✔ [545/607] Built Mathlib.Tactic.DefEqTransformations (2.3s)
✔ [546/607] Built Mathlib.Tactic.DSimpPercent (1.4s)
✔ [547/607] Built ProofWidgets.Component.MakeEditLink (1.1s)
✔ [548/607] Built ProofWidgets.Component.Panel.Basic (1.3s)
✔ [549/607] Built Mathlib.Tactic.DeprecateTo (2.1s)
✔ [550/609] Built Mathlib.Tactic.ErwQuestion (1.5s)
✔ [551/610] Built Mathlib.Tactic.ExistsI (1.1s)
✔ [552/613] Built ProofWidgets.Data.Html (2.7s)
✔ [553/613] Built Mathlib.Lean.Meta.RefinedDiscrTree.Lookup (1.7s)
✔ [554/613] Built Mathlib.Tactic.FailIfNoProgress (1.5s)
✔ [555/615] Built Mathlib.Algebra.Group.Basic (6.4s)
✔ [556/615] Built Mathlib.Tactic.DefEqAbuse (2.1s)
✔ [557/615] Built Batteries.Util.Cache (856ms)
✔ [558/615] Built Mathlib.Tactic.FunProp.Mor (1.3s)
✔ [559/616] Built ProofWidgets.Component.OfRpcMethod (1.1s)
✔ [560/616] Built ProofWidgets.Component.RefreshComponent (1.5s)
✔ [561/617] Built ProofWidgets.Component.FilterDetails (1.2s)
✔ [562/617] Built Mathlib.Tactic.FunProp.Decl (1.8s)
✔ [563/617] Built Mathlib.Order.Monotone.Basic (3.2s)
✔ [564/617] Built Mathlib.Lean.Meta.RefinedDiscrTree (1.4s)
✔ [565/620] Built Mathlib.Tactic.FunProp.ToBatteries (2.1s)
✔ [566/621] Built Mathlib.Logic.Equiv.Basic (3.0s)
✔ [567/621] Built Mathlib.Tactic.Find (1.5s)
✔ [568/624] Built Mathlib.Algebra.Group.Semiconj.Basic (1.8s)
✔ [569/624] Built Mathlib.Algebra.Group.SelfInv (1.9s)
✔ [570/624] Built Mathlib.Tactic.InferParam (1.2s)
✔ [571/624] Built Mathlib.Tactic.GrindAttrs (1.5s)
✔ [572/626] Built Mathlib.Tactic.FunProp.FunctionData (1.7s)
✔ [573/627] Built Mathlib.Algebra.Group.Hom.Basic (2.9s)
✔ [574/627] Built Mathlib.Algebra.Group.Units.Basic (3.1s)
✔ [575/627] Built Mathlib.Tactic.GuardGoalNums (1.1s)
✔ [576/628] Built Mathlib.Tactic.ClickSuggestions.Util (3.1s)
✔ [577/629] Built Mathlib.Tactic.GuardHypNums (1.1s)
✔ [578/631] Built Mathlib.Algebra.Group.Commute.Basic (1.7s)
✔ [579/631] Built Mathlib.Tactic.HigherOrder (1.4s)
✔ [580/632] Built Mathlib.Order.Lattice (4.1s)
✔ [581/632] Built Mathlib.Tactic.FunProp.Types (1.4s)
✔ [582/632] Built Mathlib.Util.TermReduce (1.4s)
✔ [583/633] Built Mathlib.Tactic.Linter.HaveLetLinter (1.4s)
✔ [584/633] Built Mathlib.Tactic.Linter.MinImports (1.3s)
✔ [585/633] Built Mathlib.Tactic.ClickSuggestions.SectionState (1.6s)
✔ [586/634] Built Mathlib.Algebra.Group.Units.Hom (2.5s)
✔ [587/634] Built Mathlib.Tactic.Linter.PPRoundtrip (1.3s)
✔ [588/634] Built Mathlib.Tactic.ClickSuggestions.Unfold (1.6s)
✔ [589/634] Built Mathlib.Tactic.Linter.UpstreamableDecl (1.3s)
✔ [590/635] Built Mathlib.Algebra.Group.Equiv.Basic (2.9s)
✔ [591/635] Built Mathlib.Algebra.Group.Torsion (1.7s)
✔ [592/635] Built Mathlib.Tactic.FunProp.Theorems (2.0s)
✔ [593/635] Built Mathlib.Tactic.IrreducibleDef (2.1s)
✔ [594/635] Built Mathlib.Tactic.Observe (1.7s)
✔ [595/635] Built Mathlib.Tactic.RSuffices (1.4s)
✔ [596/635] Built Mathlib.Order.BoundedOrder.Lattice (1.9s)
✔ [597/637] Built Mathlib.Tactic.ClickSuggestions.ApplyAt (1.8s)
✔ [598/637] Built Mathlib.Tactic.ClickSuggestions.Apply (2.0s)
✔ [599/637] Built Mathlib.Tactic.Linter (1.1s)
✔ [600/638] Built Mathlib.Tactic.Recover (1.4s)
✔ [601/638] Built Mathlib.Tactic.ClickSuggestions.GRewrite (2.4s)
✔ [602/638] Built Mathlib.Tactic.Rename (1.3s)
✔ [603/639] Built Mathlib.Tactic.ClickSuggestions.Rewrite (2.3s)
✔ [604/642] Built Mathlib.Algebra.Group.Units.Equiv (2.3s)
✔ [605/642] Built Mathlib.Tactic.FunProp.Attr (1.4s)
✔ [606/643] Built Mathlib.Util.Tactic (1.5s)
✔ [607/643] Built Mathlib.Tactic.Says (1.8s)
✔ [608/644] Built Mathlib.Tactic.Set (1.8s)
✔ [609/645] Built Mathlib.Algebra.Group.Opposite (2.0s)
✔ [610/645] Built Mathlib.Algebra.Group.TypeTags.Basic (3.1s)
✔ [611/646] Built Mathlib.Lean.Elab.Tactic.Basic (1.4s)
✔ [612/646] Built Mathlib.Tactic.SimpIntro (1.4s)
✔ [613/647] Built Mathlib.Tactic.RenameBVar (1.3s)
✔ [614/647] Built Mathlib.Order.Disjoint (3.3s)
✔ [615/647] Built Mathlib.Tactic.Substs (1.2s)
✔ [616/648] Built Mathlib.Tactic.ClickSuggestions.FindPremises (2.2s)
✔ [617/649] Built Mathlib.Tactic.FunProp.Core (4.1s)
✔ [618/649] Built Mathlib.Tactic.SuccessIfFailWithMsg (1.3s)
✔ [619/650] Built Mathlib.Tactic.SudoSetOption (1.1s)
✔ [620/650] Built Mathlib.Tactic.SwapVar (1.3s)
✔ [621/651] Built Mathlib.Tactic.Setm (1.6s)
✔ [622/652] Built Mathlib.Tactic.ToLevel (1.1s)
✔ [623/656] Built Mathlib.Algebra.Group.TypeTags.Hom (2.1s)
✔ [624/656] Built Mathlib.Order.PropInstances (1.5s)
✔ [625/656] Built Mathlib.Tactic.ToFun (1.4s)
✔ [626/656] Built Mathlib.Tactic.Tauto (2.3s)
✔ [627/660] Built Mathlib.Tactic.Trace (1.0s)
✔ [628/662] Built Mathlib.Tactic.UnsetOption (1.0s)
✔ [629/662] Built Mathlib.Tactic.ClickSuggestions.TryPremises (2.5s)
✔ [630/665] Built Mathlib.Tactic.FunProp.Elab (1.8s)
✔ [631/665] Built Mathlib.Tactic.Widget.SelectInsertParamsClass (1.2s)
✔ [632/665] Built Mathlib.Tactic.Variable (2.1s)
✔ [633/665] Built Mathlib.Algebra.Group.Prod (4.6s)
✔ [634/665] Built Mathlib.Tactic.WLOG (1.7s)
✔ [635/671] Built Mathlib.Util.PrintSorries (1.8s)
✔ [636/671] Built Mathlib.Util.TransImports (1.3s)
✔ [637/680] Built Mathlib.Util.CountHeartbeats (1.9s)
✔ [638/690] Built Mathlib.Algebra.Group.Equiv.TypeTags (2.3s)
✔ [639/691] Built Mathlib.Tactic.ClickSuggestions (2.0s)
✔ [640/691] Built Mathlib.Data.Set.Basic (3.4s)
✔ [641/691] Built Mathlib.Tactic.Widget.SelectPanelUtils (1.4s)
✔ [642/691] Built Mathlib.Util.WhatsNew (1.5s)
✔ [643/694] Built Mathlib.Tactic.FunProp (1.1s)
✔ [644/694] Built Batteries.Tactic.Congr (1.2s)
✔ [645/694] Built Mathlib.Control.ULift (1.1s)
✔ [646/694] Built Mathlib.Data.Prod.PProd (1.0s)
✔ [647/694] Built Mathlib.Tactic.Monotonicity.Attr (1.1s)
✔ [648/696] Built AeneasMeta.Async.Test (69s)
✔ [649/696] Built Mathlib.Order.GaloisConnection.Defs (2.1s)
✔ [650/698] Built AeneasMeta.Async.Test:c.o (418ms)
✔ [651/698] Built Mathlib.Order.BoundedOrder.Monotone (1.5s)
✔ [652/698] Built AeneasMeta.Async.Test:dynlib (173ms)
✔ [653/702] Built Mathlib.Tactic.Widget.CongrM (1.3s)
✔ [654/702] Built Mathlib.Data.Set.Disjoint (1.8s)
✔ [655/702] Built Mathlib.Data.Set.Inclusion (1.7s)
✔ [656/703] Built Mathlib.Util.PPOptions (1.1s)
✔ [657/703] Built Mathlib.Tactic.Widget.Calc (2.1s)
✔ [658/703] Built Mathlib.Data.ULift (1.4s)
✔ [659/712] Built Mathlib.Tactic.Widget.Conv (2.6s)
✔ [660/719] Built Mathlib.Algebra.Order.ZeroLEOne (1.6s)
✔ [661/719] Built Mathlib.Order.Interval.Set.Defs (1.7s)
✔ [662/719] Built Mathlib.Tactic.Widget.LibraryRewrite (3.4s)
✔ [663/720] Built Mathlib.Logic.Embedding.Basic (2.4s)
✔ [664/720] Built Mathlib.Order.Bounds.Defs (1.5s)
✔ [665/721] Built Mathlib.Basic.Nontrivial.Basic (1.5s)
✔ [666/721] Built AeneasMeta.Async (2.7s)
✔ [667/722] Built Mathlib.Data.Option.NAry (1.4s)
✔ [668/722] Built AeneasMeta.Async:c.o (163ms)
✔ [669/722] Built Mathlib.Data.Set.Insert (2.0s)
✔ [670/724] Built AeneasMeta.Async:dynlib (179ms)
✔ [671/724] Built Mathlib.Order.TypeTags (1.5s)
✔ [672/724] Built Mathlib.Algebra.Order.IsBotOne (2.1s)
✔ [673/724] Built Mathlib.Tactic.Common (1.9s)
✔ [674/724] Built Mathlib.Control.Monad.Basic (1.3s)
✔ [675/724] Built Mathlib.Util.Delaborators (3.3s)
✔ [676/726] Built Mathlib.Dynamics.FixedPoints.Defs (1.4s)
✔ [677/729] Built Mathlib.Order.Iterate (1.9s)
✔ [678/731] Built Mathlib.Data.Bool.Set (1.6s)
✔ [679/731] Built Mathlib.Data.Set.Subsingleton (2.3s)
✔ [680/733] Built Mathlib.Tactic.SetLike (1.3s)
✔ [681/733] Built Batteries.Control.ForInStep.Lemmas (635ms)
✔ [682/735] Built Batteries.Data.List.Pairwise (631ms)
✔ [683/738] Built Mathlib.Order.Heyting.Basic (6.2s)
✔ [684/738] Built Mathlib.Order.RelIso.Basic (3.9s)
✔ [685/738] Built Mathlib.Order.SetNotation (3.4s)
✔ [686/742] Built AeneasMeta (2.7s)
✔ [687/755] Built AeneasMeta:c.o (192ms)
✔ [688/755] Built Mathlib.Data.List.TFAE (1.1s)
✔ [689/755] Built AeneasMeta:shared (292ms)
✔ [690/757] Built Mathlib.Lean.Expr.ExtraRecognizers (1.4s)
✔ [691/757] Built Mathlib.Basic.SetLike.Basic (2.2s)
✔ [692/757] Built Mathlib.Algebra.Group.End (4.6s)
✔ [693/757] Built Mathlib.Order.BooleanAlgebra.Defs (2.6s)
✔ [694/757] Built Aeneas.Tactic.Step.Simp (2.1s)
✔ [695/762] Built Mathlib.Data.Part (3.3s)
✔ [696/763] Built Aeneas.Tactic.Elab.TraitDefault.Init (2.2s)
✔ [697/765] Built Aeneas.Std.Spec (2.6s)
✔ [698/765] Built Mathlib.Util.AtomM (1.3s)
✔ [699/766] Built Mathlib.Data.Set.Notation (1.6s)
✔ [700/776] Built Mathlib.Algebra.Group.Int.Defs (1.2s)
✔ [701/776] Built Batteries.Data.List.Lemmas (4.9s)
✔ [702/776] Built Aeneas.Tactic.Step.DspecInduction (3.5s)
✔ [703/779] Built Mathlib.Logic.OpClass (1.3s)
✔ [704/779] Built Mathlib.Util.AtomM.Recurse (1.6s)
✔ [705/779] Built Batteries.Classes.RatCast (547ms)
✔ [706/782] Built Mathlib.Data.Int.Basic (1.7s)
✔ [707/783] Built Mathlib.Order.Hom.Basic (6.5s)
✔ [708/785] Built Mathlib.Order.WithBot (8.8s)
✔ [709/785] Built Mathlib.Algebra.Group.Equiv.Opposite (2.9s)
✔ [710/788] Built Mathlib.Algebra.Order.Monoid.Unbundled.Defs (2.5s)
✔ [711/788] Built Mathlib.Order.BooleanAlgebra.Basic (4.2s)
✔ [712/788] Built Mathlib.Data.Rat.Init (1.2s)
✔ [713/788] Built Aeneas.Extract.Extract (5.1s)
✔ [714/788] Built Mathlib.Data.Nat.Cast.Defs (1.4s)
✔ [715/788] Built Mathlib.Order.MinMax (2.2s)
✔ [716/788] Built Mathlib.Data.List.Pairwise (2.7s)
✔ [717/788] Built Mathlib.Algebra.Group.IsCommutative (1.4s)
✔ [718/788] Built Mathlib.Order.Part (2.0s)
✔ [719/792] Built Mathlib.Algebra.GroupWithZero.Defs (1.8s)
✔ [720/794] Built Mathlib.Order.Antisymmetrization (2.3s)
✔ [721/794] Built Mathlib.Data.Int.Cast.Defs (1.2s)
✔ [722/794] Built Mathlib.Algebra.Group.Even (2.6s)
✔ [723/794] Built Aeneas.Extract (1.7s)
✔ [724/794] Built Mathlib.Algebra.Notation.Bracket (1.3s)
✔ [725/802] Built Mathlib.Order.BooleanAlgebra.Set (2.0s)
✔ [726/802] Built Mathlib.Data.Rat.Defs (2.5s)
✔ [727/802] Built Mathlib.Order.Lex (1.7s)
✔ [728/802] Built Aeneas.Std.Core.Result (2.5s)
✔ [729/802] Built Mathlib.Order.SymmDiff (3.3s)
✔ [730/806] Built Mathlib.Algebra.CharZero.Defs (1.6s)
✔ [731/811] Built Mathlib.Data.Int.Cast.Basic (1.8s)
✔ [732/811] Built Mathlib.Algebra.NeZero (1.3s)
✔ [733/811] Built Mathlib.Algebra.Ring.Defs (3.4s)
✔ [734/817] Built Mathlib.Data.Set.SymmDiff (1.7s)
✔ [735/817] Built Aeneas.Std.Primitives (2.8s)
✔ [736/817] Built Mathlib.Tactic.TFAE (2.5s)
✔ [737/817] Built Mathlib.Algebra.Group.Semiconj.Units (1.8s)
✔ [738/817] Built Mathlib.Algebra.Group.Invertible.Defs (1.8s)
✔ [739/817] Built Mathlib.Algebra.Order.Monoid.Unbundled.Basic (5.0s)
✔ [740/817] Built Mathlib.Algebra.Group.Hom.Instances (3.4s)
✔ [741/817] Built Mathlib.Algebra.GroupWithZero.NeZero (1.3s)
✔ [742/817] Built Mathlib.Algebra.Ring.Semiconj (1.3s)
✔ [743/817] Built Mathlib.Algebra.Order.Group.Synonym (3.5s)
✔ [744/817] Built Mathlib.Algebra.Ring.GrindInstances (1.7s)
✔ [745/817] Built Mathlib.Algebra.Ring.Int.Defs (1.8s)
✔ [746/817] Built Mathlib.Algebra.Field.Defs (1.9s)
✔ [747/817] Built Mathlib.Tactic.Nontriviality.Core (1.8s)
✔ [748/817] Built Mathlib.Order.Interval.Set.Basic (5.1s)
✔ [749/818] Built Aeneas.Std.Core.Ops (2.5s)
✔ [750/821] Built Mathlib.Algebra.Order.Sub.Defs (2.0s)
✔ [751/821] Built Aeneas.Std.Delab (2.6s)
✔ [752/823] Built Mathlib.Algebra.Ring.Basic (2.2s)
✔ [753/825] Built Mathlib.Algebra.GroupWithZero.InjSurj (2.2s)
✔ [754/825] Built Mathlib.Algebra.Group.Commute.Units (2.6s)
✔ [755/825] Built Mathlib.Tactic.Nontriviality (1.7s)
✔ [756/829] Built Mathlib.Algebra.Order.Ring.Synonym (2.2s)
✔ [757/829] Built Mathlib.Algebra.GroupWithZero.Basic (2.5s)
✔ [758/831] Built Mathlib.Tactic.Bound.Init (1.5s)
✔ [759/834] Built Mathlib.Data.Set.Image (4.0s)
✔ [760/834] Built Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual (1.8s)
✔ [761/837] Built Mathlib.Algebra.Group.Nat.Defs (1.2s)
✔ [762/837] Built Mathlib.Algebra.Group.Invertible.Basic (1.0s)
✔ [763/837] Built Mathlib.Algebra.Order.GroupWithZero.Defs (2.8s)
✔ [764/837] Built Mathlib.Data.Nat.Cast.Pi (1.2s)
✔ [765/837] Built Mathlib.Algebra.Divisibility.Basic (2.5s)
✔ [766/837] Built Mathlib.Algebra.GroupWithZero.Units.Basic (2.8s)
✔ [767/837] Built Mathlib.Tactic.Bound.Attribute (1.7s)
✔ [768/837] Built Mathlib.Algebra.GroupWithZero.Hom (2.5s)
✔ [769/837] Built Mathlib.Data.Set.Restrict (2.1s)
✔ [770/837] Built Mathlib.Algebra.Order.Group.Unbundled.Basic (4.4s)
✔ [771/837] Built Mathlib.Data.Nat.Cast.NeZero (1.5s)
✔ [772/837] Built Mathlib.Data.Nat.Set (1.9s)
✔ [773/840] Built Mathlib.Algebra.GroupWithZero.Nat (1.4s)
✔ [774/840] Built Mathlib.Order.Directed (2.9s)
✔ [775/840] Built Mathlib.Algebra.Ring.InjSurj (5.0s)
✔ [776/840] Built Mathlib.Algebra.Group.Nat.Hom (1.9s)
✔ [777/840] Built Mathlib.Algebra.GroupWithZero.Invertible (1.8s)
✔ [778/844] Built Mathlib.Algebra.Divisibility.Hom (2.1s)
✔ [779/850] Built Mathlib.Algebra.Order.Monoid.Unbundled.Pow (3.0s)
✔ [780/853] Built Mathlib.Data.Set.Prod (4.4s)
✔ [781/853] Built Mathlib.Algebra.Ring.Nat (1.7s)
✔ [782/853] Built Mathlib.Algebra.Ring.Rat (2.5s)
✔ [783/857] Built Mathlib.Algebra.GroupWithZero.Semiconj (1.9s)
✔ [784/857] Built Mathlib.Algebra.Order.Group.OrderIso (2.3s)
✔ [785/858] Built Mathlib.Data.Nat.Sqrt (1.4s)
✔ [786/858] Built Mathlib.Algebra.Ring.Invertible (2.1s)
✔ [787/858] Built Mathlib.Data.PNat.Notation (1.2s)
✔ [788/858] Built Mathlib.Algebra.Ring.Hom.Defs (3.6s)
✔ [789/860] Built Mathlib.Algebra.Divisibility.Units (2.2s)
✔ [790/860] Built Mathlib.Algebra.GroupWithZero.Commute (1.9s)
✔ [791/860] Built Mathlib.Data.Nat.Find (2.2s)
✔ [792/860] Built Mathlib.Data.Set.NAry (2.6s)
✔ [793/860] Built Mathlib.Tactic.HaveI (1.7s)
✔ [794/864] Built Mathlib.Algebra.Order.Group.Lattice (2.4s)
✔ [795/864] Built Mathlib.Data.Int.Sqrt (2.5s)
✔ [796/867] Built Mathlib.Data.PNat.Defs (2.1s)
✔ [797/867] Built Mathlib.Lean.Expr.Rat (1.3s)
✔ [798/867] Built Mathlib.Algebra.Group.Nat.Even (2.6s)
✔ [799/869] Built Mathlib.Algebra.Ring.Units (1.9s)
✔ [800/869] Built Mathlib.Data.Set.Function (4.6s)
✔ [801/869] Built Mathlib.Util.Qq (1.4s)
✔ [802/869] Built Mathlib.Order.Bounds.Basic (5.9s)
✔ [803/869] Built Mathlib.Data.Nat.Cast.Basic (2.6s)
✔ [804/869] Built Mathlib.Algebra.GroupWithZero.Divisibility (2.4s)
✔ [805/869] Built Mathlib.Order.Nat (1.6s)
✔ [806/869] Built Mathlib.Algebra.GroupWithZero.Units.Lemmas (1.9s)
✔ [807/869] Built Mathlib.Tactic.TryThis (1.4s)
✔ [808/869] Built Mathlib.Algebra.Ring.Commute (2.0s)
✔ [809/869] Built Mathlib.Algebra.Group.Int.Even (2.4s)
✔ [810/869] Built Mathlib.Algebra.Order.Group.Unbundled.Abs (3.5s)
✔ [811/869] Built Mathlib.Data.Set.Pairwise.Basic (2.7s)
✔ [812/869] Built Mathlib.Tactic.NormNum.Result (3.6s)
✔ [813/870] Built Mathlib.Order.WellFounded (3.1s)
✔ [814/870] Built Mathlib.Data.Nat.Cast.Commute (1.9s)
✔ [815/874] Built Mathlib.Order.CompleteLattice.Defs (2.0s)
✔ [816/874] Built Mathlib.Data.Ineq (716ms)
✔ [817/876] Built Mathlib.Order.Bounds.Image (3.6s)
✔ [818/877] Built Mathlib.Data.Nat.Cast.Order.Basic (2.9s)
✔ [819/877] Built Mathlib.Logic.Equiv.Set (4.1s)
✔ [820/877] Built Mathlib.Algebra.Order.Group.Unbundled.Int (2.2s)
✔ [821/879] Built Mathlib.Algebra.Order.GroupWithZero.Basic (5.6s)
✔ [822/879] Built Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE (1.9s)
✔ [823/879] Built Mathlib.Algebra.Order.Monoid.Defs (2.2s)
✔ [824/881] Built Mathlib.Algebra.GroupWithZero.Regular (1.5s)
✔ [825/883] Built Mathlib.Tactic.NormNum.Core (3.5s)
✔ [826/884] Built Mathlib.Algebra.Field.Basic (4.0s)
✔ [827/884] Built Mathlib.Order.ScottContinuity (2.4s)
✔ [828/885] Built Mathlib.Algebra.Ring.Parity (3.6s)
✔ [829/885] Built Mathlib.Algebra.Group.WithOne.Defs (2.9s)
✔ [830/885] Built Mathlib.Algebra.GroupWithZero.Equiv (1.9s)
✔ [831/885] Built Mathlib.Algebra.Regular.Basic (1.9s)
✔ [832/885] Built Mathlib.Algebra.Order.Monoid.Canonical.Defs (2.6s)
✔ [833/887] Built Mathlib.Order.Hom.Set (3.0s)
✔ [834/888] Built Mathlib.Algebra.Order.Nonneg.Basic (3.5s)
✔ [835/888] Built Mathlib.Algebra.Order.Group.Defs (2.3s)
✔ [836/888] Built Mathlib.Algebra.Order.Ring.Unbundled.Rat (4.0s)
✔ [837/888] Built Mathlib.Algebra.Order.Group.Int (1.9s)
✔ [838/888] Built Mathlib.Algebra.Ring.Int.Parity (3.4s)
✔ [839/888] Built Mathlib.Algebra.Group.WithOne.Map (2.4s)
✔ [840/891] Built Mathlib.Data.Int.Cast.Lemmas (3.4s)
✔ [841/891] Built Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (5.1s)
✔ [842/891] Built Mathlib.Algebra.Order.Group.Nat (1.0s)
✔ [843/891] Built Mathlib.Algebra.Order.Monoid.Units (2.3s)
✔ [844/896] Built Mathlib.Algebra.Order.Monoid.OrderDual (2.2s)
✔ [845/896] Built Mathlib.Order.Preorder.Chain (2.7s)
✔ [846/896] Built Mathlib.Tactic.NormNum.Basic (6.7s)
✔ [847/900] Built Mathlib.Algebra.GroupWithZero.WithZero (4.5s)
✔ [848/902] Built Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags (2.4s)
✔ [849/902] Built Mathlib.Algebra.Order.Monoid.WithTop (2.4s)
✔ [850/902] Built Mathlib.Data.Rat.Lemmas (2.0s)
✔ [851/902] Built Mathlib.Data.NNRat.Defs (3.4s)
✔ [852/902] Built Mathlib.Algebra.Order.Group.Units (1.8s)
✔ [853/907] Built Mathlib.Algebra.Order.Monoid.NatCast (1.9s)
✔ [854/908] Built Mathlib.Util.SynthesizeUsing (1.2s)
✔ [855/910] Built Mathlib.Algebra.Order.Monoid.Unbundled.MinMax (2.5s)
✔ [856/912] Built Mathlib.Algebra.Order.Monoid.TypeTags (1.8s)
✔ [857/912] Built Mathlib.Algebra.Order.Sub.Unbundled.Basic (2.2s)
✔ [858/914] Built Mathlib.Order.CompleteLattice.Basic (6.4s)
✔ [859/914] Built Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes (1.5s)
✔ [860/914] Built Mathlib.Lean.Meta.Tactic.Rewrite (1.3s)
✔ [861/916] Built Mathlib.Algebra.Order.AddGroupWithTop (2.4s)
✔ [862/916] Built Mathlib.Algebra.Field.Rat (2.6s)
✔ [863/916] Built Mathlib.Data.Tree.Basic (1.7s)
✔ [864/916] Built Mathlib.Order.OmegaCompletePartialOrder (4.7s)
✔ [865/916] Built Mathlib.Tactic.NormNum.Pow (4.6s)
✔ [866/919] Built Mathlib.Tactic.Zify (2.2s)
✔ [867/922] Built Mathlib.Algebra.Order.Sub.Basic (2.3s)
✔ [868/923] Built Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm (1.6s)
✔ [869/924] Built Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Gauss (1.6s)
✔ [870/925] Built Mathlib.Util.ElabWithoutMVars (1.4s)
✔ [871/929] Built Mathlib.Order.CompleteLattice.Lemmas (2.9s)
✔ [872/932] Built Mathlib.Algebra.Order.Ring.Unbundled.Basic (3.9s)
✔ [873/932] Built Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.PositiveVector (1.3s)
✔ [874/935] Built Mathlib.Order.ConditionallyCompleteLattice.Defs (2.2s)
✔ [875/935] Built Mathlib.Order.ConditionallyCompletePartialOrder.Defs (1.9s)
✔ [876/937] Built Mathlib.Order.GaloisConnection.Basic (3.8s)
✔ [877/939] Built Mathlib.Data.Rat.Cast.Defs (2.9s)
✔ [878/939] Built Mathlib.Data.Set.Order (1.9s)
✔ [879/939] Built Mathlib.Order.Antichain (2.6s)
✔ [880/941] Built Mathlib.Algebra.Order.Monoid.Basic (2.0s)
✔ [881/946] Built Mathlib.Algebra.Order.Ring.Defs (2.4s)
✔ [882/946] Built Mathlib.Order.ConditionallyCompletePartialOrder.Basic (2.4s)
✔ [883/946] Built Mathlib.Order.Interval.Set.Image (3.4s)
✔ [884/946] Built Mathlib.Order.LatticeIntervals (3.2s)
✔ [885/946] Built Mathlib.Order.Hom.Order (2.5s)
✔ [886/947] Built Mathlib.Order.Interval.Set.LinearOrder (4.3s)
✔ [887/947] Built Mathlib.Data.Rat.Cast.CharZero (2.9s)
✔ [888/950] Built Mathlib.Algebra.Order.GroupWithZero.Canonical (6.0s)
✔ [889/950] Built Mathlib.Algebra.Order.Ring.InjSurj (1.0s)
✔ [890/953] Built Mathlib.Algebra.Order.Ring.Rat (2.4s)
✔ [891/954] Built Mathlib.Algebra.Order.Positive.Ring (2.5s)
✔ [892/954] Built Mathlib.Algebra.Order.Group.Abs (3.3s)
✔ [893/956] Built Mathlib.Algebra.Order.Ring.Canonical (2.4s)
✔ [894/956] Built Mathlib.Data.Int.GCD (2.6s)
✔ [895/958] Built Mathlib.Algebra.Notation (1.6s)
✔ [896/958] Built Mathlib.Tactic.CancelDenoms.Core (3.6s)
✔ [897/958] Built Mathlib.Algebra.Order.Ring.Nat (2.5s)
✔ [898/964] Built Mathlib.Algebra.Order.Hom.Basic (2.1s)
✔ [899/964] Built Mathlib.Order.Interval.Set.UnorderedInterval (3.5s)
✔ [900/965] Built Mathlib.Order.CompleteBooleanAlgebra (7.3s)
✔ [901/966] Built Mathlib.Tactic.NormNum.Inv (3.8s)
✔ [902/966] Built Mathlib.Data.Int.Cast.Field (1.8s)
✔ [903/966] Built Mathlib.Data.Int.Cast.Pi (1.3s)
✔ [904/966] Built Mathlib.Algebra.Order.Ring.Basic (3.2s)
✔ [905/966] Built Mathlib.Algebra.Order.Field.Canonical (2.8s)
✔ [906/966] Built Mathlib.Algebra.Notation.Support (3.2s)
✔ [907/969] Built Mathlib.Algebra.Order.Ring.Int (2.9s)
✔ [908/970] Built Mathlib.Data.Nat.Cast.Order.Ring (2.5s)
✔ [909/971] Built Mathlib.Data.Set.BooleanAlgebra (2.1s)
✔ [910/971] Built Mathlib.Order.Interval.Set.OrderEmbedding (2.5s)
✔ [911/971] Built Mathlib.Algebra.Order.Group.PosPart (3.7s)
✔ [912/971] Built Aeneas.Tactic.Simp.SimpScalar.Init (2.1s)
✔ [913/971] Built Aeneas.Tactic.Solver.ScalarTac.Init (2.9s)
✔ [914/971] Built Mathlib.Data.Nat.Factorial.Basic (3.4s)
✔ [915/972] Built Aeneas.Tactic.Simp.SimpBoolProp.Init (1.8s)
✔ [916/974] Built Mathlib.Tactic.NormNum.Eq (3.1s)
✔ [917/974] Built Mathlib.Data.Int.CharZero (2.2s)
✔ [918/974] Built Mathlib.Algebra.Order.Invertible (2.4s)
✔ [919/974] Built Aeneas.Tactic.Conv.Bvify.Init (1.9s)
✔ [920/975] Built Mathlib.Tactic.NormNum.Abs (2.6s)
✔ [921/975] Built Mathlib.Algebra.Order.Ring.Cast (2.8s)
✔ [922/975] Built Mathlib.Tactic.Linarith.Lemmas (2.3s)
✔ [923/975] Built Aeneas.Data.Nat (1.9s)
✔ [924/976] Built Aeneas.Data.Int (1.7s)
✔ [925/980] Built Mathlib.Order.Interval.Set.OrdConnected (2.9s)
✔ [926/986] Built Mathlib.Data.Set.Lattice.Indexed (3.1s)
✔ [927/986] Built Aeneas.Tactic.Simp.SimpLists.Init (1.0s)
✔ [928/986] Built Mathlib.Algebra.Group.Nat.Units (1.7s)
✔ [929/986] Built Aeneas.Tactic.Simp.SimpBoolProp.SimpBoolProp (2.7s)
✔ [930/988] Built Mathlib.Algebra.Group.Irreducible.Defs (1.6s)
✔ [931/988] Built Batteries.Data.Fin.Basic (1.2s)
✔ [932/991] Built Mathlib.Tactic.Linarith.Datatypes (3.2s)
✔ [933/991] Built Aeneas.Std.Scalar.Elab (3.6s)
✔ [934/991] Built Mathlib.Data.Int.DivMod (1.5s)
✔ [935/991] Built Mathlib.Tactic.NormNum.Ineq (4.6s)
✔ [936/991] Built Mathlib.Algebra.GroupWithZero.Opposite (2.1s)
✔ [937/991] Built Mathlib.Algebra.Prime.Defs (2.8s)
✔ [938/991] Built Mathlib.Data.Set.Lattice.Bounded (3.8s)
✔ [939/992] Built Mathlib.Algebra.Group.ULift (3.0s)
✔ [940/992] Built Mathlib.Tactic.Ring.Common (11s)
✔ [941/995] Built Mathlib.Tactic.Linarith.Parsing (3.4s)
✔ [942/995] Built Mathlib.Tactic.Positivity.Core (7.2s)
✔ [943/997] Built Mathlib.Tactic.Linarith.Preprocessing (4.6s)
✔ [944/997] Built Mathlib.Order.ConditionallyCompleteLattice.Basic (6.3s)
✔ [945/997] Built Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm (3.5s)
✔ [946/997] Built Mathlib.Data.Fin.Basic (3.3s)
✔ [947/997] Built Mathlib.Tactic.NormNum.DivMod (3.8s)
✔ [948/997] Built Mathlib.Algebra.Group.ModEq (2.7s)
✔ [949/998] Built Mathlib.Data.Nat.Prime.Defs (3.3s)
✔ [950/998] Built Mathlib.Order.BourbakiWitt (3.4s)
✔ [951/998] Built Mathlib.Algebra.Ring.Equiv (5.9s)
✔ [952/998] Built Mathlib.Algebra.Ring.Opposite (4.0s)
✔ [953/1000] Built Mathlib.Data.Nat.GCD.Basic (3.6s)
✔ [954/1000] Built Mathlib.Data.Nat.Cast.Prod (2.2s)
✔ [955/1000] Built Mathlib.Tactic.Linarith.Verification (4.2s)
✔ [956/1001] Built Mathlib.Algebra.GroupWithZero.Units.Equiv (2.1s)
✔ [957/1005] Built Mathlib.Algebra.CharP.Defs (3.1s)
✔ [958/1005] Built Mathlib.Order.CompleteLatticeIntervals (4.2s)
✔ [959/1005] Built Mathlib.Tactic.Ring.Basic (6.7s)
✔ [960/1005] Built Mathlib.Algebra.Group.Int.Units (2.3s)
✔ [961/1005] Built Mathlib.Data.Fin.SuccPred (4.0s)
✔ [962/1005] Built Mathlib.Order.FixedPoints (3.9s)
✔ [963/1005] Built Mathlib.Data.Nat.ModEq (3.0s)
✔ [964/1005] Built Mathlib.Algebra.Ring.ULift (4.2s)
✔ [965/1005] Built Mathlib.Data.ENat.Defs (1.7s)
✔ [966/1015] Built Mathlib.Algebra.Order.Sub.WithTop (2.4s)
✔ [967/1015] Built Mathlib.Algebra.Ring.Int.Units (1.6s)
✔ [968/1015] Built Mathlib.Algebra.Order.Nonneg.Lattice (2.5s)
✔ [969/1015] Built Mathlib.Data.Fin.Rev (2.2s)
✔ [970/1015] Built Aeneas.Data.Coinductive.ITreeWP.FunctionalWP (2.4s)
✔ [971/1015] Built Mathlib.Tactic.Ring.RingNF (3.4s)
✔ [972/1015] Built Mathlib.Order.Interval.Set.WithBotTop (2.5s)
✔ [973/1019] Built Mathlib.Tactic.Linarith.Frontend (3.0s)
✔ [974/1019] Built Mathlib.Data.Int.ModEq (3.0s)
✔ [975/1021] Built Mathlib.Data.ENat.Basic (3.1s)
✔ [976/1026] Built Mathlib.Algebra.Order.Ring.WithTop (6.9s)
✔ [977/1026] Built Mathlib.Algebra.Order.Nonneg.Ring (3.1s)
✔ [978/1026] Built Mathlib.Data.List.Monad (1.4s)
✔ [979/1026] Built Mathlib.Control.Functor (1.8s)
✔ [980/1026] Built Mathlib.Algebra.Group.Fin.Basic (2.8s)
✔ [981/1026] Built Aeneas.Data.Coinductive.ITreeWP.DWLP (2.9s)
✔ [982/1027] Built Aeneas.Data.Coinductive.ITreeWP.DWP (3.3s)
✔ [983/1032] Built Mathlib.Tactic.Positivity.Basic (13s)
✔ [984/1032] Built Batteries.Data.List.Perm (2.1s)
✔ [985/1035] Built Aeneas.Data.Coinductive.ITreeWP.Taxonomy (654ms)
✔ [986/1036] Built Mathlib.Data.List.InsertIdx (2.8s)
✔ [987/1037] Built Mathlib.Data.List.Forall2 (3.4s)
✔ [988/1037] Built Mathlib.Data.List.Defs (2.8s)
✔ [989/1039] Built Aeneas.Data.Coinductive.ITreeWP.Tests (1.3s)
✔ [990/1039] Built Mathlib.Data.ENat.Monoid (3.9s)
✔ [991/1045] Built Mathlib.Algebra.CharP.Basic (3.1s)
✔ [992/1052] Built Mathlib.Data.List.Count (2.5s)
✔ [993/1052] Built Mathlib.Data.Finset.Attr (1.6s)
✔ [994/1063] Built Aeneas.Data.Coinductive.ITreeWP (676ms)
✔ [995/1063] Built Mathlib.Algebra.Order.Nonneg.Field (4.4s)
✔ [996/1064] Built Mathlib.Order.Cover (6.6s)
✔ [997/1068] Built Mathlib.Tactic.NormNum.OfScientific (3.5s)
✔ [998/1075] Built Mathlib.Data.Set.List (2.0s)
✔ [999/1083] Built Mathlib.Data.List.Perm.Basic (2.0s)
✔ [1000/1084] Built Mathlib.Basic.Finite.Defs (1.0s)
✔ [1001/1088] Built Mathlib.Data.List.Induction (2.4s)
✔ [1002/1091] Built Batteries.Data.Fin.Lemmas (2.1s)
✔ [1003/1092] Built Mathlib.Algebra.Order.Field.Rat (3.4s)
✔ [1004/1092] Built Mathlib.Logic.Small.Defs (1.8s)
✔ [1005/1092] Built Mathlib.Basic.Countable.Defs (2.0s)
✔ [1006/1092] Built Mathlib.Data.List.TakeDrop (4.6s)
✔ [1007/1092] Built Mathlib.Data.Fin.Embedding (3.5s)
✔ [1008/1097] Built Mathlib.Data.List.Basic (5.5s)
✔ [1009/1097] Built Mathlib.Algebra.BigOperators.Group.List.Defs (1.7s)
✔ [1010/1097] Built Mathlib.Data.List.Flatten (1.0s)
✔ [1011/1097] Built Mathlib.Basic.UnivLE (1.6s)
✔ [1012/1097] Built Mathlib.Data.List.ProdSigma (2.2s)
✔ [1013/1097] Built Mathlib.Logic.Small.Basic (1.0s)
✔ [1014/1097] Built Aeneas.Std.WP (6.7s)
✔ [1015/1100] Built Mathlib.Data.List.Lex (2.5s)
✔ [1016/1100] Built Mathlib.Order.SuccPred.Basic (6.9s)
✔ [1017/1100] Built Mathlib.Order.Fin.Basic (3.3s)
✔ [1018/1100] Built Mathlib.Algebra.Order.Hom.Monoid (6.3s)
✔ [1019/1103] Built Mathlib.Data.Rat.Cast.Order (4.5s)
✔ [1020/1103] Built Mathlib.Data.List.Infix (2.8s)
✔ [1021/1103] Built Mathlib.Basic.Countable.Small (1.9s)
✔ [1022/1103] Built Mathlib.Data.List.Lattice (3.0s)
✔ [1023/1103] Built Mathlib.Data.List.Perm.Subperm (2.6s)
✔ [1024/1105] Built Mathlib.Data.List.Nodup (3.9s)
✔ [1025/1105] Built Mathlib.Algebra.BigOperators.Group.List.Basic (4.9s)
✔ [1026/1105] Built Mathlib.Order.SuccPred.WithBot (2.7s)
✔ [1027/1105] Built Aeneas.Tactic.Step.PrepareIntroOutputs (3.6s)
✔ [1028/1105] Built Mathlib.Data.List.Chain (3.8s)
✔ [1029/1107] Built Mathlib.Tactic.NormNum (2.8s)
✔ [1030/1107] Built Mathlib.Order.SuccPred.Archimedean (3.0s)
✔ [1031/1107] Built Mathlib.Algebra.Order.Hom.MonoidWithZero (3.9s)
✔ [1032/1109] Built Mathlib.Data.List.Dedup (2.8s)
✔ [1033/1109] Built Mathlib.Data.Multiset.Defs (3.4s)
✔ [1034/1109] Built Aeneas.Command.Decompose (6.5s)
✔ [1035/1112] Built Mathlib.Data.List.Perm.Lattice (2.9s)
✔ [1036/1112] Built Mathlib.Data.Fin.Tuple.Basic (5.2s)
✔ [1037/1112] Built Mathlib.Data.List.Duplicate (2.9s)
✔ [1038/1112] Built Mathlib.Data.List.Rotate (3.3s)
✔ [1039/1112] Built Aeneas.Tactic.Step.SpecInfo (2.9s)
✔ [1040/1115] Built Mathlib.Data.List.Range (2.5s)
✔ [1041/1115] Built Mathlib.Data.List.Enum (2.1s)
✔ [1042/1115] Built Mathlib.Tactic.Linarith (2.6s)
✔ [1043/1115] Built Mathlib.Data.Nat.Choose.Basic (2.7s)
✔ [1044/1115] Built Mathlib.Data.Multiset.ZeroCons (3.1s)
✔ [1045/1115] Built Mathlib.Data.List.OfFn (2.6s)
✔ [1046/1115] Built Mathlib.Data.Finset.Defs (3.1s)
✔ [1047/1116] Built Mathlib.Data.List.FinRange (2.9s)
✔ [1048/1116] Built Mathlib.Algebra.Order.Hom.Ring (4.1s)
✔ [1049/1116] Built Mathlib.Data.Set.Piecewise (2.4s)
✔ [1050/1121] Built Mathlib.Algebra.BigOperators.Group.List.Lemmas (3.2s)
✔ [1051/1121] Built Mathlib.Order.SuccPred.Limit (5.4s)
✔ [1052/1126] Built Mathlib.Data.Multiset.Count (2.4s)
✔ [1053/1126] Built Mathlib.Data.List.OffDiag (3.2s)
✔ [1054/1127] Built Mathlib.Data.Multiset.Basic (2.4s)
✔ [1055/1131] Built Mathlib.Data.Finset.Empty (2.7s)
✔ [1056/1131] Built Aeneas.Tactic.Solver.ScalarTac.Core (3.9s)
✔ [1057/1131] Built Mathlib.Data.List.Sort (4.1s)
✔ [1058/1136] Built Mathlib.Order.Hom.Bounded (4.4s)
✔ [1059/1138] Built Mathlib.Data.Set.Sigma (4.1s)
✔ [1060/1142] Built Mathlib.Data.Multiset.AddSub (3.4s)
✔ [1061/1142] Built Mathlib.Order.Hom.Lattice (5.3s)
✔ [1062/1143] Built Mathlib.Algebra.Order.SuccPred (4.4s)
✔ [1063/1143] Built Mathlib.Logic.Embedding.Set (3.7s)
✔ [1064/1147] Built Aeneas.Tactic.Step.Init (9.5s)
✔ [1065/1147] Built Mathlib.Data.Set.Lattice.Image (4.8s)
✔ [1066/1147] Built Mathlib.Control.Applicative (2.2s)
✔ [1067/1147] Built Mathlib.Logic.Function.DependsOn (2.8s)
✔ [1068/1147] Built Mathlib.Control.Traversable.Basic (2.1s)
✔ [1069/1151] Built Mathlib.Data.List.NodupEquivFin (3.7s)
✔ [1070/1151] Built Mathlib.Data.Multiset.Replicate (2.6s)
✔ [1071/1155] Built Mathlib.Data.Vector.Defs (2.6s)
✔ [1072/1155] Built Mathlib.Order.SuccPred.Nat (2.6s)
✔ [1073/1155] Built Mathlib.Tactic.ApplyFun (2.5s)
✔ [1074/1155] Built Mathlib.Order.Setoid.Basic (3.2s)
✔ [1075/1159] Built Mathlib.Data.List.Sublists (2.6s)
✔ [1076/1159] Built Aeneas.Tactic.Solver.ScalarTac.ScalarTac (7.4s)
✔ [1077/1161] Built Aeneas.Std.Core.Cmp (3.3s)
✔ [1078/1161] Built Mathlib.Data.List.Zip (2.5s)
✔ [1079/1165] Built Aeneas.Std.Core.Core (3.7s)
✔ [1080/1165] Built Mathlib.Order.Hom.BoundedLattice (5.0s)
✔ [1081/1165] Built Mathlib.Data.Nat.Bits (1.8s)
✔ [1082/1165] Built Mathlib.Data.Set.Lattice.Disjoint (2.2s)
✔ [1083/1168] Built Mathlib.Data.Multiset.MapFold (3.6s)
✔ [1084/1169] Built Mathlib.Data.Nat.Pairing (2.4s)
✔ [1085/1169] Built Mathlib.Data.PNat.Equiv (1.9s)
✔ [1086/1169] Built Mathlib.Order.SuccPred.ENat (3.1s)
✔ [1087/1169] Built Mathlib.Data.Vector.Basic (3.9s)
✔ [1088/1169] Built Mathlib.Data.Nat.Order.Lemmas (2.5s)
✔ [1089/1169] Built Mathlib.Data.Set.Pairwise.Lattice (2.4s)
✔ [1090/1171] Built Mathlib.Logic.Small.Set (2.1s)
✔ [1091/1175] Built Aeneas.Std.Alloc.Alloc (3.2s)
✔ [1092/1175] Built Aeneas.Std.Core.Convert (3.4s)
✔ [1093/1175] Built Mathlib.Data.List.MinMax (4.8s)
✔ [1094/1175] Built Mathlib.Data.Finset.Attach (2.6s)
✔ [1095/1175] Built Mathlib.Logic.Equiv.Nat (2.2s)
✔ [1096/1175] Built Mathlib.Data.Multiset.Filter (3.1s)
✔ [1097/1179] Built Mathlib.Order.Minimal (4.4s)
✔ [1098/1179] Built Mathlib.Data.ENat.Pow (2.8s)
✔ [1099/1179] Built Mathlib.Order.RelIso.Set (2.4s)
✔ [1100/1179] Built Mathlib.Order.Prod.Lex.Basic (4.0s)
✔ [1101/1179] Built Mathlib.Basic.Countable.Basic (3.2s)
✔ [1102/1179] Built Mathlib.Logic.Encodable.Basic (3.9s)
✔ [1103/1188] Built Aeneas.Std.Alloc.Boxed (4.3s)
✔ [1104/1190] Built Mathlib.Data.Finset.Erase (2.5s)
✔ [1105/1192] Built Mathlib.Data.Finset.Filter (3.2s)
✔ [1106/1192] Built Mathlib.Algebra.BigOperators.Group.Multiset.Defs (3.0s)
✔ [1107/1192] Built Mathlib.Order.UpperLower.Basic (5.5s)
✔ [1108/1192] Built Mathlib.Order.Sum.Order (5.9s)
✔ [1109/1192] Built Mathlib.Order.CompleteLattice.Chain (2.2s)
✔ [1110/1193] Built Mathlib.SetTheory.Cardinal.Defs (2.5s)
✔ [1111/1196] Built Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (2.0s)
✔ [1112/1199] Built Aeneas.Std.Scalar.Core (11s)
✔ [1113/1199] Built Mathlib.Data.Multiset.UnionInter (3.2s)
✔ [1114/1199] Built Mathlib.Algebra.Ring.CompTypeclasses (2.4s)
✔ [1115/1200] Built Mathlib.Algebra.GroupWithZero.Prod (2.7s)
✔ [1116/1201] Built Mathlib.Data.Int.Cast.Prod (2.1s)
✔ [1117/1203] Built Mathlib.Data.Fintype.Defs (3.5s)
✔ [1118/1210] Built Mathlib.Order.Zorn (2.3s)
✔ [1119/1210] Built Mathlib.Order.Hom.Lex (3.4s)
✔ [1120/1215] Built Mathlib.Data.Multiset.Dedup (2.6s)
✔ [1121/1215] Built Mathlib.Data.Multiset.Range (2.5s)
✔ [1122/1215] Built Mathlib.Algebra.Group.Action.Defs (3.4s)
✔ [1123/1215] Built Mathlib.Algebra.Group.Subsemigroup.Defs (3.1s)
✔ [1124/1215] Built Mathlib.Algebra.Group.Conj (3.2s)
✔ [1125/1215] Built Mathlib.SetTheory.Cardinal.SchroederBernstein (2.9s)
✔ [1126/1215] Built Mathlib.Algebra.Ring.Prod (4.1s)
✔ [1127/1215] Built Mathlib.Order.ConditionallyCompleteLattice.Indexed (5.1s)
✔ [1128/1215] Built Mathlib.Data.Finset.Dedup (2.5s)
✔ [1129/1217] Built Mathlib.Data.Multiset.Fold (2.4s)
✔ [1130/1219] Built Mathlib.Data.Multiset.FinsetOps (2.8s)
✔ [1131/1219] Built Mathlib.Algebra.Order.Group.Multiset (2.9s)
✔ [1132/1219] Built Mathlib.Order.InitialSeg (4.2s)
✔ [1133/1219] Built Mathlib.Algebra.Group.Action.Faithful (2.0s)
✔ [1134/1221] Built Mathlib.Algebra.Group.Pi.Lemmas (5.2s)
✔ [1135/1221] Built Mathlib.Algebra.Group.Action.Opposite (2.5s)
✔ [1136/1221] Built Mathlib.Algebra.Group.Subsemigroup.Basic (2.7s)
✔ [1137/1221] Built Mathlib.Algebra.Group.Pointwise.Set.Scalar (2.7s)
✔ [1138/1222] Built Mathlib.Order.SuccPred.CompleteLinearOrder (3.2s)
✔ [1139/1222] Built Mathlib.Algebra.Group.Submonoid.Defs (3.7s)
✔ [1140/1223] Built Mathlib.Data.Multiset.Lattice (2.6s)
✔ [1141/1223] Built Mathlib.Data.Finset.Lattice.Basic (3.1s)
✔ [1142/1223] Built Mathlib.Data.Finset.Insert (3.8s)
✔ [1143/1223] Built Mathlib.Algebra.Group.Center (6.3s)
✔ [1144/1223] Built Mathlib.Algebra.BigOperators.Group.Multiset.Basic (3.4s)
✔ [1145/1223] Built Mathlib.Data.Multiset.Sum (2.5s)
✔ [1146/1223] Built Mathlib.Logic.Function.CompTypeclasses (1.6s)
✔ [1147/1223] Built Mathlib.Algebra.Group.Action.Units (2.4s)
✔ [1148/1223] Built Mathlib.Data.Sym.Basic (3.8s)
✔ [1149/1223] Built Mathlib.Algebra.Group.Submonoid.MulAction (2.4s)
✔ [1150/1223] Built Mathlib.Algebra.GroupWithZero.Action.Defs (3.0s)
✔ [1151/1223] Built Mathlib.Algebra.Regular.SMul (2.3s)
✔ [1152/1226] Built Mathlib.Data.Finset.Lattice.Lemmas (2.5s)
✔ [1153/1226] Built Mathlib.Data.Finset.SDiff (2.8s)
✔ [1154/1231] Built Mathlib.Algebra.Group.Submonoid.Basic (3.4s)
✔ [1155/1231] Built Mathlib.Data.Finset.Range (2.9s)
✔ [1156/1232] Built Mathlib.Data.Finset.Disjoint (2.8s)
✔ [1157/1232] Built Mathlib.GroupTheory.Subsemigroup.Center (2.2s)
✔ [1158/1232] Built Mathlib.Algebra.Group.Hom.CompTypeclasses (1.8s)
✔ [1159/1232] Built Mathlib.Data.Multiset.Bind (3.1s)
✔ [1160/1234] Built Mathlib.Algebra.Group.Action.Basic (2.4s)
✔ [1161/1234] Built Mathlib.Algebra.Group.Submonoid.DistribMulAction (2.1s)
✔ [1162/1234] Built Mathlib.Algebra.Group.Action.TypeTags (1.9s)
✔ [1163/1235] Built Mathlib.Algebra.Module.Defs (2.2s)
✔ [1164/1238] Built Mathlib.Algebra.Group.Subgroup.Defs (5.5s)
✔ [1165/1239] Built Mathlib.Algebra.GroupWithZero.Action.Units (2.3s)
✔ [1166/1246] Built Mathlib.Data.Finset.Basic (3.7s)
✔ [1167/1246] Built Mathlib.Algebra.Group.Action.Pretransitive (2.4s)
✔ [1168/1248] Built Mathlib.Algebra.Group.Commute.Hom (1.9s)
✔ [1169/1258] Built Mathlib.Data.Multiset.Pi (3.1s)
✔ [1170/1258] Built Mathlib.Data.Multiset.Powerset (3.2s)
✔ [1171/1258] Built Mathlib.Algebra.Group.Support (2.6s)
✔ [1172/1263] Built Mathlib.Data.Finset.Image (4.8s)
✔ [1173/1263] Built Mathlib.Algebra.Order.Group.Action (1.9s)
✔ [1174/1263] Built Mathlib.Algebra.Group.Action.Hom (2.1s)
✔ [1175/1263] Built Mathlib.Algebra.Group.Irreducible.Lemmas (1.0s)
✔ [1176/1263] Built Mathlib.GroupTheory.GroupAction.Defs (4.8s)
✔ [1177/1263] Built Mathlib.Algebra.Ring.Divisibility.Basic (2.6s)
✔ [1178/1264] Built Mathlib.Data.List.Permutation (2.8s)
✔ [1179/1264] Built Mathlib.Dynamics.FixedPoints.Basic (2.6s)
✔ [1180/1264] Built Mathlib.Data.PNat.Basic (3.6s)
✔ [1181/1267] Built Mathlib.Data.Finset.BooleanAlgebra (2.8s)
✔ [1182/1267] Built Mathlib.Algebra.Group.Submonoid.Operations (8.9s)
✔ [1183/1267] Built Mathlib.Data.Finset.Fold (2.0s)
✔ [1184/1267] Built Mathlib.Data.Fintype.OfMap (2.7s)
✔ [1185/1267] Built Mathlib.Data.Finset.SymmDiff (2.5s)
✔ [1186/1267] Built Mathlib.Algebra.GroupWithZero.Action.End (1.9s)
✔ [1187/1267] Built Mathlib.Algebra.Prime.Lemmas (2.5s)
✔ [1188/1268] Built Mathlib.Algebra.Group.Embedding (2.3s)
✔ [1189/1275] Built Mathlib.Data.Finset.Piecewise (2.9s)
✔ [1190/1277] Built Mathlib.Algebra.Order.Ring.Abs (3.8s)
✔ [1191/1278] Built Mathlib.Algebra.Group.Pointwise.Set.Basic (10s)
✔ [1192/1278] Built Mathlib.Algebra.Ring.Action.Basic (2.4s)
✔ [1193/1283] Built Mathlib.GroupTheory.Submonoid.Center (3.0s)
✔ [1194/1284] Built Mathlib.Data.Fintype.Sets (3.8s)
✔ [1195/1284] Built Mathlib.Data.Finset.Union (4.0s)
✔ [1196/1284] Built Mathlib.Data.Finset.Card (6.6s)
✔ [1197/1284] Built Mathlib.Algebra.Notation.Indicator (3.0s)
✔ [1198/1284] Built Mathlib.Algebra.Group.Subgroup.Lattice (6.3s)
✔ [1199/1285] Built Mathlib.Algebra.Group.Pointwise.Set.Lattice (3.4s)
✔ [1200/1285] Built Mathlib.Algebra.GroupWithZero.Associated (4.2s)
✔ [1201/1287] Built Mathlib.Algebra.Group.Subsemigroup.MulOpposite (2.7s)
✔ [1202/1287] Built Mathlib.Order.Hom.WithTopBot (4.5s)
✔ [1203/1287] Built Mathlib.Data.Fintype.Basic (3.3s)
✔ [1204/1288] Built Mathlib.Algebra.Group.Action.Pointwise.Set.Basic (3.8s)
✔ [1205/1288] Built Mathlib.Data.Finset.Option (2.6s)
✔ [1206/1288] Built Mathlib.Data.Finset.Pi (3.0s)
✔ [1207/1288] Built Mathlib.Data.Finset.Sum (3.2s)
✔ [1208/1288] Built Mathlib.Data.Finset.Prod (3.7s)
✔ [1209/1288] Built Mathlib.Algebra.BigOperators.Group.Finset.Defs (6.4s)
✔ [1210/1288] Built Mathlib.Data.Nat.Prime.Basic (3.2s)
✔ [1211/1288] Built Mathlib.Algebra.Group.Idempotent (2.1s)
✔ [1212/1289] Built Mathlib.Algebra.Ring.Associated (2.9s)
✔ [1213/1289] Built Mathlib.Algebra.Group.Submonoid.MulOpposite (2.0s)
✔ [1214/1289] Built Mathlib.Algebra.FreeMonoid.Basic (4.5s)
✔ [1215/1289] Built Mathlib.Algebra.Group.Subgroup.Map (5.8s)
✔ [1216/1289] Built Mathlib.Data.Fintype.Card (3.1s)
✔ [1217/1293] Built Mathlib.Algebra.Group.Submonoid.Finite (2.6s)
✔ [1218/1293] Built Mathlib.Algebra.Group.TransferInstance (2.0s)
✔ [1219/1293] Built Mathlib.Algebra.Order.BigOperators.Group.List (3.1s)
✔ [1220/1293] Built Mathlib.Order.CompleteLattice.Finset (3.2s)
✔ [1221/1295] Built Mathlib.Order.Sigma.Lex (1.7s)
✔ [1222/1295] Built Mathlib.Algebra.CharP.Two (2.0s)
✔ [1223/1300] Built Mathlib.Algebra.Group.Subgroup.MulOpposite (3.1s)
✔ [1224/1306] Built Mathlib.GroupTheory.GroupAction.Hom (12s)
✔ [1225/1306] Built Mathlib.Algebra.Group.Commutator (1.6s)
✔ [1226/1310] Built Mathlib.Algebra.Group.Subgroup.ZPowers.Basic (3.2s)
✔ [1227/1310] Built Mathlib.Data.Finset.Lattice.Fold (6.5s)
✔ [1228/1310] Built Mathlib.Data.Fintype.EquivFin (3.5s)
✔ [1229/1310] Built Mathlib.Algebra.Group.Action.End (3.3s)
✔ [1230/1310] Built Mathlib.GroupTheory.Subsemigroup.Centralizer (2.5s)
✔ [1231/1314] Built Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic (2.3s)
✔ [1232/1314] Built Mathlib.Algebra.Group.Action.Prod (2.7s)
✔ [1233/1314] Built Mathlib.Algebra.Quotient (2.5s)
✔ [1234/1314] Built Mathlib.Algebra.GCDMonoid.Basic (7.5s)
✔ [1235/1314] Built Mathlib.Algebra.BigOperators.Group.Finset.Basic (8.6s)
✔ [1236/1314] Built Mathlib.Data.Finset.Lattice.Union (2.5s)
✔ [1237/1314] Built Mathlib.Algebra.Group.Subgroup.Ker (6.6s)
✔ [1238/1314] Built Mathlib.Data.Finset.Sigma (2.9s)
✔ [1239/1314] Built Mathlib.Data.Fintype.Prod (2.6s)
✔ [1240/1314] Built Mathlib.Data.Fintype.Option (2.5s)
✔ [1241/1314] Built Mathlib.Data.Fintype.Sum (3.0s)
✔ [1242/1314] Built Mathlib.Data.Finset.Max (4.9s)
✔ [1243/1314] Built Mathlib.GroupTheory.Submonoid.Centralizer (2.6s)
✔ [1244/1314] Built Mathlib.Basic.Denumerable (3.6s)
✔ [1245/1314] Built Mathlib.Data.ZMod.Defs (3.5s)
✔ [1246/1314] Built Mathlib.Algebra.Group.Submonoid.Membership (5.8s)
✔ [1247/1314] Built Mathlib.Algebra.GroupWithZero.Action.Basic (3.2s)
✔ [1248/1314] Built Mathlib.Data.Set.Finite.Basic (4.5s)
✔ [1249/1314] Built Mathlib.Algebra.GCDMonoid.Nat (3.4s)
✔ [1250/1314] Built Mathlib.Algebra.GCDMonoid.Multiset (3.1s)
✔ [1251/1315] Built Mathlib.GroupTheory.Congruence.Defs (5.2s)
✔ [1252/1315] Built Mathlib.GroupTheory.Coset.Defs (4.4s)
✔ [1253/1315] Built Mathlib.Algebra.BigOperators.GroupWithZero.Finset (2.8s)
✔ [1254/1315] Built Mathlib.Data.Finset.Powerset (3.7s)
✔ [1255/1315] Built Mathlib.Algebra.BigOperators.Option (2.0s)
✔ [1256/1315] Built Mathlib.Data.Finset.NoncommProd (3.9s)
✔ [1257/1315] Built Mathlib.Algebra.BigOperators.Group.Finset.Sigma (2.9s)
✔ [1258/1315] Built Mathlib.Logic.Equiv.List (2.7s)
✔ [1259/1315] Built Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (4.8s)
✔ [1260/1315] Built Mathlib.Data.Fintype.Sigma (3.7s)
✔ [1261/1315] Built Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set (3.1s)
✔ [1262/1317] Built Mathlib.SetTheory.Cardinal.Order (4.1s)
✔ [1263/1317] Built Mathlib.Data.Finset.Preimage (3.3s)
✔ [1264/1317] Built Mathlib.Data.Fintype.Pi (3.3s)
✔ [1265/1319] Built Mathlib.Data.Set.Finite.Range (3.4s)
✔ [1266/1319] Built Mathlib.Order.Preorder.Finite (3.6s)
✔ [1267/1319] Built Mathlib.Algebra.GCDMonoid.Finset (3.1s)
✔ [1268/1319] Built Mathlib.Data.Fintype.List (2.6s)
✔ [1269/1319] Built Mathlib.Algebra.Module.NatInt (3.1s)
✔ [1270/1323] Built Mathlib.Data.Set.Finite.Powerset (2.6s)
✔ [1271/1325] Built Mathlib.Data.Fintype.Powerset (2.5s)
✔ [1272/1325] Built Mathlib.GroupTheory.Congruence.Hom (3.6s)
✔ [1273/1325] Built Mathlib.Algebra.GroupWithZero.Action.Opposite (1.9s)
✔ [1274/1325] Built Mathlib.Algebra.Group.Submonoid.BigOperators (3.1s)
✔ [1275/1325] Built Mathlib.Algebra.Regular.Opposite (1.7s)
✔ [1276/1328] Built Mathlib.Algebra.Group.Subgroup.Basic (9.2s)
✔ [1277/1328] Built Mathlib.Basic.Finite.Prod (2.6s)
✔ [1278/1328] Built Mathlib.Logic.Equiv.Sigma (1.9s)
✔ [1279/1328] Built Mathlib.Data.Set.Countable (2.7s)
✔ [1280/1331] Built Mathlib.Algebra.Module.Opposite (2.3s)
✔ [1281/1331] Built Mathlib.Data.Nat.Log (3.1s)
✔ [1282/1331] Built Mathlib.Data.Nat.Prime.Pow (3.1s)
✔ [1283/1331] Built Mathlib.Data.List.Cycle (5.1s)
✔ [1284/1331] Built Mathlib.Data.Set.Finite.Lattice (5.2s)
✔ [1285/1331] Built Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas (3.8s)
✔ [1286/1331] Built Mathlib.GroupTheory.Subgroup.Center (3.5s)
✔ [1287/1331] Built Mathlib.GroupTheory.QuotientGroup.Defs (6.2s)
✔ [1288/1331] Built Mathlib.Algebra.Group.Pointwise.Set.Finite (3.4s)
✔ [1289/1334] Built Mathlib.Order.Interval.Finset.Defs (7.8s)
✔ [1290/1335] Built Mathlib.Data.Fintype.Vector (2.8s)
✔ [1291/1335] Built Mathlib.Basic.Finite.Sigma (2.6s)
✔ [1292/1335] Built Mathlib.GroupTheory.Coset.Basic (6.2s)
✔ [1293/1335] Built Mathlib.Algebra.Order.BigOperators.Group.Multiset (3.2s)
✔ [1294/1335] Built Mathlib.Algebra.Order.Monoid.Multiset (2.4s)
✔ [1295/1336] Built Mathlib.Algebra.Module.Torsion.Free (3.2s)
✔ [1296/1336] Built Mathlib.Algebra.IsPrimePow (2.5s)
✔ [1297/1339] Built Mathlib.Dynamics.PeriodicPts.Defs (3.5s)
✔ [1298/1340] Built Mathlib.Algebra.Group.Subgroup.Actions (3.1s)
✔ [1299/1342] Built Mathlib.Order.Interval.Set.SuccPred (3.2s)
✔ [1300/1345] Built Mathlib.GroupTheory.Subgroup.Centralizer (3.8s)
✔ [1301/1345] Built Mathlib.Algebra.Ring.CharZero (2.6s)
✔ [1302/1347] Built Mathlib.Order.ConditionallyCompleteLattice.Finset (4.2s)
✔ [1303/1347] Built Mathlib.Data.Fintype.BigOperators (3.6s)
✔ [1304/1347] Built Mathlib.Data.List.NatAntidiagonal (2.8s)
✔ [1305/1347] Built Mathlib.Algebra.BigOperators.Ring.List (2.9s)
✔ [1306/1349] Built Mathlib.Algebra.Order.Antidiag.Prod (4.8s)
✔ [1307/1349] Built Mathlib.Data.List.Prime (3.1s)
✔ [1308/1349] Built Mathlib.Order.Interval.Finset.Basic (6.2s)
✔ [1309/1349] Built Mathlib.Order.Interval.Finset.SuccPred (3.9s)
✔ [1310/1350] Built Mathlib.Algebra.Order.BigOperators.Group.Finset (6.5s)
✔ [1311/1350] Built Mathlib.Data.Nat.Prime.Infinite (2.4s)
✔ [1312/1350] Built Mathlib.Order.Interval.Set.Infinite (2.4s)
✔ [1313/1350] Built Mathlib.GroupTheory.GroupAction.ConjAct (3.4s)
✔ [1314/1357] Built Mathlib.GroupTheory.GroupAction.Basic (5.4s)
✔ [1315/1357] Built Mathlib.Data.Multiset.NatAntidiagonal (2.3s)
✔ [1316/1357] Built Mathlib.Tactic.FinCases (2.5s)
✔ [1317/1357] Built Mathlib.Data.Nat.Factors (3.1s)
✔ [1318/1360] Built Mathlib.GroupTheory.GroupAction.SubMulAction (8.8s)
✔ [1319/1360] Built Aeneas.Tactic.Simproc.ReduceZMod.Init (2.9s)
✔ [1320/1362] Built Mathlib.SetTheory.Cardinal.Basic (5.3s)
✔ [1321/1362] Built Mathlib.Order.Interval.Multiset (3.6s)
✔ [1322/1362] Built Mathlib.Algebra.Module.RingHom (2.9s)
✔ [1323/1364] Built Mathlib.Algebra.Order.Interval.Finset.SuccPred (4.0s)
✔ [1324/1365] Built Mathlib.Data.Finset.NatAntidiagonal (3.4s)
✔ [1325/1370] Built Mathlib.GroupTheory.Commutator.Basic (8.8s)
✔ [1326/1374] Built Mathlib.Data.Nat.PrimeFin (2.0s)
✔ [1327/1374] Built Mathlib.Algebra.EuclideanDomain.Defs (2.3s)
✔ [1328/1374] Built Mathlib.Data.Nat.Prime.Int (2.4s)
✔ [1329/1374] Built Mathlib.Algebra.GroupWithZero.Action.Regular (1.9s)
✔ [1330/1374] Built Mathlib.Algebra.Group.PUnit (1.6s)
✔ [1331/1376] Built Mathlib.Order.Interval.Finset.Nat (3.5s)
✔ [1332/1376] Built Mathlib.SetTheory.Cardinal.ENat (3.7s)
✔ [1333/1376] Built Aeneas.Tactic.Solver.ScalarTac.CondSimpTac (7.0s)
✔ [1334/1376] Built Mathlib.Algebra.EuclideanDomain.Field (2.4s)
✔ [1335/1376] Built Mathlib.Algebra.EuclideanDomain.Int (2.0s)
✔ [1336/1376] Built Mathlib.Algebra.Ring.PUnit (1.7s)
✔ [1337/1378] Built Mathlib.Algebra.EuclideanDomain.Basic (3.3s)
✔ [1338/1378] Built Mathlib.Algebra.Module.Submodule.Defs (4.6s)
✔ [1339/1378] Built Mathlib.Algebra.GroupWithZero.Idempotent (1.0s)
✔ [1340/1379] Built Mathlib.Tactic.Abel (5.6s)
✔ [1341/1379] Built Mathlib.Algebra.GroupWithZero.NonZeroDivisors (4.3s)
✔ [1342/1383] Built Mathlib.Order.Lattice.Nat (3.3s)
✔ [1343/1383] Built Mathlib.GroupTheory.GroupAction.Quotient (6.3s)
✔ [1344/1389] Built Mathlib.Algebra.Module.PUnit (2.6s)
✔ [1345/1390] Built Mathlib.SetTheory.Cardinal.ToNat (3.3s)
✔ [1346/1391] Built Mathlib.Algebra.GroupWithZero.Action.Prod (2.7s)
✔ [1347/1392] Built Mathlib.Algebra.Ring.Idempotent (2.6s)
✔ [1348/1393] Built Mathlib.RingTheory.Ideal.Defs (2.8s)
✔ [1349/1393] Built Mathlib.Dynamics.PeriodicPts.Lemmas (2.7s)
✔ [1350/1393] Built Mathlib.Algebra.Module.LinearMap.Defs (10s)
✔ [1351/1396] Built Mathlib.Algebra.Module.Submodule.Basic (3.1s)
✔ [1352/1397] Built Mathlib.Algebra.Module.Prod (2.3s)
✔ [1353/1397] Built Mathlib.Order.OrderIsoNat (3.1s)
✔ [1354/1398] Built Mathlib.Basic.Finite.Set (2.7s)
✔ [1355/1400] Built Mathlib.SetTheory.Cardinal.Finite (3.6s)
✔ [1356/1402] Built Mathlib.Order.Hom.CompleteLattice (4.7s)
✔ [1357/1402] Built Mathlib.Data.Finset.Order (2.8s)
✔ [1358/1403] Built Mathlib.Data.Set.Lattice.Order (2.8s)
✔ [1359/1403] Built Mathlib.Order.Interval.Set.OrderIso (2.6s)
✔ [1360/1405] Built Mathlib.NumberTheory.Divisors (9.7s)
✔ [1361/1405] Built Mathlib.Data.Set.Monotone (2.9s)
✔ [1362/1410] Built Mathlib.Algebra.Algebra.Defs (3.7s)
✔ [1363/1410] Built Mathlib.Order.WellQuasiOrder (2.0s)
✔ [1364/1413] Built Mathlib.Order.Closure (3.1s)
✔ [1365/1415] Built Mathlib.Algebra.Module.Torsion.Field (2.3s)
✔ [1366/1417] Built Mathlib.Data.Finset.Lattice.Prod (3.3s)
✔ [1367/1417] Built Mathlib.Algebra.GroupWithZero.Units.Fintype (2.7s)
✔ [1368/1418] Built Mathlib.Tactic.Ring.PNat (2.5s)
✔ [1369/1419] Built Mathlib.GroupTheory.Coset.Card (4.6s)
✔ [1370/1419] Built Mathlib.Algebra.Group.Action.Pi (2.6s)
✔ [1371/1421] Built Mathlib.Algebra.GroupWithZero.Pi (2.1s)
✔ [1372/1421] Built Mathlib.Order.ModularLattice (5.0s)
✔ [1373/1424] Built Mathlib.Order.WellFoundedSet (4.8s)
✔ [1374/1424] Built Mathlib.Data.Set.Card (6.7s)
✔ [1375/1424] Built Mathlib.Tactic.Ring (3.7s)
✔ [1376/1424] Built Mathlib.Algebra.Order.SuccPred.WithBot (3.1s)
✔ [1377/1424] Built Mathlib.Data.ENat.Lattice (4.4s)
✔ [1378/1424] Built Mathlib.Order.SupClosed (6.2s)
✔ [1379/1424] Built Mathlib.Algebra.GroupWithZero.Action.Pi (3.7s)
✔ [1380/1424] Built Mathlib.Algebra.Module.Equiv.Defs (12s)
✔ [1381/1424] Built Mathlib.Basic.Rel (5.3s)
✔ [1382/1424] Built Mathlib.Algebra.Ring.Pi (4.3s)
✔ [1383/1426] Built Mathlib.Data.DFinsupp.Defs (7.8s)
✔ [1384/1429] Built Mathlib.Data.Fin.VecNotation (5.2s)
✔ [1385/1432] Built Mathlib.Data.Fintype.Pigeonhole (3.0s)
✔ [1386/1432] Built Mathlib.Algebra.Module.Equiv.Opposite (3.4s)
✔ [1387/1434] Built Mathlib.SetTheory.Cardinal.NatCard (3.7s)
✔ [1388/1434] Built Mathlib.Algebra.Group.Hom.End (2.7s)
✔ [1389/1434] Built Mathlib.Order.SupIndep (6.4s)
✔ [1390/1434] Built Mathlib.Algebra.Group.Submonoid.Pointwise (5.3s)
✔ [1391/1436] Built Mathlib.Algebra.Module.Pi (3.7s)
✔ [1392/1438] Built Mathlib.Algebra.GroupWithZero.Action.Hom (2.9s)
✔ [1393/1438] Built Mathlib.Algebra.GroupWithZero.ULift (2.1s)
✔ [1394/1438] Built Mathlib.Order.Atoms (8.0s)
✔ [1395/1438] Built Mathlib.Algebra.Module.Submodule.Lattice (6.6s)
✔ [1396/1438] Built Mathlib.Algebra.Module.End (3.3s)
✔ [1397/1438] Built Mathlib.Algebra.Group.Subgroup.Finite (4.8s)
✔ [1398/1438] Built Mathlib.Algebra.Module.Torsion.Pi (3.4s)
✔ [1399/1438] Built Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise (3.9s)
✔ [1400/1438] Built Mathlib.Algebra.Module.LinearMap.End (6.9s)
✔ [1401/1439] Built Mathlib.Data.DFinsupp.Module (4.2s)
✔ [1402/1439] Built Mathlib.Algebra.Group.Subgroup.Pointwise (6.3s)
✔ [1403/1441] Built Mathlib.RingTheory.NonUnitalSubsemiring.Defs (4.4s)
✔ [1404/1441] Built Mathlib.Order.RelSeries (8.9s)
✔ [1405/1441] Built Mathlib.GroupTheory.GroupAction.DomAct.Basic (4.8s)
✔ [1406/1441] Built Mathlib.Algebra.Module.ULift (4.7s)
✔ [1407/1441] Built Mathlib.Algebra.Module.Submodule.RestrictScalars (4.9s)
✔ [1408/1442] Built Mathlib.Order.CompactlyGenerated.Basic (5.8s)
✔ [1409/1442] Built Mathlib.RingTheory.Ideal.Lattice (3.0s)
✔ [1410/1443] Built Mathlib.Algebra.Ring.Action.Subobjects (3.6s)
✔ [1411/1443] Built Mathlib.LinearAlgebra.Span.Defs (6.8s)
✔ [1412/1443] Built Mathlib.Algebra.Group.Subsemigroup.Membership (3.5s)
✔ [1413/1444] Built Mathlib.Algebra.GroupWithZero.Subgroup (4.3s)
✔ [1414/1444] Built Mathlib.Algebra.Module.Submodule.LinearMap (5.4s)
✔ [1415/1447] Built Mathlib.RingTheory.NonUnitalSubring.Defs (4.7s)
✔ [1416/1447] Built Mathlib.Algebra.Ring.Subsemiring.Defs (4.4s)
✔ [1417/1449] Built Mathlib.Algebra.GroupWithZero.Center (2.7s)
✔ [1418/1449] Built Mathlib.Algebra.Module.LinearMap.Basic (4.6s)
✔ [1419/1453] Built Mathlib.Algebra.Ring.Center (3.7s)
✔ [1420/1456] Built Mathlib.RingTheory.Ideal.Prime (3.9s)
✔ [1421/1456] Built Mathlib.Algebra.Module.Hom (4.3s)
✔ [1422/1459] Built Mathlib.Algebra.Ring.Centralizer (2.9s)
✔ [1423/1469] Built Mathlib.Algebra.Ring.Submonoid.Basic (2.0s)
✔ [1424/1470] Built Mathlib.Algebra.Group.Subsemigroup.Operations (7.5s)
✔ [1425/1472] Built Mathlib.Order.KrullDimension (7.5s)
✔ [1426/1473] Built Mathlib.GroupTheory.QuotientGroup.Basic (10s)
✔ [1427/1473] Built Mathlib.Algebra.Ring.Hom.InjSurj (2.4s)
✔ [1428/1473] Built Mathlib.Algebra.Group.Action.TransferInstance (3.4s)
✔ [1429/1473] Built Mathlib.Algebra.NoZeroSMulDivisors.Defs (2.8s)
✔ [1430/1473] Built Mathlib.Algebra.Ring.Aut (2.0s)
✔ [1431/1473] Built Mathlib.Algebra.Ring.Subring.Defs (5.2s)
✔ [1432/1476] Built Mathlib.Algebra.Group.Pointwise.Set.ListOfFn (2.9s)
✔ [1433/1476] Built Mathlib.Algebra.Module.Submodule.Map (7.0s)
✔ [1434/1478] Built Mathlib.Algebra.Group.Pointwise.Set.BigOperators (3.9s)
✔ [1435/1478] Built Mathlib.Data.Finset.NAry (4.4s)
✔ [1436/1478] Built Mathlib.RingTheory.NonUnitalSubsemiring.Basic (5.4s)
✔ [1437/1478] Built Mathlib.Algebra.GroupWithZero.Action.TransferInstance (3.1s)
✔ [1438/1478] Built Mathlib.Algebra.Ring.Action.Group (2.8s)
✔ [1439/1478] Built Mathlib.Algebra.Group.IsApply (2.5s)
✔ [1440/1480] Built Mathlib.Algebra.BigOperators.Group.Finset.Lemmas (2.0s)
✔ [1441/1481] Built Mathlib.Algebra.Group.Shrink (3.4s)
✔ [1442/1481] Built Mathlib.Algebra.FiniteSupport.Defs (2.1s)
✔ [1443/1483] Built Mathlib.Algebra.Module.Submodule.Ker (3.6s)
✔ [1444/1483] Built Mathlib.Algebra.Module.Submodule.Pointwise (4.3s)
✔ [1445/1483] Built Mathlib.Algebra.Module.TransferInstance (2.8s)
✔ [1446/1483] Built Mathlib.Algebra.BigOperators.Pi (3.8s)
✔ [1447/1483] Built Mathlib.GroupTheory.Index (8.5s)
✔ [1448/1483] Built Mathlib.Algebra.Group.Indicator (3.0s)
✔ [1449/1483] Built Mathlib.Algebra.Module.Equiv.Basic (12s)
✔ [1450/1484] Built Mathlib.Algebra.GroupWithZero.Indicator (2.4s)
✔ [1451/1484] Built Mathlib.RingTheory.NonUnitalSubring.Basic (5.4s)
✔ [1452/1488] Built Mathlib.Algebra.Notation.FiniteSupport (2.6s)
✔ [1453/1488] Built Mathlib.Algebra.Module.Submodule.EqLocus (2.0s)
✔ [1454/1491] Built Mathlib.Algebra.Ring.Subsemiring.Basic (6.6s)
✔ [1455/1492] Built Mathlib.Algebra.Module.Basic (2.5s)
✔ [1456/1492] Built Mathlib.Algebra.Module.Shrink (2.3s)
✔ [1457/1494] Built Mathlib.Algebra.Order.Group.Indicator (2.6s)
✔ [1458/1499] Built Mathlib.Algebra.BigOperators.Group.Finset.Pi (2.5s)
✔ [1459/1499] Built Mathlib.Data.Multiset.Antidiagonal (2.5s)
✔ [1460/1499] Built Mathlib.Algebra.Module.Submodule.Range (4.2s)
✔ [1461/1500] Built Mathlib.Algebra.Group.Pointwise.Finset.Basic (8.8s)
✔ [1462/1500] Built Mathlib.Data.Multiset.Sections (2.7s)
✔ [1463/1506] Built Mathlib.Algebra.Order.Hom.GroupNorm (2.3s)
✔ [1464/1508] Built Mathlib.Algebra.Order.BigOperators.GroupWithZero.List (1.8s)
✔ [1465/1509] Built Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset (2.9s)
✔ [1466/1511] Built Mathlib.Algebra.Order.BigOperators.Ring.List (2.2s)
✔ [1467/1517] Built Mathlib.Algebra.Group.Pi.Torsion (1.8s)
✔ [1468/1519] Built Mathlib.Algebra.FiniteSupport.Basic (3.2s)
✔ [1469/1519] Built Mathlib.Algebra.Order.Hom.RingNorm (1.9s)
✔ [1470/1519] Built Mathlib.Algebra.BigOperators.Ring.Multiset (2.5s)
✔ [1471/1521] Built Mathlib.Data.List.Find (1.8s)
✔ [1472/1521] Built Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset (2.3s)
✔ [1473/1523] Built Mathlib.Algebra.Module.Submodule.Equiv (4.3s)
✔ [1474/1524] Built Mathlib.Algebra.BigOperators.Group.Finset.Preimage (2.6s)
✔ [1475/1524] Built Mathlib.Data.Rat.BigOperators (2.5s)
✔ [1476/1524] Built Mathlib.Algebra.Ring.NonZeroDivisors (2.7s)
✔ [1477/1525] Built Mathlib.Algebra.Ring.Submonoid.Pointwise (3.2s)
✔ [1478/1525] Built Mathlib.Data.Multiset.Find (2.4s)
✔ [1479/1525] Built Mathlib.Algebra.Order.AbsoluteValue.Basic (3.7s)
✔ [1480/1527] Built Mathlib.Algebra.Ring.Subring.Basic (8.6s)
✔ [1481/1527] Built Mathlib.Algebra.BigOperators.Ring.Finset (3.8s)
✔ [1482/1528] Built Mathlib.Algebra.Order.BigOperators.Ring.Multiset (2.8s)
✔ [1483/1528] Built Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise (3.1s)
✔ [1484/1528] Built Mathlib.Algebra.Order.Kleene (3.6s)
✔ [1485/1531] Built Mathlib.Data.Fintype.Lattice (2.3s)
✔ [1486/1531] Built Mathlib.Data.Finsupp.Defs (3.1s)
✔ [1487/1531] Built Mathlib.Algebra.Field.IsField (2.5s)
✔ [1488/1536] Built Mathlib.RingTheory.Coprime.Basic (3.8s)
✔ [1489/1536] Built Mathlib.Data.Finset.Fin (2.9s)
✔ [1490/1536] Built Mathlib.Data.Set.Semiring (3.8s)
✔ [1491/1539] Built Mathlib.Algebra.Order.BigOperators.Ring.Finset (4.6s)
✔ [1492/1541] Built Mathlib.LinearAlgebra.Span.Basic (6.2s)
✔ [1493/1541] Built Mathlib.Algebra.Algebra.Basic (5.5s)
✔ [1494/1541] Built Mathlib.Data.Finsupp.Single (3.5s)
✔ [1495/1544] Built Mathlib.Order.Interval.Set.Fin (4.3s)
✔ [1496/1545] Built Mathlib.Data.Fintype.Order (3.6s)
✔ [1497/1545] Built Mathlib.GroupTheory.OrderOfElement (17s)
✔ [1498/1545] Built Mathlib.Algebra.Order.Interval.Set.Monoid (2.5s)
✔ [1499/1545] Built Mathlib.RingTheory.Coprime.Lemmas (3.9s)
✔ [1500/1545] Built Mathlib.Order.SuccPred.LinearLocallyFinite (4.0s)
✔ [1501/1545] Built Mathlib.Algebra.BigOperators.NatAntidiagonal (2.5s)
✔ [1502/1546] Built Mathlib.RingTheory.Ideal.Span (3.0s)
✔ [1503/1547] Built Mathlib.Data.Finsupp.Indicator (2.5s)
✔ [1504/1547] Built Mathlib.LinearAlgebra.BilinearMap (13s)
✔ [1505/1548] Built Mathlib.Algebra.Group.Finsupp (4.4s)
✔ [1506/1549] Built Mathlib.Order.PartialSups (3.6s)
✔ [1507/1549] Built Mathlib.Order.Interval.Finset.Fin (4.5s)
✔ [1508/1554] Built Mathlib.Algebra.Algebra.Hom (5.6s)
✔ [1509/1554] Built Mathlib.Algebra.Order.Interval.Finset.Basic (3.4s)
✔ [1510/1554] Built Mathlib.RingTheory.Ideal.Maximal (4.5s)
✔ [1511/1554] Built Mathlib.RingTheory.Multiplicity (5.9s)
✔ [1512/1559] Built Mathlib.Data.Finsupp.SMulWithZero (2.8s)
✔ [1513/1559] Built Mathlib.Algebra.BigOperators.Finprod (10s)
✔ [1514/1559] Built Mathlib.Data.Finsupp.Ext (2.8s)
✔ [1515/1562] Built Mathlib.Tactic.Order.CollectFacts (3.0s)
✔ [1516/1564] Built Mathlib.Data.ZMod.Basic (6.5s)
✔ [1517/1564] Built Mathlib.Algebra.Module.Submodule.Bilinear (3.8s)
✔ [1518/1564] Built Mathlib.Order.Disjointed (3.3s)
✔ [1519/1564] Built Mathlib.RingTheory.Ideal.Nonunits (2.7s)
✔ [1520/1564] Built Mathlib.Tactic.Order.Preprocessing (2.0s)
✔ [1521/1564] Built Mathlib.Tactic.Order.Graph.Basic (1.9s)
✔ [1522/1564] Built Mathlib.Order.Interval.Set.Disjoint (3.0s)
✔ [1523/1565] Built Mathlib.Tactic.Order.ToInt (2.7s)
✔ [1524/1566] Built Mathlib.Algebra.BigOperators.GroupWithZero.Action (3.0s)
✔ [1525/1570] Built Mathlib.Order.Filter.Defs (3.6s)
✔ [1526/1570] Built Mathlib.Tactic.Order.Graph.Tarjan (1.8s)
✔ [1527/1570] Built Mathlib.Algebra.Algebra.ZMod (2.7s)
✔ [1528/1570] Built Mathlib.Algebra.Order.Group.Basic (2.1s)
✔ [1529/1570] Built Mathlib.Algebra.Order.Group.Action.Synonym (1.8s)
✔ [1530/1571] Built Mathlib.Algebra.Algebra.Equiv (7.8s)
✔ [1531/1571] Built Mathlib.Algebra.BigOperators.Finsupp.Basic (5.7s)
✔ [1532/1572] Built Mathlib.Algebra.Module.BigOperators (2.6s)
✔ [1533/1574] Built Mathlib.Algebra.Algebra.NonUnitalHom (6.6s)
✔ [1534/1576] Built Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (3.6s)
✔ [1535/1576] Built Mathlib.Algebra.Order.GroupWithZero.Synonym (1.7s)
✔ [1536/1577] Built Mathlib.Algebra.Group.Fin.Tuple (2.7s)
✔ [1537/1577] Built Mathlib.LinearAlgebra.TensorProduct.Defs (6.1s)
✔ [1538/1577] Built Mathlib.Tactic.Order (3.5s)
✔ [1539/1577] Built Mathlib.Order.Filter.Basic (4.5s)
✔ [1540/1578] Built Mathlib.Algebra.Algebra.Prod (3.7s)
✔ [1541/1578] Built Mathlib.Algebra.Group.Graph (4.3s)
✔ [1542/1578] Built Mathlib.Algebra.Algebra.Opposite (4.9s)
✔ [1543/1580] Built Mathlib.Algebra.Order.GroupWithZero.Action.Synonym (2.7s)
✔ [1544/1580] Built Aeneas.Tactic.Simproc.ReduceZMod.ReduceZMod (6.0s)
✔ [1545/1580] Built Mathlib.Algebra.BigOperators.Intervals (4.9s)
✔ [1546/1585] Built Mathlib.Logic.Equiv.Fin.Basic (3.6s)
✔ [1547/1585] Built Mathlib.Order.Filter.AtTopBot.Defs (2.8s)
✔ [1548/1585] Built Mathlib.LinearAlgebra.Quotient.Defs (4.6s)
✔ [1549/1585] Built Mathlib.Order.Filter.Map (3.9s)
✔ [1550/1593] Built Mathlib.Data.Set.Finite.Lemmas (3.3s)
✔ [1551/1593] Built Mathlib.Order.Filter.AtTopBot.Disjoint (2.4s)
✔ [1552/1595] Built Mathlib.Data.Finsupp.Basic (10s)
✔ [1553/1595] Built Mathlib.Data.Nat.Choose.Sum (4.3s)
✔ [1554/1596] Built Mathlib.Order.Filter.Bases.Basic (4.1s)
✔ [1555/1596] Built Mathlib.LinearAlgebra.TensorProduct.Basic (10s)
✔ [1556/1596] Built Mathlib.Order.Filter.Tendsto (3.4s)
✔ [1557/1597] Built Mathlib.Algebra.GroupWithZero.Submonoid.Primal (3.5s)
✔ [1558/1597] Built Mathlib.Algebra.Algebra.Tower (6.5s)
✔ [1559/1597] Built Aeneas.Tactic.Solver.ScalarTac.Lemmas (8.6s)
✔ [1560/1597] Built Mathlib.GroupTheory.FreeGroup.Basic (9.4s)
✔ [1561/1600] Built Mathlib.Algebra.Order.Module.Defs (9.1s)
✔ [1562/1600] Built Mathlib.Data.Finsupp.Option (3.6s)
✔ [1563/1602] Built Mathlib.Data.Finsupp.SMul (3.5s)
✔ [1564/1610] Built Mathlib.Data.BitVec (2.4s)
✔ [1565/1611] Built Mathlib.LinearAlgebra.Prod (10s)
✔ [1566/1611] Built Mathlib.Order.Filter.AtTopBot.Tendsto (2.2s)
✔ [1567/1613] Built Mathlib.RingTheory.UniqueFactorizationDomain.Defs (2.4s)
✔ [1568/1613] Built Aeneas.Std.Scalar.BvComp (3.8s)
✔ [1569/1620] Built Mathlib.Algebra.Order.Nonneg.Module (2.6s)
✔ [1570/1624] Built Mathlib.Tactic.Algebraize (3.4s)
✔ [1571/1624] Built Batteries.Data.Nat.Bitwise.Lemmas (728ms)
✔ [1572/1624] Built Mathlib.Data.List.GetD (1.7s)
✔ [1573/1626] Built Mathlib.Order.Filter.AtTopBot.Basic (2.9s)
✔ [1574/1628] Built Batteries.Data.Nat.Bitwise (673ms)
✔ [1575/1628] Built Aeneas.Tactic.Simp.SimpLemmas (2.0s)
✔ [1576/1629] Built Aeneas.Data.ListN (1.3s)
✔ [1577/1629] Built Batteries.Data.BitVec.Basic (774ms)
✔ [1578/1629] Built Batteries.Data.Fin.OfBits (636ms)
✔ [1579/1633] Built Aeneas.Std.Scalar.CloneCopy (4.4s)
✔ [1580/1633] Built Batteries.Data.Int (723ms)
✔ [1581/1635] Built Aeneas.Std.Core.Default (2.9s)
✔ [1582/1640] Built Mathlib.LinearAlgebra.Finsupp.Defs (5.6s)
✔ [1583/1640] Built Mathlib.GroupTheory.Finiteness (6.3s)
✔ [1584/1645] Built Batteries.Data.BitVec.Lemmas (884ms)
✔ [1585/1646] Built Aeneas.Tactic.Conv.Natify.Init (1.9s)
✔ [1586/1647] Built Aeneas.Tactic.Conv.ZModify.Init (1.9s)
✔ [1587/1656] Built Mathlib.LinearAlgebra.Pi (6.5s)
✔ [1588/1657] Built Aeneas.Data.Byte (2.7s)
✔ [1589/1657] Built Mathlib.Data.Nat.Bitwise (3.3s)
✔ [1590/1659] Built Mathlib.LinearAlgebra.TensorProduct.Map (9.6s)
✔ [1591/1659] Built Aeneas.Tactic.Simproc.ReduceNat (2.6s)
✔ [1592/1659] Built Mathlib.RingTheory.Finiteness.Defs (3.1s)
✔ [1593/1659] Built Aeneas.Std.SliceDef (3.9s)
✔ [1594/1660] Built Mathlib.LinearAlgebra.Finsupp.LSum (4.4s)
✔ [1595/1660] Built Aeneas.Std.Scalar.LeadingZeros (3.5s)
✔ [1596/1661] Built Aeneas.Std.Scalar.Pow (3.6s)
✔ [1597/1661] Built Aeneas.Std.Scalar.Rotate (3.8s)
✔ [1598/1661] Built Aeneas.Std.Scalar.SaturatingOps (3.8s)
✔ [1599/1664] Built Aeneas.Std.Scalar.EqOrd (4.8s)
✔ [1600/1664] Built Aeneas.Tactic.Simp.SimpLists.SimpLists (3.6s)
✔ [1601/1669] Built Aeneas.Tactic.Simp.SimpScalar.SimpScalar (3.0s)
✔ [1602/1670] Built Aeneas.Std.Scalar.WrappingOps.Add (3.7s)
✔ [1603/1670] Built Mathlib.Algebra.Algebra.Bilinear (4.3s)
✔ [1604/1670] Built Mathlib.LinearAlgebra.Finsupp.Supported (3.3s)
✔ [1605/1677] Built Aeneas.Std.StringDef (3.8s)
✔ [1606/1677] Built Aeneas.Std.Scalar.WrappingOps.Mul (4.4s)
✔ [1607/1677] Built Mathlib.RingTheory.Finiteness.Basic (4.5s)
✔ [1608/1677] Built Aeneas.Std.Scalar.WrappingOps.Shl (4.3s)
✔ [1609/1683] Built Aeneas.Std.Scalar.WrappingOps.Shr (4.2s)
✔ [1610/1686] Built Mathlib.Control.Lawful (1.2s)
✔ [1611/1688] Built Aeneas.Std.Scalar.WrappingOps.Sub (4.4s)
✔ [1612/1691] Built Mathlib.Control.Monad.Writer (1.9s)
✔ [1613/1692] Built Aeneas.Std.RawPtr (3.9s)
✔ [1614/1692] Built Aeneas.Std.Alloc.String (2.3s)
✔ [1615/1692] Built Aeneas.Tactic.Simp.SimpScalar.Lemmas (4.9s)
✔ [1616/1694] Built Mathlib.Algebra.Module.Submodule.Finsupp (2.9s)
✔ [1617/1695] Built Aeneas.Std.Core.Atomic (2.3s)
✔ [1618/1695] Built Mathlib.RingTheory.Noetherian.Defs (2.9s)
✔ [1619/1696] Built Mathlib.Control.Monad.Cont (2.1s)
✔ [1620/1701] Built Mathlib.LinearAlgebra.Finsupp.LinearCombination (4.9s)
✔ [1621/1701] Built Aeneas.Std.Core.CoreResult (3.2s)
✔ [1622/1701] Built Aeneas.Std.Core.Panic (2.4s)
✔ [1623/1713] Built Aeneas.Std.Core.Marker (3.0s)
✔ [1624/1714] Built Aeneas.Std.Scalar.WrappingOps (3.8s)
✔ [1625/1716] Built Aeneas.Std.Core.Pin (2.3s)
✔ [1626/1719] Built Aeneas.Std.Core.Ptr (3.9s)
✔ [1627/1720] Built Aeneas.Std.PrimitivesLemmas (2.8s)
✔ [1628/1720] Built Aeneas.Tactic.Simp.SimpIfs.Init (1.7s)
✔ [1629/1720] Built Aeneas.Tactic.Simp.SimpScalar.Tests (4.1s)
✔ [1630/1721] Built Aeneas.Data.Tuples (2.5s)
✔ [1631/1722] Built Mathlib.RingTheory.Ideal.Basic (3.2s)
✔ [1632/1724] Built Aeneas.Data.Range.DivRange.Basic (2.4s)
✔ [1633/1726] Built Aeneas.Data.Fin (3.8s)
✔ [1634/1743] Built Aeneas.Data.Range.Lemmas (2.5s)
✔ [1635/1744] Built Aeneas.Do.Elab (5.1s)
✔ [1636/1746] Built Aeneas.Std.Core.Alloc (3.9s)
✔ [1637/1750] Built Aeneas.Data.Range.MulRange.Basic (2.6s)
✔ [1638/1751] Built Aeneas.Tactic.Elab.TraitDefault.Test (1.1s)
✔ [1639/1752] Built Mathlib.Algebra.Algebra.Operations (7.2s)
✔ [1640/1752] Built Aeneas.Tactic.Simp.SimpIfs.SimpIfs (4.2s)
✔ [1641/1752] Built Aeneas.Data.Range.Notations (4.2s)
✔ [1642/1752] Built Aeneas.Tactic.Misc.FCongr.FCongr (1.1s)
✔ [1643/1752] Built Aeneas.Tactic.Simp.SimpScalar (4.2s)
✔ [1644/1752] Built Aeneas.Data.Range.DivRange.Lemmas (3.4s)
✔ [1645/1752] Built Aeneas.Tactic.Misc.FApplyExact (1.9s)
✔ [1646/1754] Built Aeneas.Data.Range.SRRange.Basic (2.5s)
✔ [1647/1754] Built Aeneas.Tactic.Elab.TraitDefault (856ms)
✔ [1648/1754] Built Aeneas.Tactic.Misc.FCongr (846ms)
✔ [1649/1759] Built Aeneas.Tactic.RustAttributes (1.6s)
✔ [1650/1762] Built Aeneas.Tactic.Elab (907ms)
✔ [1651/1762] Built Aeneas.Tactic.Misc.Let.Let (2.2s)
✔ [1652/1765] Built Aeneas.Tactic.Solver.BvTac.Init (1.6s)
✔ [1653/1767] Built Aeneas.Tactic.Misc.Let (1.8s)
✔ [1654/1768] Built Aeneas.Tactic.Simp.SimpIfs (3.7s)
✔ [1655/1773] Built Aeneas.Data.Range.MulRange.Notations (3.8s)
✔ [1656/1774] Built Aeneas.Tactic.Simp.SimpBoolProp (3.5s)
✔ [1657/1777] Built Aeneas.Data.Range.DivRange.Notations (3.7s)
✔ [1658/1777] Built Aeneas.Tactic.Simp.RingEqNF.Tactic (3.3s)
✔ [1659/1779] Built Aeneas.Data.Range.MulRange.Lemmas (3.0s)
✔ [1660/1781] Built Aeneas.Data.Range.SRRange.Notations (4.0s)
✔ [1661/1783] Built Aeneas.Tactic.Solver.Grind (1.2s)
✔ [1662/1784] Built Aeneas.Tactic.Simproc.ReduceFin.Init (1.0s)
✔ [1663/1784] Built Aeneas.Tactic.Misc (2.2s)
✔ [1665/1809] Built Aeneas.Tactic.Step.InferPost (3.6s)
✔ [1666/1809] Built Aeneas.Tactic.Simproc.ReduceZMod (4.2s)
✔ [1667/1809] Built Aeneas.Data.Range.DivRange (3.7s)
✔ [1668/1809] Built Aeneas.Tactic.Simproc.ReduceFin.ReduceFin (2.3s)
✔ [1669/1809] Built Aeneas.Data.Range.MulRange (3.6s)
✔ [1670/1809] Built Aeneas.Tactic.Simp.RingEqNF.Tests (3.9s)
✔ [1671/1809] Built Mathlib.RingTheory.Ideal.Operations (8.2s)
✔ [1672/1809] Built Aeneas.Tactic.Solver.Grind.Tests (3.9s)
✔ [1673/1809] Built AeneasMeta.Split (4.3s)
✔ [1674/1809] Built Aeneas.Tactic.Simproc.ReduceFin (1.7s)
✔ [1675/1809] Built Aeneas.Tactic.Simp.RingEqNF (2.1s)
✔ [1676/1809] Built Mathlib.RingTheory.UniqueFactorizationDomain.Ideal (2.1s)
✔ [1677/1809] Built Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain (2.1s)
✔ [1678/1809] Built Mathlib.RingTheory.Ideal.Maps (4.3s)
✔ [1679/1809] Built Aeneas.Tactic.Solver.ScalarTac.Tests (7.0s)
✔ [1680/1809] Built Mathlib.RingTheory.Ideal.Prod (1.4s)
✔ [1681/1809] Built Mathlib.RingTheory.PrincipalIdealDomain (1.5s)
✔ [1682/1809] Built Mathlib.RingTheory.Int.Basic (1.3s)
✔ [1683/1809] Built Aeneas.Tactic.Solver.Arith.Lemmas (2.4s)
✔ [1684/1809] Built Aeneas.Tactic.Conv.Zify (2.2s)
✔ [1685/1809] Built Aeneas.Tactic.Solver.ScalarTac (2.3s)
✔ [1686/1809] Built Aeneas.Tactic.Solver.Arith (2.3s)
✔ [1687/1809] Built Aeneas.Tactic.Conv.Natify.Natify (2.8s)
✔ [1688/1809] Built Aeneas.Tactic.Conv.ZModify.ZModify (2.9s)
✔ [1689/1809] Built Aeneas.Std.Range (3.9s)
✔ [1690/1809] Built Aeneas.Std.Scalar.Misc (4.3s)
✔ [1691/1809] Built Aeneas.Std.Scalar.Bitwise (4.8s)
✔ [1692/1809] Built Aeneas.Tactic.Conv.Natify (4.2s)
✔ [1693/1809] Built Aeneas.Tactic.Conv.ZModify (4.1s)
✔ [1694/1809] Built Aeneas.Tactic.Step.GrindState (4.8s)
✔ [1695/1809] Built Aeneas.Tactic.Solver.ScalarDecrTac (5.1s)
✔ [1696/1809] Built Aeneas.Std.Scalar.Casts (5.4s)
✔ [1697/1809] Built Aeneas.Data.List.List (7.6s)
✔ [1698/1809] Built Aeneas.Std.Scalar.Ops.Neg (4.6s)
✔ [1699/1809] Built Aeneas.Std.Scalar.Ops.Rem (5.4s)
✔ [1700/1809] Built Aeneas.Std.Scalar.Ops.Sub (5.5s)
✔ [1701/1809] Built Aeneas.Std.Scalar.Ops.Add (5.3s)
✔ [1702/1809] Built Aeneas.Std.Scalar.Ops.Mul (5.6s)
✔ [1703/1809] Built Aeneas.Std.Scalar.Ops.Div (6.7s)
✔ [1704/1809] Built Aeneas.Data.List (4.0s)
✔ [1705/1809] Built Aeneas.Std.Array.Core (5.2s)
✔ [1706/1809] Built Aeneas.Data.Range.SRRange.Lemmas (6.0s)
✔ [1707/1809] Built Aeneas.Std.Scalar.CheckedOps.Rem (5.2s)
✔ [1708/1809] Built Aeneas.Std.Scalar.CheckedOps.Sub (6.0s)
✔ [1709/1809] Built Aeneas.Std.Scalar.CheckedOps.Add (6.2s)
✔ [1710/1809] Built Aeneas.Std.Scalar.CheckedOps.Mul (5.9s)
✔ [1711/1809] Built Aeneas.Std.Scalar.Notations (6.7s)
✔ [1712/1809] Built Aeneas.Std.Scalar.Ops (5.3s)
✔ [1713/1809] Built Aeneas.Std.Scalar.CheckedOps.Div (5.0s)
✔ [1714/1809] Built Aeneas.Data.Array (6.1s)
✔ [1715/1809] Built Aeneas.Std.Array.Array (7.9s)
✔ [1716/1809] Built Aeneas.Data.Range.SRRange (5.9s)
✔ [1717/1809] Built Aeneas.Data.BitVec (9.4s)
✔ [1718/1809] Built Aeneas.Std.Scalar.Default (5.0s)
✔ [1719/1809] Built Aeneas.Data.Discriminant (7.2s)
✔ [1720/1809] Built Aeneas.Std.Scalar.OverflowingOps.Mul (7.6s)
✔ [1721/1809] Built Aeneas.Std.Slice (10s)
✔ [1722/1809] Built Aeneas.Std.Scalar.OverflowingOps.Sub (8.6s)
✔ [1723/1809] Built Aeneas.Std.Scalar.OverflowingOps.Div (6.5s)
✔ [1724/1809] Built Aeneas.Std.Scalar.CheckedOps (4.9s)
✔ [1725/1809] Built Aeneas.Std.Core.Fmt (4.9s)
✔ [1726/1809] Built Aeneas.Data.Vector (5.9s)
✔ [1727/1809] Built Aeneas.Data.Range (4.7s)
✔ [1728/1809] Built Aeneas.Std.Scalar.OverflowingOps.Add (11s)
✔ [1729/1809] Built Aeneas.Std.Core.Hash (5.4s)
✔ [1730/1809] Built Aeneas.Std.Scalar.CoreConvertNum (7.7s)
✔ [1731/1809] Built Aeneas.Std.Std.Io (5.1s)
✔ [1732/1809] Built Aeneas.Std.Core.Error (5.2s)
✔ [1733/1809] Built Aeneas.Std.Scalar.Fmt (5.4s)
✔ [1734/1809] Built Aeneas.Std.Scalar.Display (5.1s)
✔ [1735/1809] Built Aeneas.Std.Array.ArrayDebug (4.7s)
✔ [1736/1809] Built Aeneas.Std.Array.ArraySlice (6.4s)
✔ [1737/1809] Built Aeneas.Std.Core.Iter (6.9s)
✔ [1738/1809] Built Aeneas.Tactic.Setup (4.9s)
✔ [1739/1809] Built Aeneas.Data (3.9s)
✔ [1740/1809] Built Aeneas.Std.Scalar.OverflowingOps (3.6s)
✔ [1741/1809] Built Aeneas.Std.Core.Discriminant (3.5s)
✔ [1742/1809] Built Aeneas.Std.Std (3.3s)
✔ [1743/1809] Built Aeneas.Std.Array (2.8s)
✔ [1744/1809] Built Aeneas.Std.Scalar (2.2s)
✔ [1745/1809] Built Aeneas.Std.SliceIter (4.1s)
✔ [1746/1809] Built Aeneas.Std.Target (3.4s)
✔ [1747/1809] Built Aeneas.Std.String (3.7s)
✔ [1748/1809] Built Aeneas.Std.Alloc.Vec (4.9s)
✔ [1749/1809] Built Aeneas.Std.RangeIter (5.6s)
✔ [1750/1809] Built Aeneas.Std.Core.FmtWithSlice (3.9s)
✔ [1751/1809] Built Aeneas.Std.Core.CoreOption (4.1s)
✔ [1752/1809] Built Aeneas.Std.StringIter (4.3s)
✔ [1753/1809] Built Aeneas.Std.Alloc.Vec.IntoIter (3.6s)
✔ [1754/1809] Built Aeneas.Std.Alloc.Slice (3.6s)
✔ [1755/1809] Built Aeneas.Std.Core (2.6s)
✔ [1756/1809] Built Aeneas.Tactic.Conv.Bvify.Bvify (10s)
✔ [1757/1809] Built Aeneas.Std.Alloc (2.5s)
✔ [1758/1809] Built Aeneas.Std (2.6s)
✔ [1759/1809] Built Aeneas.Tactic.Conv.Bvify.Lemmas (3.5s)
✔ [1760/1809] Built Aeneas.Tactic.Conv.Bvify (2.0s)
✔ [1761/1809] Built Aeneas.Tactic.Conv.Bvify.Tests (3.5s)
✔ [1762/1809] Built Aeneas.Do.Delab (3.9s)
✔ [1763/1809] Built Aeneas.Tactic.Simp.SimpLists.Tests (6.6s)
✔ [1764/1809] Built Aeneas.Tactic.Conv (4.4s)
✔ [1765/1809] Built Aeneas.Command.Decompose.TestsRec (4.9s)
✔ [1766/1809] Built Aeneas.Do.Tests (5.5s)
✔ [1767/1809] Built Aeneas.Tactic.Simp.SimpLists (3.3s)
✔ [1768/1809] Built Aeneas.Command.Decompose.Tests (8.0s)
✔ [1769/1809] Built Aeneas.Tactic.Simp.SimpListsScalar (2.8s)
✔ [1770/1809] Built Aeneas.Do (3.5s)
✔ [1771/1809] Built Aeneas.Tactic.Simp (2.6s)
✔ [1772/1809] Built Aeneas.Command.Decompose.TestsBig (17s)
✔ [1773/1809] Built Aeneas.Command (1.7s)
✔ [1774/1809] Built Aeneas.Tactic.Step.Step (10s)
✔ [1775/1809] Built Aeneas.Tactic.Solver.BvTac.BvTac (20s)
✔ [1776/1809] Built Aeneas.Tactic.Step.Tests.DspecInduction (4.1s)
✔ [1777/1809] Built Aeneas.Tactic.Step.StepArraySpec (4.7s)
✔ [1778/1809] Built Aeneas.Tactic.Simproc.BvSimprocs (4.2s)
✔ [1779/1809] Built Aeneas.Tactic.Simproc (3.2s)
✔ [1780/1809] Built Aeneas.Tactic.Step.StepStar (9.0s)
✔ [1781/1809] Built Aeneas.Tactic.Solver.BvTac.Lemmas (9.7s)
✔ [1782/1809] Built Aeneas.Tactic.Step.Deprecated (5.2s)
✔ [1783/1809] Built Aeneas.Tactic.Solver.BvTac.Tests (14s)
✔ [1784/1809] Built Aeneas.Tactic.Solver.BvTac (5.2s)
✔ [1785/1809] Built Aeneas.Tactic.Step (6.2s)
✔ [1786/1809] Built Aeneas.Tactic.Solver (7.0s)
✔ [1787/1809] Built Aeneas.Tactic.Step.Tests.MvcgenSpec (10s)
✔ [1788/1809] Built Aeneas.Tactic.Step.Tests.MaxRecDepthMetavar (11s)
✔ [1789/1809] Built Aeneas.Tactic.Step.Tests.UncurryBind (12s)
✔ [1790/1809] Built Aeneas.Tactic.Step.Tests.TupleDestruct (12s)
✔ [1791/1809] Built Aeneas.Tactic.Step.Tests.IntroOutputsRecursion (12s)
✔ [1792/1809] Built Aeneas.Tactic.Step.Tests.SpecParameters (9.0s)
✔ [1793/1809] Built Aeneas.Tactic.Step.Tests.HigherOrderOption (13s)
✔ [1794/1809] Built Aeneas.Tactic.Step.Tests.Coin (13s)
✔ [1795/1809] Built Aeneas.Tactic.Step.Tests.IntroOutputs (17s)
✔ [1796/1809] Built Aeneas.Tactic.Step.Tests.HigherOrder (18s)
✔ [1797/1809] Built Aeneas.Tactic.Step.Tests.ParserErrors (8.5s)
✔ [1798/1809] Built Aeneas.Tactic.Step.Tests.DischargeTactic (8.3s)
✔ [1799/1809] Built Aeneas.Tactic.Step.Tests.Triple (8.4s)
✔ [1800/1809] Built Aeneas.Tactic.Step.Tests (4.6s)
✔ [1801/1809] Built Aeneas.Tactic.Tests (620ms)
✔ [1802/1809] Built Aeneas.Tactic (5.8s)
✔ [1803/1809] Built Aeneas (6.2s)
✔ [1804/1809] Built CloneFrom0.Anchors (12s)
✔ [1805/1809] Built CloneFrom1.Anchors (12s)
✔ [1806/1809] Built CloneFrom16.Anchors (12s)
✔ [1807/1809] Built Anchors (14s)
✔ [1808/1809] Built CrcProofs.TableCloneFrom (65s)
✔ [1809/1809] Built CrcProofs.Table (64s)
Build completed successfully (1809 jobs).
$ lake env lean --stdin (proofs.rs formal extraction and axiom audit)
proofs.rs:formal:{"axioms":["propext","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"self","type":"TableCloneFrom0.crc.Table0","type_segments":[{"ref":"TableCloneFrom0.crc.Table0","text":"TableCloneFrom0.crc.Table0"}]},{"binder":"explicit","kind":"variable","name":"source","type":"TableCloneFrom0.crc.Table0","type_segments":[{"ref":"TableCloneFrom0.crc.Table0","text":"TableCloneFrom0.crc.Table0"}]}],"conclusion":"∃ out, TableCloneFrom0.core.clone.Clone.clone_from.default self source = Aeneas.Std.Result.ok out ∧ out = source","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"TableCloneFrom0.core.clone.Clone.clone_from.default","text":"TableCloneFrom0.core.clone.Clone.clone_from.default"},{"text":" "},{"text":"self"},{"text":" "},{"text":"source"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"source"}],"definitions":[{"module":"CloneFrom0.Anchors","name":"TableCloneFrom0.crc.Table0","source":{"first_line":23,"last_line":28}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"CloneFrom0.Anchors","name":"TableCloneFrom0.core.clone.Clone.clone_from.default","source":{"first_line":39,"last_line":46}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}}],"definitions_truncated":false,"first_line":7,"last_line":10,"module":"CrcProofs.TableCloneFrom","program":null,"program_head":null,"statement":"∀ (self source : TableCloneFrom0.crc.Table0),\n @Exists.{1} TableCloneFrom0.crc.Table0 fun (out : TableCloneFrom0.crc.Table0) =>\n And\n (@Eq.{1} (Aeneas.Std.Result.{0} TableCloneFrom0.crc.Table0)\n (TableCloneFrom0.core.clone.Clone.clone_from.default self source)\n (@Aeneas.Std.Result.ok.{0} TableCloneFrom0.crc.Table0 out))\n (@Eq.{1} TableCloneFrom0.crc.Table0 out source)","theorem":"CrcProofs.table_clone_from_l0_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"c","type":"crc_mono_anchors.crc.CrcU8Table1","type_segments":[{"ref":"crc_mono_anchors.crc.CrcU8Table1","text":"crc_mono_anchors.crc.CrcU8Table1"}]}],"conclusion":"∃ out, crc_mono_anchors.crc.crc8.CrcU8Table1.table1 c = Aeneas.Std.Result.ok out ∧ out = c.data","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"crc_mono_anchors.crc.crc8.CrcU8Table1.table1","text":"crc_mono_anchors.crc.crc8.CrcU8Table1.table1"},{"text":" "},{"text":"c"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"c"},{"text":"."},{"ref":"crc_mono_anchors.crc.CrcU8Table1.data","text":"data"}],"definitions":[{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU8Table1","source":{"first_line":358,"last_line":365}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Aeneas.Std.Array.Array","name":"Aeneas.Std.Array","source":{"first_line":28,"last_line":30}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U8","source":{"first_line":669,"last_line":669}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize.ofNat","source":{"first_line":703,"last_line":703}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table0._proof_1","source":null},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table1._proof_1","source":null},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Anchors","name":"crc_mono_anchors.crc.crc8.CrcU8Table1.table1","source":{"first_line":367,"last_line":376}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU8Table1.data","source":{"first_line":365,"last_line":365}}],"definitions_truncated":false,"first_line":11,"last_line":14,"module":"CrcProofs.Table","program":null,"program_head":null,"statement":"∀ (c : crc_mono_anchors.crc.CrcU8Table1),\n @Exists.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U8\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1))\n fun\n (out :\n Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U8\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1)) =>\n And\n (@Eq.{1}\n (Aeneas.Std.Result.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U8\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1)))\n (crc_mono_anchors.crc.crc8.CrcU8Table1.table1 c)\n (@Aeneas.Std.Result.ok.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U8\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1))\n out))\n (@Eq.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U8\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1))\n out (crc_mono_anchors.crc.CrcU8Table1.data c))","theorem":"CrcProofs.table_u8_l1_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"c","type":"crc_mono_anchors.crc.CrcU128Table16","type_segments":[{"ref":"crc_mono_anchors.crc.CrcU128Table16","text":"crc_mono_anchors.crc.CrcU128Table16"}]}],"conclusion":"∃ out, crc_mono_anchors.crc.crc128.CrcU128Table16.table16 c = Aeneas.Std.Result.ok out ∧ out = c.data","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"crc_mono_anchors.crc.crc128.CrcU128Table16.table16","text":"crc_mono_anchors.crc.crc128.CrcU128Table16.table16"},{"text":" "},{"text":"c"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"c"},{"text":"."},{"ref":"crc_mono_anchors.crc.CrcU128Table16.data","text":"data"}],"definitions":[{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table16","source":{"first_line":78,"last_line":85}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Aeneas.Std.Array.Array","name":"Aeneas.Std.Array","source":{"first_line":28,"last_line":30}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U128","source":{"first_line":673,"last_line":673}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize.ofNat","source":{"first_line":703,"last_line":703}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table0._proof_1","source":null},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table16._proof_1","source":null},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Anchors","name":"crc_mono_anchors.crc.crc128.CrcU128Table16.table16","source":{"first_line":87,"last_line":96}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table16.data","source":{"first_line":85,"last_line":85}}],"definitions_truncated":false,"first_line":76,"last_line":79,"module":"CrcProofs.Table","program":null,"program_head":null,"statement":"∀ (c : crc_mono_anchors.crc.CrcU128Table16),\n @Exists.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U128\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1))\n fun\n (out :\n Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U128\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1)) =>\n And\n (@Eq.{1}\n (Aeneas.Std.Result.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U128\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1)))\n (crc_mono_anchors.crc.crc128.CrcU128Table16.table16 c)\n (@Aeneas.Std.Result.ok.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U128\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1))\n out))\n (@Eq.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U128\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1))\n out (crc_mono_anchors.crc.CrcU128Table16.data c))","theorem":"CrcProofs.table_u128_l16_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"c","type":"crc_mono_anchors.crc.CrcU16Table0","type_segments":[{"ref":"crc_mono_anchors.crc.CrcU16Table0","text":"crc_mono_anchors.crc.CrcU16Table0"}]}],"conclusion":"∃ out, crc_mono_anchors.crc.crc16.CrcU16Table0.table0 c = Aeneas.Std.Result.ok out ∧ out = c.data","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"crc_mono_anchors.crc.crc16.CrcU16Table0.table0","text":"crc_mono_anchors.crc.crc16.CrcU16Table0.table0"},{"text":" "},{"text":"c"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"c"},{"text":"."},{"ref":"crc_mono_anchors.crc.CrcU16Table0.data","text":"data"}],"definitions":[{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU16Table0","source":{"first_line":113,"last_line":120}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Aeneas.Std.Array.Array","name":"Aeneas.Std.Array","source":{"first_line":28,"last_line":30}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U16","source":{"first_line":670,"last_line":670}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize.ofNat","source":{"first_line":703,"last_line":703}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table0._proof_1","source":null},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table0._proof_2","source":null},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Anchors","name":"crc_mono_anchors.crc.crc16.CrcU16Table0.table0","source":{"first_line":122,"last_line":131}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU16Table0.data","source":{"first_line":120,"last_line":120}}],"definitions_truncated":false,"first_line":21,"last_line":24,"module":"CrcProofs.Table","program":null,"program_head":null,"statement":"∀ (c : crc_mono_anchors.crc.CrcU16Table0),\n @Exists.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U16\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2))\n fun\n (out :\n Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U16\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2)) =>\n And\n (@Eq.{1}\n (Aeneas.Std.Result.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U16\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2)))\n (crc_mono_anchors.crc.crc16.CrcU16Table0.table0 c)\n (@Aeneas.Std.Result.ok.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U16\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2))\n out))\n (@Eq.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U16\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2))\n out (crc_mono_anchors.crc.CrcU16Table0.data c))","theorem":"CrcProofs.table_u16_l0_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"c","type":"crc_mono_anchors.crc.CrcU64Table16","type_segments":[{"ref":"crc_mono_anchors.crc.CrcU64Table16","text":"crc_mono_anchors.crc.CrcU64Table16"}]}],"conclusion":"∃ out, crc_mono_anchors.crc.crc64.CrcU64Table16.table16 c = Aeneas.Std.Result.ok out ∧ out = c.data","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"crc_mono_anchors.crc.crc64.CrcU64Table16.table16","text":"crc_mono_anchors.crc.crc64.CrcU64Table16.table16"},{"text":" "},{"text":"c"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"c"},{"text":"."},{"ref":"crc_mono_anchors.crc.CrcU64Table16.data","text":"data"}],"definitions":[{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU64Table16","source":{"first_line":303,"last_line":310}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Aeneas.Std.Array.Array","name":"Aeneas.Std.Array","source":{"first_line":28,"last_line":30}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U64","source":{"first_line":672,"last_line":672}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize.ofNat","source":{"first_line":703,"last_line":703}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table0._proof_1","source":null},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table16._proof_1","source":null},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Anchors","name":"crc_mono_anchors.crc.crc64.CrcU64Table16.table16","source":{"first_line":312,"last_line":321}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU64Table16.data","source":{"first_line":310,"last_line":310}}],"definitions_truncated":false,"first_line":61,"last_line":64,"module":"CrcProofs.Table","program":null,"program_head":null,"statement":"∀ (c : crc_mono_anchors.crc.CrcU64Table16),\n @Exists.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U64\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1))\n fun\n (out :\n Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U64\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1)) =>\n And\n (@Eq.{1}\n (Aeneas.Std.Result.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U64\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1)))\n (crc_mono_anchors.crc.crc64.CrcU64Table16.table16 c)\n (@Aeneas.Std.Result.ok.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U64\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1))\n out))\n (@Eq.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U64\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1))\n out (crc_mono_anchors.crc.CrcU64Table16.data c))","theorem":"CrcProofs.table_u64_l16_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"c","type":"crc_mono_anchors.crc.CrcU128Table1","type_segments":[{"ref":"crc_mono_anchors.crc.CrcU128Table1","text":"crc_mono_anchors.crc.CrcU128Table1"}]}],"conclusion":"∃ out, crc_mono_anchors.crc.crc128.CrcU128Table1.table1 c = Aeneas.Std.Result.ok out ∧ out = c.data","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"crc_mono_anchors.crc.crc128.CrcU128Table1.table1","text":"crc_mono_anchors.crc.crc128.CrcU128Table1.table1"},{"text":" "},{"text":"c"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"c"},{"text":"."},{"ref":"crc_mono_anchors.crc.CrcU128Table1.data","text":"data"}],"definitions":[{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table1","source":{"first_line":58,"last_line":65}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Aeneas.Std.Array.Array","name":"Aeneas.Std.Array","source":{"first_line":28,"last_line":30}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U128","source":{"first_line":673,"last_line":673}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize.ofNat","source":{"first_line":703,"last_line":703}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table0._proof_1","source":null},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table1._proof_1","source":null},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Anchors","name":"crc_mono_anchors.crc.crc128.CrcU128Table1.table1","source":{"first_line":67,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table1.data","source":{"first_line":65,"last_line":65}}],"definitions_truncated":false,"first_line":71,"last_line":74,"module":"CrcProofs.Table","program":null,"program_head":null,"statement":"∀ (c : crc_mono_anchors.crc.CrcU128Table1),\n @Exists.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U128\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1))\n fun\n (out :\n Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U128\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1)) =>\n And\n (@Eq.{1}\n (Aeneas.Std.Result.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U128\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1)))\n (crc_mono_anchors.crc.crc128.CrcU128Table1.table1 c)\n (@Aeneas.Std.Result.ok.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U128\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1))\n out))\n (@Eq.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U128\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1))\n out (crc_mono_anchors.crc.CrcU128Table1.data c))","theorem":"CrcProofs.table_u128_l1_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"self","type":"TableCloneFrom1.crc.Table1","type_segments":[{"ref":"TableCloneFrom1.crc.Table1","text":"TableCloneFrom1.crc.Table1"}]},{"binder":"explicit","kind":"variable","name":"source","type":"TableCloneFrom1.crc.Table1","type_segments":[{"ref":"TableCloneFrom1.crc.Table1","text":"TableCloneFrom1.crc.Table1"}]}],"conclusion":"∃ out, TableCloneFrom1.core.clone.Clone.clone_from.default self source = Aeneas.Std.Result.ok out ∧ out = source","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"TableCloneFrom1.core.clone.Clone.clone_from.default","text":"TableCloneFrom1.core.clone.Clone.clone_from.default"},{"text":" "},{"text":"self"},{"text":" "},{"text":"source"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"source"}],"definitions":[{"module":"CloneFrom1.Anchors","name":"TableCloneFrom1.crc.Table1","source":{"first_line":23,"last_line":28}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"CloneFrom1.Anchors","name":"TableCloneFrom1.core.clone.Clone.clone_from.default","source":{"first_line":39,"last_line":46}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}}],"definitions_truncated":false,"first_line":12,"last_line":15,"module":"CrcProofs.TableCloneFrom","program":null,"program_head":null,"statement":"∀ (self source : TableCloneFrom1.crc.Table1),\n @Exists.{1} TableCloneFrom1.crc.Table1 fun (out : TableCloneFrom1.crc.Table1) =>\n And\n (@Eq.{1} (Aeneas.Std.Result.{0} TableCloneFrom1.crc.Table1)\n (TableCloneFrom1.core.clone.Clone.clone_from.default self source)\n (@Aeneas.Std.Result.ok.{0} TableCloneFrom1.crc.Table1 out))\n (@Eq.{1} TableCloneFrom1.crc.Table1 out source)","theorem":"CrcProofs.table_clone_from_l1_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"c","type":"crc_mono_anchors.crc.CrcU16Table16","type_segments":[{"ref":"crc_mono_anchors.crc.CrcU16Table16","text":"crc_mono_anchors.crc.CrcU16Table16"}]}],"conclusion":"∃ out, crc_mono_anchors.crc.crc16.CrcU16Table16.table16 c = Aeneas.Std.Result.ok out ∧ out = c.data","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"crc_mono_anchors.crc.crc16.CrcU16Table16.table16","text":"crc_mono_anchors.crc.crc16.CrcU16Table16.table16"},{"text":" "},{"text":"c"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"c"},{"text":"."},{"ref":"crc_mono_anchors.crc.CrcU16Table16.data","text":"data"}],"definitions":[{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU16Table16","source":{"first_line":153,"last_line":160}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Aeneas.Std.Array.Array","name":"Aeneas.Std.Array","source":{"first_line":28,"last_line":30}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U16","source":{"first_line":670,"last_line":670}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize.ofNat","source":{"first_line":703,"last_line":703}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table0._proof_1","source":null},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table16._proof_1","source":null},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Anchors","name":"crc_mono_anchors.crc.crc16.CrcU16Table16.table16","source":{"first_line":162,"last_line":171}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU16Table16.data","source":{"first_line":160,"last_line":160}}],"definitions_truncated":false,"first_line":31,"last_line":34,"module":"CrcProofs.Table","program":null,"program_head":null,"statement":"∀ (c : crc_mono_anchors.crc.CrcU16Table16),\n @Exists.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U16\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1))\n fun\n (out :\n Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U16\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1)) =>\n And\n (@Eq.{1}\n (Aeneas.Std.Result.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U16\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1)))\n (crc_mono_anchors.crc.crc16.CrcU16Table16.table16 c)\n (@Aeneas.Std.Result.ok.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U16\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1))\n out))\n (@Eq.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U16\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1))\n out (crc_mono_anchors.crc.CrcU16Table16.data c))","theorem":"CrcProofs.table_u16_l16_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"c","type":"crc_mono_anchors.crc.CrcU8Table16","type_segments":[{"ref":"crc_mono_anchors.crc.CrcU8Table16","text":"crc_mono_anchors.crc.CrcU8Table16"}]}],"conclusion":"∃ out, crc_mono_anchors.crc.crc8.CrcU8Table16.table16 c = Aeneas.Std.Result.ok out ∧ out = c.data","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"crc_mono_anchors.crc.crc8.CrcU8Table16.table16","text":"crc_mono_anchors.crc.crc8.CrcU8Table16.table16"},{"text":" "},{"text":"c"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"c"},{"text":"."},{"ref":"crc_mono_anchors.crc.CrcU8Table16.data","text":"data"}],"definitions":[{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU8Table16","source":{"first_line":378,"last_line":385}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Aeneas.Std.Array.Array","name":"Aeneas.Std.Array","source":{"first_line":28,"last_line":30}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U8","source":{"first_line":669,"last_line":669}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize.ofNat","source":{"first_line":703,"last_line":703}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table0._proof_1","source":null},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table16._proof_1","source":null},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Anchors","name":"crc_mono_anchors.crc.crc8.CrcU8Table16.table16","source":{"first_line":387,"last_line":396}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU8Table16.data","source":{"first_line":385,"last_line":385}}],"definitions_truncated":false,"first_line":16,"last_line":19,"module":"CrcProofs.Table","program":null,"program_head":null,"statement":"∀ (c : crc_mono_anchors.crc.CrcU8Table16),\n @Exists.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U8\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1))\n fun\n (out :\n Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U8\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1)) =>\n And\n (@Eq.{1}\n (Aeneas.Std.Result.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U8\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1)))\n (crc_mono_anchors.crc.crc8.CrcU8Table16.table16 c)\n (@Aeneas.Std.Result.ok.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U8\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1))\n out))\n (@Eq.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U8\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1))\n out (crc_mono_anchors.crc.CrcU8Table16.data c))","theorem":"CrcProofs.table_u8_l16_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"c","type":"crc_mono_anchors.crc.CrcU32Table16","type_segments":[{"ref":"crc_mono_anchors.crc.CrcU32Table16","text":"crc_mono_anchors.crc.CrcU32Table16"}]}],"conclusion":"∃ out, crc_mono_anchors.crc.crc32.CrcU32Table16.table16 c = Aeneas.Std.Result.ok out ∧ out = c.data","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"crc_mono_anchors.crc.crc32.CrcU32Table16.table16","text":"crc_mono_anchors.crc.crc32.CrcU32Table16.table16"},{"text":" "},{"text":"c"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"c"},{"text":"."},{"ref":"crc_mono_anchors.crc.CrcU32Table16.data","text":"data"}],"definitions":[{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU32Table16","source":{"first_line":228,"last_line":235}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Aeneas.Std.Array.Array","name":"Aeneas.Std.Array","source":{"first_line":28,"last_line":30}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U32","source":{"first_line":671,"last_line":671}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize.ofNat","source":{"first_line":703,"last_line":703}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table0._proof_1","source":null},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table16._proof_1","source":null},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Anchors","name":"crc_mono_anchors.crc.crc32.CrcU32Table16.table16","source":{"first_line":237,"last_line":246}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU32Table16.data","source":{"first_line":235,"last_line":235}}],"definitions_truncated":false,"first_line":46,"last_line":49,"module":"CrcProofs.Table","program":null,"program_head":null,"statement":"∀ (c : crc_mono_anchors.crc.CrcU32Table16),\n @Exists.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U32\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1))\n fun\n (out :\n Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U32\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1)) =>\n And\n (@Eq.{1}\n (Aeneas.Std.Result.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U32\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1)))\n (crc_mono_anchors.crc.crc32.CrcU32Table16.table16 c)\n (@Aeneas.Std.Result.ok.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U32\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1))\n out))\n (@Eq.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U32\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 16) (instOfNatNat (nat_lit 16)))\n crc_mono_anchors.crc.CrcU128Table16._proof_1))\n out (crc_mono_anchors.crc.CrcU32Table16.data c))","theorem":"CrcProofs.table_u32_l16_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"t","type":"crc_mono_anchors.crc.Table1","type_segments":[{"ref":"crc_mono_anchors.crc.Table1","text":"crc_mono_anchors.crc.Table1"}]}],"conclusion":"∃ out, crc_mono_anchors.crc.Table1.Insts.CoreCloneClone.clone t = Aeneas.Std.Result.ok out ∧ out = t","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"crc_mono_anchors.crc.Table1.Insts.CoreCloneClone.clone","text":"crc_mono_anchors.crc.Table1.Insts.CoreCloneClone.clone"},{"text":" "},{"text":"t"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"t"}],"definitions":[{"module":"Anchors","name":"crc_mono_anchors.crc.Table1","source":{"first_line":414,"last_line":419}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Anchors","name":"crc_mono_anchors.crc.Table1.Insts.CoreCloneClone.clone","source":{"first_line":421,"last_line":428}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}}],"definitions_truncated":false,"first_line":86,"last_line":88,"module":"CrcProofs.Table","program":null,"program_head":null,"statement":"∀ (t : crc_mono_anchors.crc.Table1),\n @Exists.{1} crc_mono_anchors.crc.Table1 fun (out : crc_mono_anchors.crc.Table1) =>\n And\n (@Eq.{1} (Aeneas.Std.Result.{0} crc_mono_anchors.crc.Table1)\n (crc_mono_anchors.crc.Table1.Insts.CoreCloneClone.clone t)\n (@Aeneas.Std.Result.ok.{0} crc_mono_anchors.crc.Table1 out))\n (@Eq.{1} crc_mono_anchors.crc.Table1 out t)","theorem":"CrcProofs.table_clone_l1_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"c","type":"crc_mono_anchors.crc.CrcU8Table0","type_segments":[{"ref":"crc_mono_anchors.crc.CrcU8Table0","text":"crc_mono_anchors.crc.CrcU8Table0"}]}],"conclusion":"∃ out, crc_mono_anchors.crc.crc8.CrcU8Table0.table0 c = Aeneas.Std.Result.ok out ∧ out = c.data","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"crc_mono_anchors.crc.crc8.CrcU8Table0.table0","text":"crc_mono_anchors.crc.crc8.CrcU8Table0.table0"},{"text":" "},{"text":"c"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"c"},{"text":"."},{"ref":"crc_mono_anchors.crc.CrcU8Table0.data","text":"data"}],"definitions":[{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU8Table0","source":{"first_line":338,"last_line":345}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Aeneas.Std.Array.Array","name":"Aeneas.Std.Array","source":{"first_line":28,"last_line":30}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U8","source":{"first_line":669,"last_line":669}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize.ofNat","source":{"first_line":703,"last_line":703}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table0._proof_1","source":null},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table0._proof_2","source":null},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Anchors","name":"crc_mono_anchors.crc.crc8.CrcU8Table0.table0","source":{"first_line":347,"last_line":356}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU8Table0.data","source":{"first_line":345,"last_line":345}}],"definitions_truncated":false,"first_line":6,"last_line":9,"module":"CrcProofs.Table","program":null,"program_head":null,"statement":"∀ (c : crc_mono_anchors.crc.CrcU8Table0),\n @Exists.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U8\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2))\n fun\n (out :\n Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U8\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2)) =>\n And\n (@Eq.{1}\n (Aeneas.Std.Result.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U8\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2)))\n (crc_mono_anchors.crc.crc8.CrcU8Table0.table0 c)\n (@Aeneas.Std.Result.ok.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U8\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2))\n out))\n (@Eq.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U8\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2))\n out (crc_mono_anchors.crc.CrcU8Table0.data c))","theorem":"CrcProofs.table_u8_l0_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"c","type":"crc_mono_anchors.crc.CrcU64Table0","type_segments":[{"ref":"crc_mono_anchors.crc.CrcU64Table0","text":"crc_mono_anchors.crc.CrcU64Table0"}]}],"conclusion":"∃ out, crc_mono_anchors.crc.crc64.CrcU64Table0.table0 c = Aeneas.Std.Result.ok out ∧ out = c.data","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"crc_mono_anchors.crc.crc64.CrcU64Table0.table0","text":"crc_mono_anchors.crc.crc64.CrcU64Table0.table0"},{"text":" "},{"text":"c"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"c"},{"text":"."},{"ref":"crc_mono_anchors.crc.CrcU64Table0.data","text":"data"}],"definitions":[{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU64Table0","source":{"first_line":263,"last_line":270}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Aeneas.Std.Array.Array","name":"Aeneas.Std.Array","source":{"first_line":28,"last_line":30}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U64","source":{"first_line":672,"last_line":672}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize.ofNat","source":{"first_line":703,"last_line":703}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table0._proof_1","source":null},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table0._proof_2","source":null},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Anchors","name":"crc_mono_anchors.crc.crc64.CrcU64Table0.table0","source":{"first_line":272,"last_line":281}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU64Table0.data","source":{"first_line":270,"last_line":270}}],"definitions_truncated":false,"first_line":51,"last_line":54,"module":"CrcProofs.Table","program":null,"program_head":null,"statement":"∀ (c : crc_mono_anchors.crc.CrcU64Table0),\n @Exists.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U64\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2))\n fun\n (out :\n Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U64\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2)) =>\n And\n (@Eq.{1}\n (Aeneas.Std.Result.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U64\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2)))\n (crc_mono_anchors.crc.crc64.CrcU64Table0.table0 c)\n (@Aeneas.Std.Result.ok.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U64\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2))\n out))\n (@Eq.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U64\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2))\n out (crc_mono_anchors.crc.CrcU64Table0.data c))","theorem":"CrcProofs.table_u64_l0_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"t","type":"crc_mono_anchors.crc.Table0","type_segments":[{"ref":"crc_mono_anchors.crc.Table0","text":"crc_mono_anchors.crc.Table0"}]}],"conclusion":"∃ out, crc_mono_anchors.crc.Table0.Insts.CoreCloneClone.clone t = Aeneas.Std.Result.ok out ∧ out = t","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"crc_mono_anchors.crc.Table0.Insts.CoreCloneClone.clone","text":"crc_mono_anchors.crc.Table0.Insts.CoreCloneClone.clone"},{"text":" "},{"text":"t"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"t"}],"definitions":[{"module":"Anchors","name":"crc_mono_anchors.crc.Table0","source":{"first_line":398,"last_line":403}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Anchors","name":"crc_mono_anchors.crc.Table0.Insts.CoreCloneClone.clone","source":{"first_line":405,"last_line":412}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}}],"definitions_truncated":false,"first_line":82,"last_line":84,"module":"CrcProofs.Table","program":null,"program_head":null,"statement":"∀ (t : crc_mono_anchors.crc.Table0),\n @Exists.{1} crc_mono_anchors.crc.Table0 fun (out : crc_mono_anchors.crc.Table0) =>\n And\n (@Eq.{1} (Aeneas.Std.Result.{0} crc_mono_anchors.crc.Table0)\n (crc_mono_anchors.crc.Table0.Insts.CoreCloneClone.clone t)\n (@Aeneas.Std.Result.ok.{0} crc_mono_anchors.crc.Table0 out))\n (@Eq.{1} crc_mono_anchors.crc.Table0 out t)","theorem":"CrcProofs.table_clone_l0_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"c","type":"crc_mono_anchors.crc.CrcU16Table1","type_segments":[{"ref":"crc_mono_anchors.crc.CrcU16Table1","text":"crc_mono_anchors.crc.CrcU16Table1"}]}],"conclusion":"∃ out, crc_mono_anchors.crc.crc16.CrcU16Table1.table1 c = Aeneas.Std.Result.ok out ∧ out = c.data","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"crc_mono_anchors.crc.crc16.CrcU16Table1.table1","text":"crc_mono_anchors.crc.crc16.CrcU16Table1.table1"},{"text":" "},{"text":"c"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"c"},{"text":"."},{"ref":"crc_mono_anchors.crc.CrcU16Table1.data","text":"data"}],"definitions":[{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU16Table1","source":{"first_line":133,"last_line":140}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Aeneas.Std.Array.Array","name":"Aeneas.Std.Array","source":{"first_line":28,"last_line":30}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U16","source":{"first_line":670,"last_line":670}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize.ofNat","source":{"first_line":703,"last_line":703}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table0._proof_1","source":null},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table1._proof_1","source":null},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Anchors","name":"crc_mono_anchors.crc.crc16.CrcU16Table1.table1","source":{"first_line":142,"last_line":151}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU16Table1.data","source":{"first_line":140,"last_line":140}}],"definitions_truncated":false,"first_line":26,"last_line":29,"module":"CrcProofs.Table","program":null,"program_head":null,"statement":"∀ (c : crc_mono_anchors.crc.CrcU16Table1),\n @Exists.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U16\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1))\n fun\n (out :\n Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U16\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1)) =>\n And\n (@Eq.{1}\n (Aeneas.Std.Result.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U16\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1)))\n (crc_mono_anchors.crc.crc16.CrcU16Table1.table1 c)\n (@Aeneas.Std.Result.ok.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U16\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1))\n out))\n (@Eq.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U16\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1))\n out (crc_mono_anchors.crc.CrcU16Table1.data c))","theorem":"CrcProofs.table_u16_l1_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"c","type":"crc_mono_anchors.crc.CrcU128Table0","type_segments":[{"ref":"crc_mono_anchors.crc.CrcU128Table0","text":"crc_mono_anchors.crc.CrcU128Table0"}]}],"conclusion":"∃ out, crc_mono_anchors.crc.crc128.CrcU128Table0.table0 c = Aeneas.Std.Result.ok out ∧ out = c.data","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"crc_mono_anchors.crc.crc128.CrcU128Table0.table0","text":"crc_mono_anchors.crc.crc128.CrcU128Table0.table0"},{"text":" "},{"text":"c"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"c"},{"text":"."},{"ref":"crc_mono_anchors.crc.CrcU128Table0.data","text":"data"}],"definitions":[{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table0","source":{"first_line":38,"last_line":45}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Aeneas.Std.Array.Array","name":"Aeneas.Std.Array","source":{"first_line":28,"last_line":30}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U128","source":{"first_line":673,"last_line":673}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize.ofNat","source":{"first_line":703,"last_line":703}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table0._proof_1","source":null},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table0._proof_2","source":null},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Anchors","name":"crc_mono_anchors.crc.crc128.CrcU128Table0.table0","source":{"first_line":47,"last_line":56}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table0.data","source":{"first_line":45,"last_line":45}}],"definitions_truncated":false,"first_line":66,"last_line":69,"module":"CrcProofs.Table","program":null,"program_head":null,"statement":"∀ (c : crc_mono_anchors.crc.CrcU128Table0),\n @Exists.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U128\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2))\n fun\n (out :\n Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U128\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2)) =>\n And\n (@Eq.{1}\n (Aeneas.Std.Result.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U128\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2)))\n (crc_mono_anchors.crc.crc128.CrcU128Table0.table0 c)\n (@Aeneas.Std.Result.ok.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U128\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2))\n out))\n (@Eq.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U128\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2))\n out (crc_mono_anchors.crc.CrcU128Table0.data c))","theorem":"CrcProofs.table_u128_l0_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"c","type":"crc_mono_anchors.crc.CrcU32Table1","type_segments":[{"ref":"crc_mono_anchors.crc.CrcU32Table1","text":"crc_mono_anchors.crc.CrcU32Table1"}]}],"conclusion":"∃ out, crc_mono_anchors.crc.crc32.CrcU32Table1.table1 c = Aeneas.Std.Result.ok out ∧ out = c.data","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"crc_mono_anchors.crc.crc32.CrcU32Table1.table1","text":"crc_mono_anchors.crc.crc32.CrcU32Table1.table1"},{"text":" "},{"text":"c"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"c"},{"text":"."},{"ref":"crc_mono_anchors.crc.CrcU32Table1.data","text":"data"}],"definitions":[{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU32Table1","source":{"first_line":208,"last_line":215}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Aeneas.Std.Array.Array","name":"Aeneas.Std.Array","source":{"first_line":28,"last_line":30}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U32","source":{"first_line":671,"last_line":671}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize.ofNat","source":{"first_line":703,"last_line":703}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table0._proof_1","source":null},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table1._proof_1","source":null},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Anchors","name":"crc_mono_anchors.crc.crc32.CrcU32Table1.table1","source":{"first_line":217,"last_line":226}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU32Table1.data","source":{"first_line":215,"last_line":215}}],"definitions_truncated":false,"first_line":41,"last_line":44,"module":"CrcProofs.Table","program":null,"program_head":null,"statement":"∀ (c : crc_mono_anchors.crc.CrcU32Table1),\n @Exists.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U32\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1))\n fun\n (out :\n Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U32\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1)) =>\n And\n (@Eq.{1}\n (Aeneas.Std.Result.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U32\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1)))\n (crc_mono_anchors.crc.crc32.CrcU32Table1.table1 c)\n (@Aeneas.Std.Result.ok.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U32\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1))\n out))\n (@Eq.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U32\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1))\n out (crc_mono_anchors.crc.CrcU32Table1.data c))","theorem":"CrcProofs.table_u32_l1_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"c","type":"crc_mono_anchors.crc.CrcU32Table0","type_segments":[{"ref":"crc_mono_anchors.crc.CrcU32Table0","text":"crc_mono_anchors.crc.CrcU32Table0"}]}],"conclusion":"∃ out, crc_mono_anchors.crc.crc32.CrcU32Table0.table0 c = Aeneas.Std.Result.ok out ∧ out = c.data","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"crc_mono_anchors.crc.crc32.CrcU32Table0.table0","text":"crc_mono_anchors.crc.crc32.CrcU32Table0.table0"},{"text":" "},{"text":"c"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"c"},{"text":"."},{"ref":"crc_mono_anchors.crc.CrcU32Table0.data","text":"data"}],"definitions":[{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU32Table0","source":{"first_line":188,"last_line":195}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Aeneas.Std.Array.Array","name":"Aeneas.Std.Array","source":{"first_line":28,"last_line":30}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U32","source":{"first_line":671,"last_line":671}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize.ofNat","source":{"first_line":703,"last_line":703}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table0._proof_1","source":null},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table0._proof_2","source":null},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Anchors","name":"crc_mono_anchors.crc.crc32.CrcU32Table0.table0","source":{"first_line":197,"last_line":206}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU32Table0.data","source":{"first_line":195,"last_line":195}}],"definitions_truncated":false,"first_line":36,"last_line":39,"module":"CrcProofs.Table","program":null,"program_head":null,"statement":"∀ (c : crc_mono_anchors.crc.CrcU32Table0),\n @Exists.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U32\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2))\n fun\n (out :\n Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U32\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2)) =>\n And\n (@Eq.{1}\n (Aeneas.Std.Result.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U32\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2)))\n (crc_mono_anchors.crc.crc32.CrcU32Table0.table0 c)\n (@Aeneas.Std.Result.ok.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U32\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2))\n out))\n (@Eq.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U32\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))\n crc_mono_anchors.crc.CrcU128Table0._proof_2))\n out (crc_mono_anchors.crc.CrcU32Table0.data c))","theorem":"CrcProofs.table_u32_l0_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"t","type":"crc_mono_anchors.crc.Table16","type_segments":[{"ref":"crc_mono_anchors.crc.Table16","text":"crc_mono_anchors.crc.Table16"}]}],"conclusion":"∃ out, crc_mono_anchors.crc.Table16.Insts.CoreCloneClone.clone t = Aeneas.Std.Result.ok out ∧ out = t","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"crc_mono_anchors.crc.Table16.Insts.CoreCloneClone.clone","text":"crc_mono_anchors.crc.Table16.Insts.CoreCloneClone.clone"},{"text":" "},{"text":"t"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"t"}],"definitions":[{"module":"Anchors","name":"crc_mono_anchors.crc.Table16","source":{"first_line":430,"last_line":435}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Anchors","name":"crc_mono_anchors.crc.Table16.Insts.CoreCloneClone.clone","source":{"first_line":437,"last_line":444}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}}],"definitions_truncated":false,"first_line":90,"last_line":92,"module":"CrcProofs.Table","program":null,"program_head":null,"statement":"∀ (t : crc_mono_anchors.crc.Table16),\n @Exists.{1} crc_mono_anchors.crc.Table16 fun (out : crc_mono_anchors.crc.Table16) =>\n And\n (@Eq.{1} (Aeneas.Std.Result.{0} crc_mono_anchors.crc.Table16)\n (crc_mono_anchors.crc.Table16.Insts.CoreCloneClone.clone t)\n (@Aeneas.Std.Result.ok.{0} crc_mono_anchors.crc.Table16 out))\n (@Eq.{1} crc_mono_anchors.crc.Table16 out t)","theorem":"CrcProofs.table_clone_l16_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Classical.choice","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"c","type":"crc_mono_anchors.crc.CrcU64Table1","type_segments":[{"ref":"crc_mono_anchors.crc.CrcU64Table1","text":"crc_mono_anchors.crc.CrcU64Table1"}]}],"conclusion":"∃ out, crc_mono_anchors.crc.crc64.CrcU64Table1.table1 c = Aeneas.Std.Result.ok out ∧ out = c.data","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"crc_mono_anchors.crc.crc64.CrcU64Table1.table1","text":"crc_mono_anchors.crc.crc64.CrcU64Table1.table1"},{"text":" "},{"text":"c"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"c"},{"text":"."},{"ref":"crc_mono_anchors.crc.CrcU64Table1.data","text":"data"}],"definitions":[{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU64Table1","source":{"first_line":283,"last_line":290}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Aeneas.Std.Array.Array","name":"Aeneas.Std.Array","source":{"first_line":28,"last_line":30}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.U64","source":{"first_line":672,"last_line":672}},{"module":"Aeneas.Std.Scalar.Core","name":"Aeneas.Std.Usize.ofNat","source":{"first_line":703,"last_line":703}},{"module":"Init.Prelude","name":"OfNat.ofNat","source":{"first_line":1393,"last_line":1393}},{"module":"Init.Prelude","name":"Nat","source":{"first_line":1349,"last_line":1371}},{"module":"Init.Prelude","name":"instOfNatNat","source":{"first_line":1395,"last_line":1397}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table0._proof_1","source":null},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU128Table1._proof_1","source":null},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Anchors","name":"crc_mono_anchors.crc.crc64.CrcU64Table1.table1","source":{"first_line":292,"last_line":301}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Anchors","name":"crc_mono_anchors.crc.CrcU64Table1.data","source":{"first_line":290,"last_line":290}}],"definitions_truncated":false,"first_line":56,"last_line":59,"module":"CrcProofs.Table","program":null,"program_head":null,"statement":"∀ (c : crc_mono_anchors.crc.CrcU64Table1),\n @Exists.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U64\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1))\n fun\n (out :\n Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U64\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1)) =>\n And\n (@Eq.{1}\n (Aeneas.Std.Result.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U64\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1)))\n (crc_mono_anchors.crc.crc64.CrcU64Table1.table1 c)\n (@Aeneas.Std.Result.ok.{0}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U64\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1))\n out))\n (@Eq.{1}\n (Aeneas.Std.Array.{0}\n (Aeneas.Std.Array.{0} Aeneas.Std.U64\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 256) (instOfNatNat (nat_lit 256)))\n crc_mono_anchors.crc.CrcU128Table0._proof_1))\n (Aeneas.Std.Usize.ofNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))\n crc_mono_anchors.crc.CrcU128Table1._proof_1))\n out (crc_mono_anchors.crc.CrcU64Table1.data c))","theorem":"CrcProofs.table_u64_l1_spec","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Quot.sound"],"binders":[{"binder":"explicit","kind":"variable","name":"self","type":"TableCloneFrom16.crc.Table16","type_segments":[{"ref":"TableCloneFrom16.crc.Table16","text":"TableCloneFrom16.crc.Table16"}]},{"binder":"explicit","kind":"variable","name":"source","type":"TableCloneFrom16.crc.Table16","type_segments":[{"ref":"TableCloneFrom16.crc.Table16","text":"TableCloneFrom16.crc.Table16"}]}],"conclusion":"∃ out, TableCloneFrom16.core.clone.Clone.clone_from.default self source = Aeneas.Std.Result.ok out ∧ out = source","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":", "},{"ref":"TableCloneFrom16.core.clone.Clone.clone_from.default","text":"TableCloneFrom16.core.clone.Clone.clone_from.default"},{"text":" "},{"text":"self"},{"text":" "},{"text":"source"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧ "},{"text":"out"},{"ref":"Eq","text":" = "},{"text":"source"}],"definitions":[{"module":"CloneFrom16.Anchors","name":"TableCloneFrom16.crc.Table16","source":{"first_line":23,"last_line":28}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"CloneFrom16.Anchors","name":"TableCloneFrom16.core.clone.Clone.clone_from.default","source":{"first_line":39,"last_line":46}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}}],"definitions_truncated":false,"first_line":17,"last_line":20,"module":"CrcProofs.TableCloneFrom","program":null,"program_head":null,"statement":"∀ (self source : TableCloneFrom16.crc.Table16),\n @Exists.{1} TableCloneFrom16.crc.Table16 fun (out : TableCloneFrom16.crc.Table16) =>\n And\n (@Eq.{1} (Aeneas.Std.Result.{0} TableCloneFrom16.crc.Table16)\n (TableCloneFrom16.core.clone.Clone.clone_from.default self source)\n (@Aeneas.Std.Result.ok.{0} TableCloneFrom16.crc.Table16 out))\n (@Eq.{1} TableCloneFrom16.crc.Table16 out source)","theorem":"CrcProofs.table_clone_from_l16_spec","translation_rerun":false,"version":1}
=== stderr ===
info: aeneas: materializing new dependency
info: aeneas: fetching revision 'be86ab0f1989d04944292b345b24c435be3ad10a' from https://github.com/AeneasVerif/aeneas.git
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'