Identifiers and Notation

Most Haskell names can be reused as Coq names (fully qualified). However, due to differences in parsing and keywords, hs-to-coq must sometimes modify the generated identifiers.

Coq keywords

The following Coq keywords are automatically translated with an extra _ following them:

Set Type Prop fun fix forall return mod match as
cons pair nil for is with left right exists

Operators

Coq does not allow the definition of identifiers composed with punctuation.

To name these identifiers, hs-to-coq uses GHC’s z-encoding to give textual names to operators. These textual operator names are preceded by op_ and followed by two underscores.

For example, the Haskell identifier == is translated to the Coq identifier GHC.Base.op_zeze__

Notation

Nevertheless, we want users to be able to use the operator syntax, (e.g. ==) in the output. Therefore, hs-to-coq defines appropriate Coq syntax for it:

Notation "'_==_'" := (op_zeze__).
Infix "==" := (op_zeze__) (no associativity, at level 70).

This works fine within the given module (here: GHC.Base), and within every module that imports GHC.Base. But in general, hs-to-coq does not import modules (it only requires them, using Require GHC.Base.), so the notation is not visible.

Therefore, the translated module will contain a Notations submodule at the end:

Module Notations.
Infix "GHC.Base.==" := (op_zeze__) (no associativity, at level 70).
Notation "'_GHC.Base.==_'" := (op_zeze__).
End Notations.

When a module needs to be required, and any of the imported names look like operators, then hs-to-coq imports the the contained Notations module:

Require GHC.Base.
Import GHC.Base.Notation.

This brings the “qualified operators” into scope.

In manually written modules (e.g. those containing the proofs), the user can choose to follow that example, and use all names and operators qualified, or they can Require Import GHC.Base, and use all names and operators unqualified, and ignore the Notations module.

In the rare case that you need to define operators in the preamble, then you have to manually add the Notations as shown here. You put the definition of the syntax for the qualified in a nested module ManualNotation and use the manual notation edit to make hs-to-coq include the ManualNotation module in the generated Notation module.

String Notation

Since Coq 8.9, string syntax notations are now available only when using Import of libraries and not merely Require. The Coq files generated by hs-to-coq will no longer offer these notations by default, either, but can be enabled by importing GHC.Base.Notation, GHC.Err, or the standard Coq libraries. hs-to-coq cunrrently cannot automatically import these notations even if the translated code uses them.