Comment by hirple

I guess Coq/Lean standard libraries fit this definition.