commit: 29477b3b7c8f13f45a969baf2e3e2bec4e34f2f9

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

Wed May 08 13:36:22 2024 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Wed May 08 13:47:15 2024 -0700
tree: 9c7d5d300e30a9dd855f32ecc65180c1d20892d5
parent: b54be549baf8d696bd5c70f40c8f70642d565f1d [diff]

feat: add `withSynthesize (postpone := partial) k`

It forces pending elaboration problems and tactics to be executed, but
allows TC ones to be postponed.

12 files changed

tree: 9c7d5d300e30a9dd855f32ecc65180c1d20892d5

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