UlfNorell
commented
10 years ago From vitus...@gmail.com on December 11, 2013 09:26:13
Related (from patch notes):
- A buggy facility coined "matrix-shaped orders" that supported uncurried functions (which take tuples of arguments instead of one argument after another) has been removed from the termination checker. [ Issue 787 ]
From jesper.c...@gmail.com on December 11, 2013 17:21:10
In the following code, is there a good reason why test is rejected by the termination checker, but test₂ isn't? I have some examples where it is more natural to work with uncurried functions, but the termination checker won't let me.
== BEGIN CODE ==
open import Data.Nat using (ℕ; zero; suc) open import Data.Product using (,; ×)
test : Set × ℕ → ℕ test (A , zero ) = zero test (A , suc n) = test (ℕ , n)
test₂ : Set → ℕ → ℕ test₂ A zero = zero test₂ A (suc n) = test₂ ℕ n
== END CODE ==
Original issue: http://code.google.com/p/agda/issues/detail?id=995