diff --git a/library/init/core.lean b/library/init/core.lean index bf2bd24c24..cf3c585805 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -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 -/ diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean index 45a3b8f23b..e8f10f1311 100644 --- a/library/init/data/list/basic.lean +++ b/library/init/data/list/basic.lean @@ -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 diff --git a/library/init/data/nat/bitwise.lean b/library/init/data/nat/bitwise.lean index 1572786efa..7c5f1dd78b 100644 --- a/library/init/data/nat/bitwise.lean +++ b/library/init/data/nat/bitwise.lean @@ -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