[Agda] Question about the meaning of 'abstract'

[Dan Licata]

Arggh, I got private and abstract confused.  Thanks for the correction!  -Dan

On Nov16, Nils Anders Danielsson wrote:
> On 2012-11-16 04:20, Dan Licata wrote:
>> BTW, Agda is already a little leaky when it comes to abstract, which
>> came up in relation to faking higher inductive types a few months ago.
>> As I recall, the problem is that there is no way to stop Agda from
>> exporting the fact that
>>
>> chalk == cheese -> void
>>
>> when chalk and cheese are abstract but defined to be datatype
>> constructors inside the abstraction, because they still reduce during
>> type checking and you can use an absurd pattern to match on the
>> equality.
>
> This discussion was unrelated to "abstract". The construction used a
> private but non-abstract data type.
>