cryptol/tests/issues/Issue883_Sig.cry
Iavor Diatchki 192b25c508 Bug fixes to the modules system.
This fixes #796.
It also fixes the @bboston7's example on #883, but not the original
example in #883.   The issue there is that `asdf` function generates
a constraint only involving the module parameter.

Normally we don't try to solve constraint that don't mention a schema's
parameters, because they can always be solved "later", and hopefully with
more things instantiated.

The weird thing in this case is that the schema adds *local" constraint to
the module parameters, but we end up ignoring these.
2020-11-11 14:35:33 -08:00

9 lines
128 B
Plaintext

module Issue883_Sig where
parameter
type w : #
type constraint (fin w)
getZeros : [w/8][8]
getZeros = split`{each=8} zero