bool vs prop

Stream: new members

[Bernardo Anibal Subercaseaux Roa]

Hi! I'm trying to understand why the following happens, which seems to be about the differences between type Bool and type Prop:

def is_odd (x : ℕ) : Bool := x % 2 = 1
def odds_until_n (n : ℕ) : List ℕ := filter (fun x => is_odd x) (range n)
#eval odds_until_n 10 -- [1, 3, 5, 7, ,9]

This works, but trying with Prop as

def is_odd (x : ℕ) : Prop := x % 2 = 1
def odds_until_n (n : ℕ) : List ℕ := filter (fun x => is_odd x = true) (range n)

I get failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Prop.linearOrder', and it does not have executable code. Why is that?

[Eric Wieser]

That's a fun corner case

[Eric Wieser]

But what you should probably be writing is

def odds_until_n (n : ℕ) : List ℕ := filter (fun x => decide (is_odd x)) (range n)

since in the second example, is_odd x = true is being interpreted asdecide (is_odd x = (true = true)) which is just nonsense!

[Bernardo Anibal Subercaseaux Roa]

with your definition I get failed to synthesize Decidable (is_odd x)... also, is there a way in VSCode of seeing "how it is being interpreted"? I feel like that would be helpful at my stage :)

[Eric Wieser]

Yes, to see how it was being parsed I:

• Added the noncomputable to silence the error
• Ran #print odds_until_n to see what it defined

[Eric Wieser]

Bernardo Anibal Subercaseaux Roa said:

with your definition I get failed to synthesize Decidable (is_odd x)

Replacing def is_odd with abbrev is_odd will fix this; as will manually implementing instance : Decidable (is_odd x).