[Agda] Why unification fail?

[Serge Leblanc]

Hi every,

Would anyone please tell me why the unification fails in the following
example and what I do to succeed?

Thank you for your help.

Saluton ĉiun,

Ĉu iu bonvolus indiki al mi la kialon pro la unuiĝo fiaskas en la sekva
ekzemplo kaj kion mi faru por sukcesi? 

Sinceran dankon pro via helpo.

-- 

Serge Leblanc
------------------------------------------------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190306/3e1e1e9d/attachment.html>
-------------- next part --------------
module Chomp1 where

  open import Data.Nat --as ℕ
  open import Data.Nat.Properties


  --open import Function using (id ; _∘_)
  open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_ ; refl) -- ; _≗_ ; refl ; sym ; trans ; cong ; cong₂ ; cong-app)
  open PropEq.≡-Reasoning


  infixr 15 _∷_

  data 𝕃′ : Set where
    [_] : (o : ℕ) → 𝕃′
    _∷_ : (x : ℕ) → (xs : 𝕃′) → 𝕃′

  head : 𝕃′ → ℕ
  head [ o ] = o
  head (h ∷ _) = h

  ŋ : 𝕃′ → ℕ
  ŋ [ o ] = o
  ŋ (h ∷ t) = h + ŋ t

  proofₒ : ∀ n → ŋ [ n ] ≡ n
  proofₒ n = refl

  proof₁ : ŋ (3 ∷ 2 ∷ [ 5 ]) ≡ 10
  proof₁ = refl

  l₁ = 3 ∷ 2 ∷ [ 4 ]

  Ō : (i : ℕ) → (l : 𝕃′) → Ordering i (ŋ l)
  Ō i l = compare i (ŋ l)

  private
    proof₂ : Ō 3 l₁ ≡ less 3 5
    proof₂ = refl

    proof₃ : Ō 9 l₁ ≡ equal 9
    proof₃ = refl

    proof₄ : Ō 11 l₁ ≡ greater 9 1
    proof₄ = refl

  ⪾ : ℕ → 𝕃′ → 𝕃′
  ⪾ i l with compare i (ŋ l)
  ... | less m k = {!   !}
  ... | equal m = l
  ... | greater m k = suc k ∷ l
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190306/3e1e1e9d/attachment.sig>