<div dir="ltr"><div><div>I'm a newbie to reflection in Agda and am excited to learn the new-reflection machinery. I'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 "by-hand" 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'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>