<div dir="ltr"><div>Here is a simple program that works in Idris but not in agda. Is there a way to make it work in agda?<br><br></div>agda:<br> <br><div>```<br><pre><span class="gmail-hs-keyword">module</span> <span class="gmail-hs-varid">terminate</span> <span class="gmail-hs-keyword">where</span>
<span class="gmail-hs-definition">open</span> <span class="gmail-hs-keyword">import</span> <span class="gmail-hs-conid">Data</span><span class="gmail-hs-varop">.</span><span class="gmail-hs-conid">Nat</span>
<span class="gmail-hs-definition">fn</span> <span class="gmail-hs-conop">:</span> <span class="gmail-hs-conid">ℕ</span> <span class="gmail-hs-sel">→</span> <span class="gmail-hs-conid">ℕ</span>
<span class="gmail-hs-definition">fn</span> <span class="gmail-hs-varid">zero</span> <span class="gmail-hs-keyglyph">=</span> <span class="gmail-hs-varid">zero</span>
<span class="gmail-hs-definition">fn</span> <span class="gmail-hs-layout">(</span><span class="gmail-hs-varid">suc</span> <span class="gmail-hs-varid">k</span><span class="gmail-hs-layout">)</span> <span class="gmail-hs-keyglyph">=</span> <span class="gmail-hs-varid">zero</span>
<span class="gmail-hs-definition">gn</span> <span class="gmail-hs-conop">:</span> <span class="gmail-hs-conid">ℕ</span> <span class="gmail-hs-sel">→</span> <span class="gmail-hs-conid">ℕ</span>
<span class="gmail-hs-definition">gn</span> <span class="gmail-hs-varid">x</span> <span class="gmail-hs-keyglyph">=</span> <span class="gmail-hs-varid">zero</span>
<span class="gmail-hs-keyword">data</span> <span class="gmail-hs-conid">Test</span> <span class="gmail-hs-conop">:</span> <span class="gmail-hs-conid">ℕ</span> <span class="gmail-hs-sel">→</span> <span class="gmail-hs-conid">Set</span> <span class="gmail-hs-keyword">where</span>
<span class="gmail-hs-conid">Tist</span> <span class="gmail-hs-conop">:</span> <span class="gmail-hs-conid">Test</span> <span class="gmail-hs-varid">zero</span>
<span class="gmail-hs-conid">Tost</span> <span class="gmail-hs-conop">:</span> <span class="gmail-hs-layout">(</span><span class="gmail-hs-varid">n</span> <span class="gmail-hs-conop">:</span> <span class="gmail-hs-conid">ℕ</span><span class="gmail-hs-layout">)</span> <span class="gmail-hs-sel">→</span> <span class="gmail-hs-conid">Test</span> <span class="gmail-hs-layout">(</span><span class="gmail-hs-varid">fn</span> <span class="gmail-hs-varid">n</span><span class="gmail-hs-layout">)</span>
<span class="gmail-hs-definition">tn</span> <span class="gmail-hs-conop">:</span> <span class="gmail-hs-layout">(</span><span class="gmail-hs-varid">n</span> <span class="gmail-hs-conop">:</span> <span class="gmail-hs-conid">ℕ</span><span class="gmail-hs-layout">)</span> <span class="gmail-hs-sel">→</span> <span class="gmail-hs-conid">Test</span> <span class="gmail-hs-layout">(</span><span class="gmail-hs-varid">fn</span> <span class="gmail-hs-varid">n</span><span class="gmail-hs-layout">)</span> <span class="gmail-hs-sel">→</span> <span class="gmail-hs-conid">ℕ</span>
<span class="gmail-hs-definition">tn</span> <span class="gmail-hs-varid">zero</span> <span class="gmail-hs-conid">Tist</span> <span class="gmail-hs-keyglyph">=</span> <span class="gmail-hs-varid">zero</span>
<span class="gmail-hs-definition">tn</span> <span class="gmail-hs-varid">zero</span> <span class="gmail-hs-layout">(</span><span class="gmail-hs-conid">Tost</span> <span class="gmail-hs-varid">zero</span><span class="gmail-hs-layout">)</span> <span class="gmail-hs-keyglyph">=</span> <span class="gmail-hs-varid">zero</span>
<span class="gmail-hs-definition">tn</span> <span class="gmail-hs-varid">zero</span> <span class="gmail-hs-layout">(</span><span class="gmail-hs-conid">Tost</span> <span class="gmail-hs-layout">(</span><span class="gmail-hs-varid">suc</span> <span class="gmail-hs-varid">k</span><span class="gmail-hs-layout">)</span><span class="gmail-hs-layout">)</span> <span class="gmail-hs-keyglyph">=</span> <span class="gmail-hs-varid">zero</span>
<span class="gmail-hs-definition">tn</span> <span class="gmail-hs-layout">(</span><span class="gmail-hs-varid">suc</span> <span class="gmail-hs-varid">y</span><span class="gmail-hs-layout">)</span> <span class="gmail-hs-varid">x</span> <span class="gmail-hs-keyglyph">=</span> <span class="gmail-hs-layout">{</span><span class="gmail-hs-varop">!!</span><span class="gmail-hs-layout">}</span>
</pre><br>```<br><br></div><div>idris:<br><br>```<br>module Main <br><br>%default total<br><br>fn : Nat -> Nat<br>fn Z = Z<br>fn (S k) = Z<br><br>gn : Nat -> Nat<br>gn x = Z<br><br><br>data Test : Nat -> Type where<br> Tost : (n : Nat) -> Test $ fn n<br> Tist : Test Z<br> <br> <br>tn : (n : Nat) -> Test $ fn n -> Nat<br>tn Z Tist = ?tn_rhs_3<br>tn Z (Tost Z) = ?tn_rhs_3<br>tn Z (Tost (S k)) = ?tn_rhs_3<br>tn (S k) x = ?tn_rhs_2<br><br>```<br></div></div>