小编Dav*_*ave的帖子

我正在尝试CoNat从Jesper Cockx 和 Andreas Abel 的这篇论文中得到的定义：

open import Data.Bool
open import Relation.Binary.PropositionalEquality

record CoNat : Set where
  coinductive
  field iszero : Bool
        pred : .(iszero ? false) -> CoNat

open CoNat public

我定义zero和plus：

zero : CoNat
iszero zero = true
pred zero ()

plus : CoNat -> CoNat -> CoNat
iszero (plus m n)                                  = iszero m ? iszero n
pred (plus m n) _ with iszero m | inspect iszero m …