问题

我有一个简单的归纳记录，其中有一个求和类型的单个字段。Unit给我们提供了一个简单的类型。

open import Data.Maybe
open import Data.Sum

data Unit : Set where
  unit : Unit

record Stream : Set where
  coinductive
  field
    step : Unit ? Stream

open Stream

作品

valid 通过终止检查器：

valid : Maybe Unit ? Stream
step (valid x) = inj? (valid x)

休息时间

但是说我想消除Maybe Unit成员，只有在有资格时递归just。

invalid? : Maybe Unit ? Stream
step (invalid? x) = maybe (? _ ? inj? (invalid? x)) (inj? unit) x

现在终止检查器不满意！

Termination checking failed for …