[Agda] [new-reflection] unsolved metas in induction

[Martin Stone Davis]

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.

  induction-example : ∀ n → sum (downFrom n) * 2 ≡ n * (n + 1)
  induction-example = induction

I tried to figure out what the induction macro is doing and came up with
this:

  by-hand : ∀ n → sum (downFrom n) * 2 ≡ n * (n + 1)
  by-hand = nat-induction (λ n → sum (downFrom n) * 2 ≡ n * (n + 1)) auto
(λ n eq → by eq)

So far, great. I also tried:

  unsolved-metas : ∀ n → sum (downFrom n) * 2 ≡ n * (n + 1)
  unsolved-metas n = induction n

but that produces 3 yellow-highlighted errors. However, there are no such
problems in the "by-hand" version:

  by-hand-2 : ∀ n → sum (downFrom n) * 2 ≡ n * (n + 1)
  by-hand-2 n = nat-induction (λ n → sum (downFrom n) * 2 ≡ n * (n + 1))
auto (λ n eq → by eq) n

I'm confused. TIA for help in understanding this.
--
Martin Stone Davis

Postal/Residential:
1223 Ferry St
Apt 5
Eugene, OR 97401
Talk / Text / Voicemail: (310) 699-3578 <3106993578>
Electronic Mail: martin.stone.davis at gmail.com
Website: martinstonedavis.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160122/0a38a29d/attachment.html