GetElem on PPoint example doesn't work

Stream: new members

[Lars Ericson]

The example code at the bottom of this chapter:

structure PPoint (α : Type) where
  x : α
  y : α
deriving Repr

instance : GetElem (PPoint α) Bool α (fun _ _ => True) where
  getElem (p : PPoint α) (i : Bool) _ :=
    if not i then p.x else p.y

def foo := ({x := 1, y := 2}: PPoint Nat)

#check foo[False]

Leads to this error:

hw_lists2.lean:12:7
failed to synthesize instance
  GetElem (PPoint Nat) Prop ?m.1822 ?m.1823
hw_lists2.lean:12:7
failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is perfomed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
⊢ ?m.1823 foo False

Is the example incorrect or am I missing something?

[Johan Commelin]

Try #check False and compare with #check false.