[Agda] inferType yields a metavariable

[Ulf Norell]

Try blockOnMeta if it comes back a meta.

/ Ulf
On Fri, 26 Feb 2016 at 06:38, Martin Stone Davis <
martin.stone.davis at gmail.com> wrote:

> Is there some way to infer-the-goal as 'Set' in foo (below)? I mean to do
> this within the tactic, not by providing implicits to id. Currently,
> infer-the-goal reports the goal as _n (some metavariable).
>
>   open import Prelude
>   open import Builtin.Reflection
>
>   macro
>     infer-the-goal : Tactic
>     infer-the-goal hole = inferType hole >>= λ goal → typeError (termErr
> goal ∷ [])
>
>   foo : Set
>   foo = id infer-the-goal
>
> --
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160226/c5e04107/attachment.html