commit: dc5c8097b5ca053dd49b5de246add54c3e999734

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

Sun Jan 05 03:20:17 2025 +0100
committer: GitHub <noreply@github.com>

Sun Jan 05 02:20:17 2025 +0000
tree: 4f7a8af4d3b6339c74e6d3747e59304d8f8b1467
parent: 9dcbc330fd08a5ae455a6e5a5c6b30b877bb2917 [diff]

feat: add term offset support to the `grind` E-matching modulo (#6533)

This PR adds support to E-matching offset patterns. For example, we want
to be able to E-match the pattern `f (#0 + 1)` with term `f (a + 2)`.

7 files changed

tree: 4f7a8af4d3b6339c74e6d3747e59304d8f8b1467

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