diff --git a/library/init/core.lean b/library/init/core.lean index 0cc29d6b89..f6e979e3b6 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -601,6 +601,9 @@ prefix ! := not infix || := or infix && := and +@[inlineIfReduce] def strictOr (b₁ b₂ : Bool) := b₁ || b₂ +@[inlineIfReduce] def strictAnd (b₁ b₂ : Bool) := b₁ && b₂ + @[inline] def bne {α : Type u} [HasBeq α] (a b : α) : Bool := !(a == b) diff --git a/tests/playground/parser.lean b/tests/playground/parser.lean index c99e268e9b..267fe2ded4 100644 --- a/tests/playground/parser.lean +++ b/tests/playground/parser.lean @@ -42,9 +42,6 @@ p s (mkInput 0 st bst) | ⟨Result.ok _ it st bst _, h⟩ := Result.ok a it st bst true | ⟨Result.error _ _ _ _ _, h⟩ := unreachableError h -@[inlineIfReduce] def strictOr (b₁ b₂ : Bool) := b₁ || b₂ -@[inlineIfReduce] def strictAnd (b₁ b₂ : Bool) := b₁ && b₂ - @[inline] def parserM.bind (x : parserM σ δ μ α) (f : α → parserM σ δ μ β) : parserM σ δ μ β := λ str inp, match x str inp with