> > On Jun 19, 2006, at 4:15 PM, Yong Luo wrote: > > > I wonder if your coverage checker is even weaker than Epigram's > > case-splitting. > > For example, we have an inductive data as follows. > > > > T [n:Nat] : Set > > c1 : T 3 > > c2 : T 100 > > c3 : T 100 > > > > And now we want to define the following function: > > > > f : (n:Nat) -> T n -> Nat > > f 3 c1 = 0 > > f 100 x = 1 > > > > I am not sure whether you need to expand it to more than 100 cases > > in order > > to check the totality. > > I'm not sure what you mean by weaker.
I am not sure either whether Epigram does better. > Indeed the coverage checker > will expand this to 102 (or something) cases, but it will have no > trouble seeing that all the missing cases are impossible. > Do you still need to prove something like for all n:Nat, T (n+101) is empty ? Yong
