[Agda] Question about the meaning of 'abstract'

Nils Anders Danielsson nad at chalmers.se
Fri Nov 16 12:02:30 CET 2012

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.


More information about the Agda mailing list