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

fix(library/init): missing @[inline]

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-18 21:42:22 -07:00
parent 17a779c36f
commit d3e225ec65
2 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
library/init/coe.lean
View file

@ -47,30 +47,30 @@ class has_coe_to_fun (a : Sort u) : Sort (max u (v+1)) :=
class has_coe_to_sort (a : Sort u) : Type (max u (v+1)) :=
(S : Sort v) (coe : a → S)
def lift {a : Sort u} {b : Sort v} [has_lift a b] : a → b :=
@[inline] def lift {a : Sort u} {b : Sort v} [has_lift a b] : a → b :=
@has_lift.lift a b _
def lift_t {a : Sort u} {b : Sort v} [has_lift_t a b] : a → b :=
@[inline] def lift_t {a : Sort u} {b : Sort v} [has_lift_t a b] : a → b :=
@has_lift_t.lift a b _
def coe_b {a : Sort u} {b : Sort v} [has_coe a b] : a → b :=
@[inline] def coe_b {a : Sort u} {b : Sort v} [has_coe a b] : a → b :=
@has_coe.coe a b _
def coe_t {a : Sort u} {b : Sort v} [has_coe_t a b] : a → b :=
@[inline] def coe_t {a : Sort u} {b : Sort v} [has_coe_t a b] : a → b :=
@has_coe_t.coe a b _
def coe_fn_b {a : Sort u} [has_coe_to_fun.{u v} a] : Π x : a, has_coe_to_fun.F.{u v} x :=
@[inline] def coe_fn_b {a : Sort u} [has_coe_to_fun.{u v} a] : Π x : a, has_coe_to_fun.F.{u v} x :=
has_coe_to_fun.coe
/- User level coercion operators -/
@[reducible] def coe {a : Sort u} {b : Sort v} [has_lift_t a b] : a → b :=
@[reducible, inline] def coe {a : Sort u} {b : Sort v} [has_lift_t a b] : a → b :=
lift_t
@[reducible] def coe_fn {a : Sort u} [has_coe_to_fun.{u v} a] : Π x : a, has_coe_to_fun.F.{u v} x :=
@[reducible, inline] def coe_fn {a : Sort u} [has_coe_to_fun.{u v} a] : Π x : a, has_coe_to_fun.F.{u v} x :=
has_coe_to_fun.coe
@[reducible] def coe_sort {a : Sort u} [has_coe_to_sort.{u v} a] : a → has_coe_to_sort.S.{u v} a :=
@[reducible, inline] def coe_sort {a : Sort u} [has_coe_to_sort.{u v} a] : a → has_coe_to_sort.S.{u v} a :=
has_coe_to_sort.coe
/- Notation -/

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

@ -34,10 +34,10 @@ section
instance : monad (state_t σ m) :=
{ pure := @state_t.pure _ _ _, bind := @state_t.bind _ _ _ }
protected def orelse [alternative m] {α : Type u} (x₁ x₂ : state_t σ m α) : state_t σ m α :=
@[inline] protected def orelse [alternative m] {α : Type u} (x₁ x₂ : state_t σ m α) : state_t σ m α :=
⟨λ s, x₁.run s <|> x₂.run s⟩
protected def failure [alternative m] {α : Type u} : state_t σ m α :=
@[inline] protected def failure [alternative m] {α : Type u} : state_t σ m α :=
⟨λ s, failure⟩
instance [alternative m] : alternative (state_t σ m) :=