Documentation missing on backtick import of types

[weaversa]

module parmodule where

parameter
        type k : #
        type constraint (fin k)

type ParObj = [k]

module parmoduleUser where

import `parmodule

type n = 8

type UserObj = ParObj n  // This is undocumented.

x : UserObj
x = 10

See: https://github.com/GaloisInc/cryptol/blob/master/docs/Syntax.md

The documentation there would lead one to believe the correct way to define this type is to do type UserObj = ParObj {k = n}.

[yav]

The plan is to remove this feature, so I am not sure we should invest much effort in documenting it.

[yav]

This feature was not removed, and is now documented here:
https://galoisinc.github.io/cryptol/master/Modules.html#instantiation-by-parametrizing-declarations