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

perf(library/init): missing [inline] attributes

Browse source
This commit is contained in:
Sebastian Ullrich 2018-10-01 11:53:19 -07:00
parent 0279cb0766
commit e261d8f222
2 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/control/reader.lean
View file

@ -54,10 +54,10 @@ section
@[inline] protected def adapt {ρ' : Type u} [monad m] {α : Type u} (f : ρ' → ρ) : reader_t ρ m α → reader_t ρ' m α :=
λ x r, x (f r)
protected def orelse [alternative m] {α : Type u} (x₁ x₂ : reader_t ρ m α) : reader_t ρ m α :=
@[inline] protected def orelse [alternative m] {α : Type u} (x₁ x₂ : reader_t ρ m α) : reader_t ρ m α :=
λ s, x₁ s <|> x₂ s
protected def failure [alternative m] {α : Type u} : reader_t ρ m α :=
@[inline] protected def failure [alternative m] {α : Type u} : reader_t ρ m α :=
λ s, failure
instance [alternative m] : alternative (reader_t ρ m) :=

6
library/init/core.lean
View file

@ -1220,8 +1220,10 @@ if h : p then decidable_of_decidable_of_iff (DP h)
⟨λ h2 _, h2, λal, al h⟩ else is_true (λ h2, absurd h2 h)
end
instance {α : Sort u} [decidable_eq α] (a b : α) : decidable (a ≠ b) :=
implies.decidable
@[inline] instance {α : Sort u} [decidable_eq α] (a b : α) : decidable (a ≠ b) :=
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
.