[Agda] It is hard to understand the agda error message

[mo jia]

Hi:

I am following the https://plfa.github.io/ In this exercise.

<-trans'' : ∀ {m n p : ℕ}
  → m < n
  → n < p
    -----
  → m < p
<-trans''  m<n n<p =  -≤-iff-< (≤-trans (s≤s (-≤-iff'-< (m<n))) (-≤-iff'-<
n<p))

I got the error

suc _m_357 != m of type ℕ
when checking that the inferred type of an application
  suc _m_357 ≤ _n_358
matches the expected type
  m ≤ _n_356

[image: agda_error.png]
The error is is hard for me to figure out the real wrong place.

At the end. I find the right way:

<-trans'  m<n n<p =  -≤-iff''-< (-≤-iff-< (≤-trans (s≤s (-≤-iff'-< (m<n)))
(-≤-iff'-< n<p)))

So the right answer contain my first try
`(-≤-iff-< (≤-trans (s≤s (-≤-iff'-< (m<n))) (-≤-iff'-< n<p))`
When I try to fix the problem. I always want to change `s≤s (-≤-iff'-<
(m<n))`
But it don't work.

So my question is  how to understand the error message? Or is there some
learning path before following the plfa book? (I suck almost 1 hour to find
out the right way which need the -≤-iff''-< helper)


-------------  The help functions ----------------
-≤-iff'-< : ∀ {m n : ℕ}
  → m < n
    -------------
  → suc m ≤ n
-≤-iff'-< {zero} {suc n} s<n = s≤s z≤n -- 0 < suc n whcich suc 0 <= suc n
-≤-iff'-< {suc m} {n} (s<s m<n) = s≤s (-≤-iff'-< m<n)

-≤-iff''-< : ∀ {m n : ℕ}
  → suc m < n
    -------------
  →  m < n
-≤-iff''-< {zero} {suc n} m<n = z<s -- 0 < suc n whcich suc 0 <= suc n
-≤-iff''-< {suc m} {n} (s<s m<n) = s<s (-≤-iff''-< m<n)
-------------  The help functions ----------------
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190908/84bff312/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: agda_error.png
Type: image/png
Size: 28603 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190908/84bff312/attachment.png>