[Agda] inferType yields a metavariable

[Martin Stone Davis]

What if there were a continueAfterMeta : (xs : List Meta) → (tc : TC A) →
TC A, which would run tc after any one of the xs were solved?

--
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

On Fri, Feb 26, 2016 at 12:03 AM, Ulf Norell <ulf.norell at gmail.com> wrote:

> Hmm, that's trickier. It's the forceFun that makes it possible to solve
> the target type, but when you blockOnMeta you lose that work. Not sure
> what's needed to make this work.
>
> / Ulf
>
> On Fri, Feb 26, 2016 at 8:40 AM, Martin Stone Davis <
> martin.stone.davis at gmail.com> wrote:
>
>> Thanks, that worked. But how about this slightly-more-complicated
>> example? If I remove "id", the goal gets reported as _n → Set, which is
>> fine for me, since I just care about seeing that it's 'Set'. However, with
>> "id", it's _n → _m. I'm not finding that blockOnMeta helps here.
>>
>>     open import Prelude
>>     open import Tactic.Reflection
>>
>>     macro
>>       infer-the-goal₂ : Tactic
>>       infer-the-goal₂ hole = do
>>         goal ← forceFun =<< inferType hole -|
>>         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
>>
>> On Thu, Feb 25, 2016 at 9:41 PM, Ulf Norell <ulf.norell at gmail.com> wrote:
>>
>>> 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/696b40f7/attachment.html