[Agda] Recursive Sets / refine vs. load

[Altenkirch Thorsten]

Could you make this more precise, Andreas?

It seems that the approach using equations also exploits that we define
everything top-level.
I don't see how to generalize this in a way which would extend uniformly
to eliminators appearing
anywhere. But maybe this is just my limitation...

Cheers,
Thorsten

On 27/03/2012 21:07, "Andreas Abel" <andreas.abel at ifi.lmu.de> wrote:

> Well, you could make sense of this, even if thinking it as a case.
> But then, the boundary between type-checked code that can be evaluated
> and not-yet-type-checked code is within terms, not only declarations.
>
> Cheers,
> Andreas
>
> On Sun, 25 Mar 2012 16:55:36 +0100, Altenkirch Thorsten wrote:
>> To me pattern matching is just a shorthand for using eliminators such
>> as case. In this view it is hard to make sense of your suggestion.
>>
>> Cheers,
>> Thorsten
>>
>> Sent from my iPad
>>
>> On 24 Mar 2012, at 22:13, "Nils Anders Danielsson" <nad at chalmers.se>
>> wrote:
>>
>>> On 2012-03-24 18:12, Brandon Moore wrote:
>>>> The following definition looks reasonable to me,
>>>> the type of the hole is reported as ℕ → Set,
>>>> and refine/give accepts what I've written there,
>>>> but then typechecking the file fails, saying
>>>> t true !=< ℕ of type Set
>>>
>>> [...]
>>>
>>>> t : Bool → Set
>>>> t true = ℕ
>>>> t false = Σ (t true) {!Vec Bool!}
>>>>
>>>> Why isn't this definition accepted?
>>>
>>> Because (non-mutual) definitions are not unfolded before they have
>>> been
>>> type-checked. Unfortunately this does not apply to goals: Agda
>>> forgets
>>> that t should not unfold when Vec Bool is type-checked. This is a
>>> long-standing bug:
>>>
>>>   http://code.google.com/p/agda/issues/detail?id=118
>>>
>>> --
>>> /NAD
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>> This message and any attachment are intended solely for the addressee
>> and may contain confidential information. If you have received this
>> message in error, please send it back to me, and immediately delete
>> it.   Please do not use, copy or disclose the information contained
>> in
>> this message or in any attachment.  Any views or opinions expressed
>> by
>> the author of this email do not necessarily reflect the views of the
>> University of Nottingham.
>>
>> This message has been checked for viruses but the contents of an
>> attachment
>> may still contain software viruses which could damage your computer
>> system:
>> you are advised to perform your own checks. Email communications with
>> the
>> University of Nottingham may be monitored as permitted by UK
>> legislation.
>
>-- 
> Andreas Abel  <><     Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> http://www.tcs.informatik.uni-muenchen.de/~abel/
>_______________________________________________
>Agda mailing list
>Agda at lists.chalmers.se
>https://lists.chalmers.se/mailman/listinfo/agda