[Agda] Problem with inductively defined type having (simulated) partial constructors

[Wouter Swierstra]

Hi Tristan,

> I've  got unexpected problems in the definition of _or_ that the
> compiler can't deduce that the conditions are true in any cases.
>
> Anybody got any hints?

First of all, you may want to include the following lines in your code:


{-#  BUILTIN NATURAL Nat   #-}
{-#  BUILTIN SUC     succ  #-}
{-#  BUILTIN ZERO    zero  #-}

You can then write "16" instead of "sixteen" etc.

There are actually two problems with your definition of or. First of,  
as you noted, there are unresolved constraints. Basically, the proofs  
that you left implicit in the data type definition are not  
automatically passed around. This is pretty easy to fix in some cases.  
Just write:

(_orone a {p}) or allzeros  = _orone a {p}

and pass around the proofs by hand. In other cases, such as:

(a orone) or (b orone) = (a or b) orone

you will need to prove that "even a" and "even b" implies "even (a or  
b)".  The proof shouldn't be too hard, but it is a little bit annoying.

The other problem with your code is that it isn't obviously  
structurally recursive, and therefore doesn't termination check. This  
surprised me a bit. It seems ok, but maybe I'm missing something here.

By the way, what are you trying to define. I couldn't quite figure out  
what the inhabitants of Octet should be just from your code. Perhaps  
there's an easier way to set things up...

Hope this helps,

  Wouter