The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Hello.

Is it possible to declare types inside module such way that I can pattern match on them outside of the module?
(When I define module satisfying signature I must declare types with Definition or wrap Inductive/Record with it;
that makes type content invisible to module users; I suspect that this behaviour is implemented intentionally.)

Sincerely,
Kirill Taran