"with" looses information needed for termination

[GoogleCodeExporter]

The current implementation of "with" by translation into an auxiliary function looses the connection

  suc (suc n) < suc n

in the example

  f : Nat -> Nat
  f zero = zero
  f (suc zero) = zero
  f (suc (suc n)) with zero
  ... | m = f (suc n)

Hence, termination checking fails.

What version of Agda are you using? 2.2.7 (darcs, 2010-01-10)
On what operating system? Any

Maybe the relation of input "suc (suc n)" and recursive argument "suc n" could be recovered if one adds some dummy arguments to the generated auxiliary function.

Original issue reported on code.google.com by andreas....@gmail.com on 11 Jan 2010 at 9:56

• Merged into: Improving termination checking of functions defined using with #59

Attachments:

• TerminationTwoConstructors.agda

[GoogleCodeExporter]

This is related to bug #59, but does not involve as-patterns. So the problem is maybe exhibited more clearly here.

Original comment by andreas....@gmail.com on 11 Jan 2010 at 9:57

[GoogleCodeExporter]

Original comment by nils.anders.danielsson on 11 Jan 2010 at 1:10

• Changed state: Duplicate