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

chore(library/init/core): avoid . as end-of-command and empty equations

Browse source
This commit is contained in:
Leonardo de Moura 2018-10-05 17:10:55 -07:00
parent fc62e8f3a4
commit eb51b9ef26
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/core.lean
View file

@ -1207,8 +1207,8 @@ match dec_eq a b with
| is_true h := is_false $ λ h', absurd h h'
| is_false h := is_true h
theorem bool.ff_ne_tt : ff = tt → false
.
theorem bool.ff_ne_tt (h : ff = tt) : false :=
bool.no_confusion h
def is_dec_eq {α : Sort u} (p : α → α → bool) : Prop := ∀ ⦃x y : α⦄, p x y = tt → x = y
def is_dec_refl {α : Sort u} (p : α → α → bool) : Prop := ∀ x, p x x = tt