Zulip Chat Archive

Stream: new members

Topic: GetElem on PPoint example doesn't work

Lars Ericson (Jul 18 2023 at 12:17):

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:

failed to synthesize instance
  GetElem (PPoint Nat) Prop ?m.1822 ?m.1823
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 (Jul 18 2023 at 12:20):

Try #check False and compare with #check false.

Last updated: Dec 20 2023 at 11:08 UTC