[Agda] Question about the meaning of 'abstract'

[Nils Anders Danielsson]

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.

-- 
/NAD