在 Agda 中，有时会出现过度展开函数定义的情况，导致编译时间变得异常缓慢或无法完成编译。这种情况通常发生在函数中使用了复杂的模式匹配或递归定义。为了解决这个问题，可以使用 pragma NO_TERMINATION_CHECK 或 NO_POSITIVITY_CHECK。

例如，考虑以下示例：

module Test where

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

plus : Nat → Nat → Nat
plus zero     m = m
plus (suc n) m = suc (plus n m)

f : Nat → Nat
f n = plus n n

在这个示例中，函数 f 中的 plus 函数被展开了两次，这是不必要的。为了解决这个问题，可以在 plus 函数上添加 NO_TERMINATION_CHECK 或 NO_POSITIVITY_CHECK，如下所示：

plus : Nat → Nat → Nat
{-# NO_TERMINATION_CHECK #-}
plus zero     m = m
plus (suc n) m = suc (plus n m)

这将停止 Agda 检查 plus 函数的终止性或正性，使 Agda 不再尝试展开 plus 函数。

需要注意的是，NO_TERMINATION_CHECK 或 NO_POSITIVITY_CHECK 实际上增加了程序的危险性，因为这使得 Agda 无法检查这些属性，可能导致编译错误或运行时错误。因此，应该尽可能避免使用这些 pragma，只在无法避免函数过度展开的情况下使用它们。