UlfNorell
commented
10 years ago From sanzhi...@gmail.com on October 04, 2013 01:27:31
Reduced further:
module X where
foo : ℕ × ℕ -> R
foo (suc m , n) = foo (m , suc n)
foo (zero , _) = ø
module Y where foo : ℕ → ℕ -> R foo (suc m) n = foo m (suc n) foo zero _ = ø
From sanzhi...@gmail.com on October 04, 2013 10:21:38
In the following, Agda-2.3.2 accepts both definitions, while the darcs version doesn't like X.foo:
data ℕ : Set where zero : ℕ suc : ℕ -> ℕ
data List (A : Set) : Set where [] : List A ∷ : A -> List A -> List A
record × (A B : Set) : Set where constructor , field proj₁ : A proj₂ : B
data T : Set where node : List T -> T step : T -> T
postulate f : List T -> List T R : Set ∙ : R -> R -> R ø : R
module X where mutual foo : T -> ℕ × ℕ -> R foo (node x) n = foos x n
foos : List T -> ℕ × ℕ -> R foos [] _ = ø foos (x ∷ xs) (suc n , m) = foo x (suc n , suc m) ∙ foos (f xs) (n , suc m) foos (x ∷ xs) n = { }0
module Y where mutual foo : T -> ℕ → ℕ -> R foo (node x) n m = foos x n m
foos : List T -> ℕ → ℕ -> R foos [] = ø foos (x ∷ xs) (suc n) m = foo x (suc n) (suc m) ∙ foos (f xs) n (suc m) foos (x ∷ xs) n m = { }1
Original issue: http://code.google.com/p/agda/issues/detail?id=915