commit: 415f8281e04c08e5ad069de8405b54df65aed35d

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

Wed Dec 25 13:05:56 2024 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Wed Dec 25 14:39:19 2024 -0800
tree: cb7d586b1ddb4963fc0654f1327f4763cf1fc059
parent: 977b8e001f8f14dc15bae22d2533fef0ea745486 [diff]

feat: support for builtin `grind` propagators

This PR declares the command `builtin_grind_propagator` for
registering equation propagator for `grind`. It also declares the
auxiliary the attribute.

5 files changed

tree: cb7d586b1ddb4963fc0654f1327f4763cf1fc059

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