idris - 如何在 idris 阐述中使用荒谬/无效

Question

我正在 idris 中编写一个简单的函数：

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

现在我想用 elaboration 来写它：

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

我似乎找不到任何使用荒谬/无效的方法，并且似乎找不到任何文档或示例。尝试使用 apply/fill 会不断抛出有关变量qquoteTy和unqTy的错误，这些变量用于 elab 的源代码（用 haskell 编写），我无法从那里找出任何东西。