Expand description
Generated by js/scripts/build-lean-root-names.mjs from Lean 4.34.1; do not edit.
Root-level constants of Lean’s prelude, which a root declaration may not redeclare.
Generated by js/scripts/build-lean-root-names.mjs from Lean 4.34.1; do not edit.
Root-level constants of Lean’s prelude, which a root declaration may not redeclare.