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

test: issue #2835

Browse source 
closes #2835
This commit is contained in:
Leonardo de Moura 2024-03-06 13:19:53 -08:00 • committed by Leonardo de Moura
parent 4208c44939
commit ef33882e2f
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/lean/run/2835.lean Normal file
View file

@ -0,0 +1,6 @@
@[simp] theorem imp_self' {a : Prop} : (a → a) ↔ True := ⟨fun _ => trivial, fun _ => id⟩
example {P : Prop} : P → P := by simp only [imp_self']
example {α : Prop} {P : α → Prop} {f : ∀ {a}, P a → α} {a : α} : (h : P a) → P (f h) := by
simp only [imp_self']