michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/data/bool): Add bxor definition

Browse source
This commit is contained in:
Joe Hendrix 2015-11-29 23:06:06 -08:00 committed by Leonardo de Moura
parent 139536896c
commit 63a17a3f48
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/data/bool.lean
View file

@ -127,4 +127,6 @@ namespace bool
theorem eq_ff_of_bnot_eq_tt {a : bool} : bnot a = tt → a = ff := theorem eq_ff_of_bnot_eq_tt {a : bool} : bnot a = tt → a = ff :=
bool.cases_on a (λ h, rfl) (by contradiction) bool.cases_on a (λ h, rfl) (by contradiction)
definition bxor (x:bool) (y:bool) := cond x (bnot y) y
end bool end bool