Postpone elaboration until type of sub-syntax is known

Stream: lean4

[Tomas Skrivan]

I would like to write a custom elaboration of element access and I seem to need to postpone it until I know the type of the container.

So if I have elaborator like

open Lean Elab Term in
elab (priority:=high) x:term noWs "[" i:term "]" : term => do
  -- the plan is to do something more complicated here
  elabTerm (← `(GetElem.getElem $x $i True.intro)) none

can I postpone it until I know what is the expected type of x?

Based on this question I know how to get expected type of the whole expression bu

[Tomas Skrivan]

I have tried this

  let x ← elabTerm x none
  let X ← inferType x
  if X.isMVar then
    throwPostpone

but it does not work as expected.