How to use absurd/void in idris elaboration

Question

I am writing a trivial function in idris :

f : (a:Nat) -> (b:Nat) -> (k:(Z=(S Z))) -> (a=b)
f a b k = absurd k   --- this works

Now I want to write it using elaboration :

f : (a:Nat) -> (b:Nat) -> (k:(Z=(S Z))) -> (a=b)
f = %runElab (do
  intro' -- a
  intro' -- b
  intro' -- k
  -- now what ??
  )

I cant seem to find any way to use absurd/void and cant seem to find any documentation or example of this. Trying to use apply/fill keeps throwing errors regarding variables qquoteTy and unqTy, which are used in source code of elab (written in haskell) and i am unable to figure out anything from there.