I am currently creating a comparison of large libraries of ITPs. I am only
considering libraries with more than 1M (nonempty) LOC, of which I know (in
alphabetical order): ACL2, HOL4, Isabelle, Lean, Metamath, Mizar, PVS, Rocq.
To that end, I want to approximate the number of definitions (incl. a
h since the 1M cutoff was simply used
> to select the systems to consider, and the numbers which are reported are
> not about LOC but about number of theorems and definitions.
>
> On Thu, Jun 5, 2025 at 9:11 PM 'David A. Wheeler' via Metamath <
> meta...@googlegroups.
t;
> Besides, I don't think it matters much since the 1M cutoff was simply used
> to select the systems to consider, and the numbers which are reported are
> not about LOC but about number of theorems and definitions.
>
> On Thu, Jun 5, 2025 at 9:11 PM 'David A. Wheeler&
