New syntax for Array access -- display syntax

Stream: lean4

[Clément Blaudeau]

Hi! As part of the Hax backend for Lean I'm trying to create a new syntax a[i]_? for array accesses that returns a custom Option type (that's why I'm not using a[i]? directly -- overriding GetElem? is not an option in my case).

I've copied the Lean definition of GetElem, and modified it to return an Result (a custom Option type with error cases)

class GetElemResult (coll : Type u) (idx : Type v) (elem : outParam (Type w)) where
  getElemResult (xs : coll) (i : idx) : Result elem

export GetElemResult (getElemResult)

@[inherit_doc getElemResult]
syntax:max term noWs "[" withoutPosition(term) "]" noWs "_?": term
macro_rules | `($x[$i]_?) => `(getElemResult $x $i)

instance Nat.instGetElemResultArray {α} : GetElemResult (Array α) Nat α where
  getElemResult xs i :=
    if h: i < xs.size then pure (xs[i])
    else .fail arrayOutOfBounds

It works, but internally, Lean does not keep the a[i]_?, but inlines them as calls to getElemResult, as can be seen by doing :

#check #[0,1,2,3][1]_? -- getElemResult #[0,1,2,3] 1 : Result Nat
#check #[0,1,2,3][1]? -- #[0,1,2,3][1]? : Option Nat

Am I missing a notation definition in addition to the macro ? I can't find any in the GetElem.lean file, unless perhaps this instance on Syntax ?
Thank you !

[Aaron Liu]

You need an unexpander or a delaborator

[Aaron Liu]

they're docs#unexpandGetElem and friends

[Clément Blaudeau]

Nice! Thank you! This works perfectly

@[app_unexpander getElemResult] meta def unexpandGetElemResult : Lean.PrettyPrinter.Unexpander
  | `($_ $array $index) => `($array[$index]_?)
  | _ => throw ()