idris - idris の説明で不条理/無効を使用する方法

Question

私は idris で簡単な関数を書いています:

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

今、私は精緻化を使用してそれを書きたい:

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

不条理/無効を使用する方法を見つけることができないようであり、これに関するドキュメントや例を見つけることができないようです。apply/fill を使用しようとすると、(haskell で記述された) elab のソース コードで使用される変数qquoteTyおよびunqTyに関するエラーがスローされ続け、そこから何も把握できません。