Parameterized Module Type Error

[michaelabernardo]

Hi there!

I have a module kind of like this:

module test where

parameter

  a : Z b

  type b : #
  type constraint (fin b, b >= 1)

and I get this error:

[error] at test.cry:1:1--8:34:
  Failed to validate user-specified signature.
    in the definition of 'test::a', at test.cry:5:3--5:4,
    we need to show that
      for any type test::b
      the following constraints hold:
        • fin test::b
            arising from
            use of partial type function Cryptol::Z
            at test.cry:5:7--5:10
        • test::b >= 1
            arising from
            use of partial type function Cryptol::Z
            at test.cry:5:7--5:10

I'm not sure how to fix it. It worked in older versions of Cryptol.

[michaelabernardo]

(Cryptol version 2.11.0.99)

[robdockins]

Looks like the same as #1240?

[michaelabernardo]

My bad! Sorry about that!