<div dir="ltr"><div><div>I&#39;m a newbie to reflection in Agda and am excited to learn the new-reflection machinery. I&#39;m starting by working through the example of induction in Tactic.Nat.<br><br>  induction-example : ∀ n → sum (downFrom n) * 2 ≡ n * (n + 1)<br>  induction-example = induction<br><br></div>I tried to figure out what the induction macro is doing and came up with this:<br><br></div><div>  by-hand : ∀ n → sum (downFrom n) * 2 ≡ n * (n + 1)<br>  by-hand = nat-induction (λ n → sum (downFrom n) * 2 ≡ n * (n + 1)) auto (λ n eq → by eq)<br><br></div><div>So far, great. I also tried:<br><br>  unsolved-metas : ∀ n → sum (downFrom n) * 2 ≡ n * (n + 1)<br>  unsolved-metas n = induction n<br><br></div><div>but that produces 3 yellow-highlighted errors. However, there are no such problems in the &quot;by-hand&quot; version:<br></div><div><br>  by-hand-2 : ∀ n → sum (downFrom n) * 2 ≡ n * (n + 1)<br>  by-hand-2 n = nat-induction (λ n → sum (downFrom n) * 2 ≡ n * (n + 1)) auto (λ n eq → by eq) n<br></div><div><br></div><div>I&#39;m confused. TIA for help in understanding this.<br clear="all"></div><div><div><div><div><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">--<br>Martin Stone Davis<br><div><br>Postal/Residential:<br></div><div style="margin-left:40px"><span>1223 Ferry St</span><span><span><br></span></span></div><div style="margin-left:40px"><span><span>Apt 5<br></span></span></div><div style="margin-left:40px"><span>Eugene, OR 97401</span><br></div>Talk / <span></span>Text / Voicemail: <a href="tel:3106993578" value="+13106993578" target="_blank">(310) 699-3578</a><br>Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a><div><div><div><span></span></div></div></div></div></div><div dir="ltr"><span style="font-size:small">Website: </span><a href="http://martinstonedavis.com/" style="color:rgb(17,85,204);font-size:small" target="_blank">martinstonedavis.com</a></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div>
</div></div></div></div>