Hi
Yong Luo wrote:
I think the problem is still about pattern coverage. It becomes clearer that
pattern matching is different from case-spliting, and that is why the
majority function comes into our discussion.
As I have explained, functions such as the majority function present no
more
f :: m:Nat - n:Nat - T m n - T m n
f 2 n t = t
f 7 9 c4 = c5
f 7 9 c5 = c4
Because, as a decision procedure for covering will tell you, that is not
a function.
Do you mean this is not a total function? I think it is.
Maybe it is, in which case I'm sorry I'm too
