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

chore(library/init/core): add strictAnd and strictOr

Browse source
This commit is contained in:
Leonardo de Moura 2019-03-28 09:42:12 -07:00
parent 19f31d483a
commit 2943fce8c8
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/init/core.lean
View file

@ -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)

3
tests/playground/parser.lean
View file

@ -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