From af632643de8daa89b5784431a27a8517255a2858 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Wed, 24 Jul 2024 09:57:45 -0700 Subject: [PATCH] additional test --- src/Lean/Elab/App.lean | 2 +- tests/lean/run/4761.lean | 9 +++++++++ 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index cbbee7da1212..dfd836c73c7a 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -1357,7 +1357,7 @@ private partial def resolveDotName (id : Syntax) (expectedType? : Option Expr) : withForallBody expectedType fun resultType => do go resultType expectedType #[] where - /-- A weak version of forallTelescopeReducing that only uses whnfCore. -/ + /-- A weak version of forallTelescopeReducing that only uses whnfCore, to avoid unfolding definitions except by `unfoldDefinition?` below. -/ withForallBody {α} (type : Expr) (k : Expr → TermElabM α) : TermElabM α := forallTelescope type fun _ body => do let body ← whnfCore body diff --git a/tests/lean/run/4761.lean b/tests/lean/run/4761.lean index 56feeba7b039..2bc1f72f17d2 100644 --- a/tests/lean/run/4761.lean +++ b/tests/lean/run/4761.lean @@ -6,3 +6,12 @@ def Foo : Prop := ∀ a : Nat, a = a protected theorem Foo.intro : Foo := sorry example : Foo := .intro + +/-! +Making sure that the type synonym `Foo'` still works. +This used to be unfolded during `forallTelescopeReducing`, +and now it is "manually" unfolded in the elaboration algorithm. +-/ +example : Nat → Option Nat := .some +def Foo' := Nat → Option Nat +example : Foo' := .some