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

fix: typo in theorem

Browse source 
`()` is `Unit`
This commit is contained in:
Leonardo de Moura 2021-03-03 19:50:11 -08:00
parent 3107473c9f
commit e841f16738
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Core.lean
View file

@ -606,8 +606,8 @@ protected theorem PSigma.eta {α : Sort u} {β : α → Sort v} {a₁ a₂ : α}
theorem PUnit.subsingleton (a b : PUnit) : a = b := by
cases a; cases b; exact rfl
@[simp] theorem PUnit.eq_punit (a : PUnit) : a = () :=
PUnit.subsingleton a ()
@[simp] theorem PUnit.eq_punit (a : PUnit) : a = ⟨⟩ :=
PUnit.subsingleton a ⟨⟩
instance : Subsingleton PUnit :=
Subsingleton.intro PUnit.subsingleton