[Agda] Recursive Sets / refine vs. load

[Andreas Abel]

 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/