From 5eed3b73bfb641932f481c786924beb6d3cf034f Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Tue, 14 Sep 2021 15:00:09 -0700 Subject: [PATCH] chore: adjust pp.analyze funext test --- tests/lean/run/PPTopDownAnalyze.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean index 36fc709eeb..4b1358654e 100644 --- a/tests/lean/run/PPTopDownAnalyze.lean +++ b/tests/lean/run/PPTopDownAnalyze.lean @@ -320,9 +320,9 @@ def stackMkInjEqSnippet := def typeAs (α : Type u) (a : α) := () -theorem myFunext : ∀ {α : Sort u} {β : α → Sort v} {f₁ f₂ : (x : α) → β x}, (∀ (x : α), f₁ x = f₂ _) → f₁ = f₂ := funext - -#testDelabN myFunext +set_option pp.analyze.explicitHoles false in +#testDelab ∀ {α : Sort u} {β : α → Sort v} {f₁ f₂ : (x : α) → β x}, (∀ (x : α), f₁ x = f₂ _) → f₁ = f₂ + expecting ∀ {α : Sort u} {β : α → Sort v} {f₁ f₂ : (x : α) → β x}, (∀ (x : α), f₁ x = f₂ x) → f₁ = f₂ set_option pp.analyze.trustSubtypeMk true in #testDelab fun (n : Nat) (val : List Nat) (property : List.length val = n) => List.length { val := val, property := property : { x : List Nat // List.length x = n } }.val = n