[Agda] Question about the meaning of 'abstract'

[Daniel Peebles]

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/fcac1224/attachment.html