mutual-merge.agda

open import Data.String as String using (String; fromList)
open import Data.Nat              using (ℕ; zero; suc; _+_; _*_; _<′_; _≤′_)
open import Data.Nat.Properties  
open import Data.Bool             using (Bool; true; false; if_then_else_)
open import Data.List   hiding (merge; partition)
open import Data.List.Properties  using (map-id; map-compose)
open import Data.Product          using (Σ; Σ-syntax; _,_; proj₁; proj₂; _×_; map)
open import Data.Sum   as Sum     using (_⊎_; inj₁; inj₂; map)
open import Data.Unit             using (⊤; tt)
open import Data.Empty            using (⊥; ⊥-elim)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; cong; cong₂; cong-app; sym; trans; subst; module ≡-Reasoning)
open ≡-Reasoning
open import Relation.Nullary      using (¬_; Dec; yes; no)
open import Induction.WellFounded
open import Relation.Binary
open import Data.Nat.Induction


mutual
  merge : List ℕ -> List ℕ -> List ℕ
  merge [] x₁ = x₁
  merge (x ∷ x₂) [] = x ∷ x₂  
  merge (x ∷ xs) (y ∷ ys) with x ≤? y
  merge (x ∷ xs) (y ∷ ys) | yes _ = x ∷ merge xs (y ∷ ys)
  merge (x ∷ xs) (y ∷ ys) | no _ = y ∷ merge' x xs ys
  
  merge' : ℕ -> List ℕ -> List ℕ -> List ℕ
  merge' x x₁ [] = x ∷ x₁
  merge' x xs (y ∷ ys) with  x ≤? y
  merge' x xs (y ∷ ys)  | yes _ = x ∷ merge xs (y ∷ ys)
  merge' x xs (y ∷ ys)  | no _ = y ∷ merge' x xs ys

相同的逻辑分别用agda和coq写
coq无法编译，请教一下原因