> 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?
I am not sure whether this is an artificial example because similar examples are used by others as well. > > >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. > 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. > Not at all. I apologise again. Yong
