max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: adjust pp.analyze funext test

Browse source
This commit is contained in:
Daniel Selsam 2021-09-14 15:00:09 -07:00 • committed by Sebastian Ullrich
parent 664737def8
commit 5eed3b73bf
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/lean/run/PPTopDownAnalyze.lean
View file

@ -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