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 difficulty (ie still none) for coverage checking in the language with refutations and equations. The only issues with such functions are pragmatic: firstly whether it's worth putting effort into supporting their recognition (eg by expansion to case-splits, as I'm given to believe is to happen in Agda 2) and secondly whether it's worth going further and adding them directly to the core theory in order to make the equations hold definitionally. Those issues can only be addressed with realistic examples. So far, I haven't seen an example which wasn't just made up to illustrate the phenomenon, which rather makes it a low priority in my mind.
Meanwhile...
Let's consider the following example which has a dependent type. T [m,n:Nat] : Type c1 : T 2 4 c2 : T 2 5 c3 : T 2 5 c4 : T 7 9 c5 : T 7 9 c6 [m:Nat] : T m (succ m) -> T m m c7 [m,n,r:Nat] : T m n -> T n r -> T m r Now, we want to define a function f as follows.
You might. I don't. Why not?
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.
I find it quite frustrating when you don't actually discuss the points I make, but rather continue to make the same invalid arguments as if I had said nothing. Because I have some respect for you, I take the time to quote from your messages and respond to the points you make in detail. I hope you do not consider this arrogant or offensive, even if it is inconvenient.
All the best Conor
