Don't export record constructor names

[janmasrovira]

Context

It is a common pattern to define record types with a single constructor named mk<Type>. E.g.

type MyRecord :=
  mkMyRecord@{
    ...
 };

The suffix of mk is just qualifying to constructor to avoid conflicts with other record types. However, since Juvix already allows qualified names, perhaps it would be more adequate to use those and avoid unnecessary verbosity in the declaration site.

Proposal

There are several ways we could improve the most common pattern. We could choose any of these options:

1. Do not export constructors named mk.
2. Do not export single constructors.
3. Do not export single constructors with record syntax. E.g. myConstr@{field1; ..};

For any of these cases the constructor would only be accessible through the type module. E.g. MyType.mk.

[lukaszcz]

The most uniform solution would be to not export any constructor names by default (like e.g. in Lean). This also would make name clashes less likely. Common data structures like lists could just have the constructors explicitly exported right after the definition:

type List A :=
  | nil : List A
  | :: : A -> List A -> List A;

open List using {nil; ::} public;
-- or
open List using {List constructors} public;

[janmasrovira]

The most uniform solution would be to not export any constructor names by default (like e.g. in Lean). This also would make name clashes less likely. Common data structures like lists could just have the constructors explicitly exported right after the definition:

type List A :=
  | nil : List A
  | :: : A -> List A -> List A;

open List using {nil; ::} public;
-- or
open List using {List constructors} public;

Approved

[jonaprieto]

Nice, less verbose; please update the docs when you can. ;)