chore(library/init/core): remove another weirdness: the bs at bnot, band and bor

This commit is contained in:
Leonardo de Moura 2019-03-22 12:57:31 -07:00
parent e1ea2b3948
commit 3fe5cf1528
3 changed files with 11 additions and 11 deletions

View file

@ -581,26 +581,26 @@ theorem optParamEq (α : Sort u) (default : α) : optParam α default = α := rf
| true x y := x
| false x y := y
@[macroInline] def bor : Bool → Bool → Bool
@[macroInline] def or : Bool → Bool → Bool
| true _ := true
| false b := b
@[macroInline] def band : Bool → Bool → Bool
@[macroInline] def and : Bool → Bool → Bool
| false _ := false
| true b := b
@[macroInline] def bnot : Bool → Bool
@[macroInline] def not : Bool → Bool
| true := false
| false := true
@[macroInline] def bxor : Bool → Bool → Bool
@[macroInline] def xor : Bool → Bool → Bool
| true false := true
| false true := true
| _ _ := false
prefix ! := bnot
infix || := bor
infix && := band
prefix ! := not
infix || := or
infix && := and
/- Logical connectives an equality -/

View file

@ -246,9 +246,9 @@ foldr (λ a r, p a || r) false l
@[inline] def all (l : List α) (p : α → Bool) : Bool :=
foldr (λ a r, p a && r) true l
def bor (l : List Bool) : Bool := any l id
def or (bs : List Bool) : Bool := bs.any id
def band (l : List Bool) : Bool := all l id
def and (bs : List Bool) : Bool := bs.all id
def zipWith (f : α → β → γ) : List α → List β → List γ
| (x::xs) (y::ys) := f x y :: zipWith xs ys

View file

@ -18,7 +18,7 @@ else
let r := bitwise n' m' in
if f b₁ b₂ then bit1 r else bit0 r
def land : Nat → Nat → Nat := bitwise band
def lor : Nat → Nat → Nat := bitwise bor
def land : Nat → Nat → Nat := bitwise and
def lor : Nat → Nat → Nat := bitwise or
end Nat