<div dir="ltr">Hi:<br><br>I am following the <a href="https://plfa.github.io/">https://plfa.github.io/</a> In this exercise.<br><br><-trans'' : ∀ {m n p : ℕ}<br>  → m < n<br>  → n < p<br>    -----<br>  → m < p<br><-trans''  m<n n<p =  -≤-iff-< (≤-trans (s≤s (-≤-iff'-< (m<n))) (-≤-iff'-< n<p))<br><br>I got the error<br><br>suc _m_357 != m of type ℕ<br>when checking that the inferred type of an application<br>  suc _m_357 ≤ _n_358<br>matches the expected type<br>  m ≤ _n_356<br><br><div><img src="cid:ii_k0a8kqx20" alt="agda_error.png" width="490" height="93"><br></div><div>The error is is hard for me to figure out the real wrong place.</div><div><br></div><div>At the end. I find the right way:</div><div><br></div><div><-trans'  m<n n<p =  -≤-iff''-< (-≤-iff-< (≤-trans (s≤s (-≤-iff'-< (m<n))) (-≤-iff'-< n<p)))<br></div><div><br></div><div>So the right answer contain my first try </div><div>`(-≤-iff-< (≤-trans (s≤s (-≤-iff'-< (m<n))) (-≤-iff'-< n<p))`</div><div>When I try to fix the problem. I always want to change `s≤s (-≤-iff'-< (m<n))`</div><div>But it don't work.</div><div><br></div><div>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)</div><div><br></div><div><br></div><div>-------------  The help functions ----------------</div><div>-≤-iff'-< : ∀ {m n : ℕ}<br>  → m < n<br>    -------------<br>  → suc m ≤ n<br>-≤-iff'-< {zero} {suc n} s<n = s≤s z≤n -- 0 < suc n whcich suc 0 <= suc n <br>-≤-iff'-< {suc m} {n} (s<s m<n) = s≤s (-≤-iff'-< m<n)<br><br>-≤-iff''-< : ∀ {m n : ℕ}<br>  → suc m < n<br>    -------------<br>  →  m < n<br>-≤-iff''-< {zero} {suc n} m<n = z<s -- 0 < suc n whcich suc 0 <= suc n <br>-≤-iff''-< {suc m} {n} (s<s m<n) = s<s (-≤-iff''-< m<n)</div><div><div>-------------  The help functions ----------------</div></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div></div>