commit: 8ab0e313b8fad223be5c9c383b14339efff793ba

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

Sun Feb 09 08:46:23 2025 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Sun Feb 09 08:46:23 2025 -0800
tree: fed878db187c657b644ab4c3aaaef15269de0794
parent: cd3eb9125cabcc9cfb063ee0075ca07c9612f3de [diff]

feat: `bv_decide` hint

This PR ensures users get an error message saying which module to
import when they try to use `bv_decide`.

2 files changed

tree: fed878db187c657b644ab4c3aaaef15269de0794

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).