commit: e968dfb68c5a99cd320f1ac8d9d0be1228308abd

[log]
author: Leonardo de Moura <leonardo@microsoft.com>

Wed Jun 29 13:29:50 2022 -0700
committer: Leonardo de Moura <leonardo@microsoft.com>

Wed Jun 29 13:30:06 2022 -0700
tree: 27b36f7b2e2590bfb14289dcfe342178bcb3d65c
parent: 598898a087d00be52658485d139b307be6d97cc1 [diff]

feat: elaborate `do` notation even when expected type is not available

see issue #1256

RELEASES.md[diff]
src/Lean/Elab/Do.lean[diff]
tests/lean/474.lean[diff]
tests/lean/625.lean[diff]
tests/lean/doIfLet.lean[diff]
tests/lean/forallMetaBounded.lean[diff]
tests/lean/run/evalDo.lean[Added - diff]
tests/lean/sepByIndentQuot.lean[diff]

8 files changed

tree: 27b36f7b2e2590bfb14289dcfe342178bcb3d65c

README.md

This is the repository for Lean 4, which is currently being released as milestone releases towards a first stable release. Lean 3 is still the latest stable release.

About

Quickstart
Homepage
Theorem Proving Tutorial
Functional Programming in Lean first chapter is available!
Manual
Release notes starting at v4.0.0-m3
Examples
FAQ

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.