<div dir="ltr"><div dir="ltr"><br></div><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Jan 31, 2019 at 5:53 PM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex">On Thu, 2019-01-31 at 18:40 +0300, Sergei Meshveliani wrote:<br>
<br>
> <br>
> And in my example of  test0 = remainder (divRem 520 10),  <br>
> proofs are not evaluated in the compiled program.<br>
> <br>
> Now, return to Agda interpreter.<br>
> [..]<br>
<br>
<br>
Consider a more clear example of test1:<br>
<br>
<br>
-- of Binary-4.2 ---------------------------------------------------<br>
open import Binary using (Bin; 0#; 1#; 2#; 3#; 4#; 5#; _+_; <br>
                                               DivMod; divMod; rem)<br>
10' : Bin<br>
10' = 5# + 5#<br>
<br>
-- test0 = let b = stringToBin "1000001000" in rem b 10' (λ())<br>
<br>
test1 : String → Bin<br>
test1 str =<br>
          let b = stringToBin str in  rem b 10' (λ())<br>
-------------------------------------------------------------<br>
<br>
<br>
First,  C-c C-l  is applied.<br>
rem  is here  remainder (divRem b 10' _).<br>
<br>
test1  is type-checked, together with all functions needed for divRem.<br>
<br>
Is it known after this that no proofs need to be evaluated for<br>
evaluation of  test1 ?</blockquote><div><br></div><div>No, why would you think that? Also it's not clear what you mean by "evaluation of test1".</div><div>Do you mean using the compile-time evaluator, running the compiled code, or some hypothetical</div><div>ideal evaluator.</div><div><br></div><div>/ Ulf </div></div></div>