Notation in a post-renamer work

[nomeata]

This is not pressing, but I wanted to note down some thoughts before I lose them.

We currently Require imported modules (no Import), and every imported entity is addressed fully qualified (GHC.Base.map). This is nice, as we don’t have to worry about Haskell’s complex import/export structure or have problems with definitions that have clashing names.

This unfortunately does not allow us to use nice notation, in particular for binary operators. All these are now prefix operators (with z-encoded names…).

Here are two variants to work around this:

• All definitions become Local Definition, all imports becomes Require Import. Because the definitions are Local, the Import does not import them, so we are in basically the situation as above. But we do get all notations.

  The disadvantage is that if we want the definitions to be in scope unqualified (e.g. for proving), then we cannot do that.

• Slightly better: Every module defines all notations in a Module Notations. … End Notations. block. We import a module Foo with Require Foo. Import Foo.Notations.

  This should fix the problem with getting the names unqualified if we want to. A downside is the slightly more verbose importing (but I think it is fine.)

  If we want to use Foo’s notation inside Foo, we can simply declare every Notation twice: Once in the code, right after its definition, and then again all Notations at the end of the file, in the Notations module.

Orthogonal issue: Do we want an operator + in Foo to be (also) available as _Foo.+_, i.e. a infix-but-manually-qualified version?

[nomeata]

With all names qualified, this (the second variant) becomes feasible now.