Re: [m-users.] Import only notations from a module?

On Wed, Jul 17, 2024 at 7:56 PM Anders Lundstedt
<[email protected]> wrote:
>
> On Mon, Jul 15, 2024 at 5:17 AM Mark Brown <[email protected]> wrote:
> > I'd also like to be able to define name equivalences for things other
> > than types, modes and insts
>
> I would really like such a feature!
>
>
> > > I would be fine with having to redefine notations, as for example in
> > > the following non-compiling attempt (which does compile if one imports
> > > the list module and removes my attempt at redefining the notations).
> >
> > Redefining them as functions loses some information, since there's
> > things we know about constructors that don't apply to functions
> > generally. In particular, when constructors are viewed as functions:
> >  - they are injective
> >  - their ranges are disjoint
>
> Yeah, I figured that ought to be the problem. I guess your suggestion
> of additional name equivalences would solve it?

I was wishing, same as you. My suggestion was that wishing would be
the easy part :-)

>
>
> On Sat, Jul 13, 2024 at 1:53 PM Anders Lundstedt
> <[email protected]> wrote:
> > I like using ‘use_module’ instead of ‘import_module’ since this forces
> > me to properly qualify names. However, some notations would be nice to
> > have—in particular, list notations.
>
> All in all, I gather that right now it is not possible to accomplish
> what I want?

No, you have to take the interface that the module author gives you.

>
>
> Best,
>
> Anders
_______________________________________________
users mailing list
[email protected]
https://lists.mercurylang.org/listinfo/users