commit: 02c45a757768064a64a670756cdba69d8c08931a

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

Tue Feb 27 20:18:51 2024 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Tue Feb 27 21:37:22 2024 -0800
tree: 67417d5032257ba90d74b4ecc2f2b056e5520df0
parent: 86ca8e32c691c7589f36c77c34f30f786814f3d1 [diff]

feat: add option `tactic.skipAssignedInstances := true` for backward compatibility

When using `set_option tactic.skipAssignedInstances false`, `simp` and
`rw` will synthesize instance implicit arguments even if they have
assigned by unification. If the synthesized argument does not match
the assigned one the rewrite is not performed. This option has been
added for backward compatibility.

6 files changed

tree: 67417d5032257ba90d74b4ecc2f2b056e5520df0

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.