How to use xor for boolean function?

Stream: new members

[Anthony Peterson]

I am trying to migrate from Coq to Lean 4 and I'm starting by translation an existing proof that I wrote in Coq into Lean. It's just a stupid simple lemma about the Xor function, and I'm stumbling trying gain access to the definition of xor in Bool

Probably just some simple thing I'm missing. I've tried to look at the file where boolean functions are defined, but my import statement doesn't work and xor doesn't seem to be in scope by default. I'm not even sure if Lean uses scopes the same way Coq does?

import init.data.bool

#eval  xor true false

[Bolton Bailey]

docs#Bool.xor

[Bolton Bailey]

Seems to be in Std.Data.Bool

[Bolton Bailey]

import Std.Data.Bool

#eval  xor true false

[Timo Carlin-Burns]

It's a bit concerning that you've pasted import init.data.bool. That lowercase naming convention for modules was only used in Lean 3.

[Anthony Peterson]

Bolton Bailey said:

import Std.Data.Bool

#eval  xor true false

Thanks that's what I needed. the Std.Data.Bool

[Eric Wieser]

Note there is also true ^^^ false notation

[Timo Carlin-Burns]

Eric Wieser said:

Note there is also true ^^^ false notation

I tested that and there doesn't seem to be an instance of Xor Bool.

[Eric Wieser]

Even with mathlib imported?

[Timo Carlin-Burns]

import Mathlib

#check true ^^^ false
-- failed to synthesize instance
--   HXor Bool Bool ?m.20