<br>Dan wrote:<br style="font-family: courier new,monospace;"><blockquote style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;" class="gmail_quote"><span style="font-family: courier new,monospace;">
height : Indexed Z -> Nat</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">height B = Z</span><br></blockquote><br>The error message (which shouldn't involve panicking) tells you that you can't pattern match on the argument, because the type checker can't figure out if I is a valid constructor. In order to do this it would have to solve the unification problem
<span style="font-family: courier new,monospace;">Z = plus n m,<span style="font-family: arial,sans-serif;"> which it can't.<br><br>The problem is that the index isn't a variable, which makes the unification problem too hard. The standard trick is to make the index a variable:
<br><br><span style="font-family: courier new,monospace;">data _==_ {A : Set}(x : A) : A -> Set where</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;"> refl : x == x
</span><br style="font-family: courier new,monospace;"><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">height' : {n : Nat} -> Indexed n -> n == Z -> Nat</span>
<br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">height' B refl = Z</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">
height' (I {Z} l r) refl = ? -- you forgot about this case</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">height' (I {S n} l r) () -- impossible case
</span><br style="font-family: courier new,monospace;"><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">height : Indexed Z -> Nat</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">height i = height' i refl</span><br style="font-family: courier new,monospace;"><br>In the I case (which you left out) we need to match on the size of the left sub-tree in order to be able to inspect the proof object. The reason your version of this approach didn't go through is that you need to
<i>first</i> match on the tree and <i>then</i> on the proof object (otherwise we're back in the same situation as we started in). Pattern matching happens from left to right, so you need the proof argument to appear after the tree argument.
<br><br>/ Ulf<br></span></span>