commit: b0ce3c4a684c5f0c8b5ae33fa5ab26b43f88c5f1

[log]
author: Leonardo de Moura <leomoura@amazon.com>

Mon Sep 02 14:03:57 2024 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Mon Sep 02 14:03:57 2024 -0700
tree: 54e6ad89d6a29418b9264a342f6fb50c1013069a
parent: df9cdcd1b7cf7863680672d147ab09394104f827 [diff]

chore: use `Expr.numObjs` instead of `lean_expr_size_shared`

Remark: declarations like `sizeWithSharing` must be in `IO` since they
are not functions.

The commit also uses the more efficient `ShareCommon.shareCommon'`.

3 files changed

tree: 54e6ad89d6a29418b9264a342f6fb50c1013069a

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean (documentation source: doc/make/index.md).