How to use absurdity / void when developing idris

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 development:

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

I cannot find a way to use absurdity / void and I cannot find any documentation or an example of this. Trying to use apply / fill continues to throw errors regarding the qquoteTy and unqTy variables that are used in the elab source code (written in haskell), and I cannot figure out anything from there.