commit: 1338a86f8074cdf2008fec4430295a2172a74b7b

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

Sun Dec 29 19:20:37 2024 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Sun Dec 29 19:20:37 2024 -0800
tree: 58de6fa85b5c1d8caae90dcdfa83e86c1abc1fb7
parent: 4e2b0f52729ae458a19bc81fdbb8a7c256d1c76e [diff]

feat: check pattern coverage in `grind_pattern`

This PR adds pattern validation to the `grind_pattern` command.
The new `checkCoverage` function will also be used to implement the attributes
`@[grind_eq]`, `@[grind_fwd]`, and `@[grind_bwd]`.

2 files changed

tree: 58de6fa85b5c1d8caae90dcdfa83e86c1abc1fb7

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