mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
40e8f4c5fb
This PR turns on the new `do` elaborator in Init, Lean, Std, Lake and the testsuite. --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
13 lines
248 B
Lean4
13 lines
248 B
Lean4
import Lean
|
|
set_option backward.do.legacy false
|
|
|
|
namespace Lean.Meta
|
|
|
|
def f (e : Expr) : MetaM Bool := do
|
|
forallTelescope e fun xs b =>
|
|
match (← uinfoldDefinition? b) with
|
|
| none => pure true
|
|
| some _ => pure false
|
|
|
|
end Lean.Meta
|