[Agda] Question about the meaning of 'abstract'

[Daniel Peebles]

Oh wait, nevermind. I thought opaque was proved by refl. In this case, I
think your definition of opaque is fine. If refl worked there, my previous
email would stand.


On Thu, Nov 15, 2012 at 8:58 PM, Daniel Peebles <pumpkingod at gmail.com>wrote:

> I'd say no. The current behavior means that somehow the unification
> mechanism is seeing through the abstraction? I'd like to be able to prove
> see-through, but opaque violates abstraction, in my opinion.
>
>
> On Thu, Nov 15, 2012 at 6:33 PM, Andreas Abel <andreas.abel at ifi.lmu.de>wrote:
>
>> If you have an abstract definition
>>
>>   abstract
>>     lhs = rhs
>>
>> is it ok with the meaning of `abstract' that
>>
>>   lhs == rhs
>>
>> holds propositionally outside the abstract block.  Agda currently says
>> yes, but would you agree with Agda?
>>
>>   abstract
>>
>>     T : Set -> Set
>>     T A = A
>>
>>     see-through : ∀ {A} → T A ≡ A
>>     see-through = refl
>>
>>   opaque : ∀ {A} → T A ≡ A
>>   opaque = see-through
>>
>> Cheers,
>> Andreas
>>
>> --
>> Andreas Abel  <><      Du bist der geliebte Mensch.
>>
>> Theoretical Computer Science, University of Munich
>> Oettingenstr. 67, D-80538 Munich, GERMANY
>>
>> andreas.abel at ifi.lmu.de
>> http://www2.tcs.ifi.lmu.de/~**abel/ <http://www2.tcs.ifi.lmu.de/~abel/>
>> ______________________________**_________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121115/911f6efe/attachment.html