Thanks. I come across another example:
R[m,n:Nat]:Set r1: R 0 0 r2: (m:Nat) -> T m m -> T m (m+1) r3: (m:Nat) -> T m (m+1) -> T (m+1) (m+1) A function g is defined as follows. g : T 0 1 -> Nat g (r2 0 r1) = 1 Does your coverage checker work for this function? Yong > > > T [n:Nat] : Set > > c1 : T 3 > > c2 : T 100 > > c3 : T 100 > > > > Do you still need to prove something like > > for all n:Nat, T (n+101) is empty ? > > Yes, but that's trivial (first order unification). > > / Ulf >
