cryptol/tests/issues/Issue883_Sig.cry

module Issue883_Sig where

parameter
  type w : #
  type constraint (fin w)

getZeros : [w/8][8]
getZeros = split`{each=8} zero
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-12 01:35:33 +03:00			`module Issue883_Sig where`

			`parameter`
			`type w : #`
			`type constraint (fin w)`

			`getZeros : [w/8][8]`
			getZeros = split`{each=8} zero