Core C++

Blueprint Summary🔗

Overview
Total entries91completed: 86; deps incomplete: 0; sorries: 0; no proof: 5
Ready now5Entries with an actionable next formalization step.
Fully closed86Local code and prerequisite closure are both complete.
Actionable priorities0Entries ready now and already unlocking downstream work.
Entry index (91)
Definitions85completed: 85; deps incomplete: 0; sorries: 0; no proof: 0
Theorems6completed: 1; deps incomplete: 0; sorries: 0; no proof: 5
Informal-only entries5
Definition Index (85)
Theorem / Proposition / Lemma / Corollary Index (6)
By parent groups (4)
Functions, parameters and calls. (2)
Syntax, tokens and the parser. (2)
Overloading, polymorphism, subtyping and inference. (1)
Abstract data types, objects, classes and inheritance. (1)
Dependency insights
Statement-used entries60Entries reused in statement dependencies.
Tracked parent groups9Grouped health rollups for parents with more than one child entry.
Most used in statements (60)
Group health (9)
  • Functions, parameters and calls.ud4
    Grouped view over entries sharing the same parent.
    total: 10closed: 8local-only: 0ready: 2blocked: 0incomplete Lean: 0unlock score: 37
    Next: determinismo stage: proofdownstream unlocks: 0
  • Syntax, tokens and the parser.ud1
    Grouped view over entries sharing the same parent.
    total: 14closed: 13local-only: 0ready: 1blocked: 0incomplete Lean: 0unlock score: 106
    Next: pp_agree stage: proofdownstream unlocks: 0
  • Abstract data types, objects, classes and inheritance.ud5
    Grouped view over entries sharing the same parent.
    total: 12closed: 11local-only: 0ready: 1blocked: 0incomplete Lean: 0unlock score: 57
    Next: cls_dispatch_agree stage: proofdownstream unlocks: 0
  • Overloading, polymorphism, subtyping and inference.ud6
    Grouped view over entries sharing the same parent.
    total: 9closed: 8local-only: 0ready: 1blocked: 0incomplete Lean: 0unlock score: 11
    Next: subtyping stage: proofdownstream unlocks: 0
  • Semantic domains, in CoreCpp/Semantics.lean and CoreCpp/Typing.lean .dominios
    Grouped view over entries sharing the same parent.
    total: 11closed: 11local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 452
    Next: no ready child currently unlocks downstream work.
  • The judgments, one Lean function each, in CoreCpp/Typing.lean and CoreCpp/Eval.lean .juizos
    Grouped view over entries sharing the same parent.
    total: 7closed: 7local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 222
    Next: no ready child currently unlocks downstream work.
  • Variables, update and commands.ud3
    Grouped view over entries sharing the same parent.
    total: 10closed: 10local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 28
    Next: no ready child currently unlocks downstream work.
  • Values, types and expressions.ud2
    Grouped view over entries sharing the same parent.
    total: 13closed: 13local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 11
    Next: no ready child currently unlocks downstream work.
  • The library, its interface and its intrinsics.ud7
    Grouped view over entries sharing the same parent.
    total: 5closed: 5local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 9
    Next: no ready child currently unlocks downstream work.
Metadata
Metadata audit
Missing owner91
Missing effort91
Untagged91
Missing owner (91)
Missing effort (91)
Untagged (91)
Structure and coverage
Informal-only5Statements with no associated Lean code yet.
Ready to formalize5Entries with an actionable next formalization step.
Fully closed86Local code and ancestor closure are both complete.
Heaviest prerequisites (80)
No prerequisites (11)
No dependents (31)