Explain the purpose of # and * for constraining deferred types in interface module specifications in the docs

[Frank-Zeyda]

Dear Cryptol Developers,

From some of the examples in cryptol-specs, I noticed that the following syntax is frequently used in interface module definitions to constraint abstract (deferred) types:

type A : #
type B : *

I may be mistaken but could not find a designated section in the reference manual that describes these operators in detail, i.e., from a syntactic, intuitive, and semantic point of view.

In case I missed something in:

https://galoisinc.github.io/cryptol/master/RefMan.html

please feel free to ignore and close the issue, perhaps with a note where an explanation can be found. Otherwise, I would recommend to formally introduce and explain these notations in the reference manual for the sake of completeness, including any other related notations to constraining deferred types in this manner.

[Frank-Zeyda]

PS: I realized that this might be a duplicate of Issue 1711 (Add some information about # and * to the reference manual).