[Agda] acyclicity of constructors

[Nils Anders Danielsson]

On Sun, Jun 29, 2008 at 5:15 AM, Dan Licata <drl at cs.cmu.edu> wrote:
>
> [What exactly does != mean here?  I'm assuming it's (the failure of)
>  unification-modulo-definitional-equality.]

Yes.

> Actually, the corresponding situation for CoNat is puzzling to me.  As
> far as I can tell, in Agda right now, you can neither prove nor refute
> (Id n (S n)) for CoNat.

You can prove it for n = omega:

  force : CoNat -> CoNat
  force Z     = Z
  force (S n) = S n

  force-eq : (n : CoNat) -> Id n (force n)
  force-eq Z     = Refl
  force-eq (S n) = Refl

  eq : Id omega (S omega)
  eq = force-eq omega

And for finite n, with

  data Finite : CoNat -> Set where
    Z : Finite Z
    S : forall {i} (n : Finite i) -> Finite (S i)

you can prove the negation.

-- 
/NAD