Re: [Why3-club] defining a type invariant

Hi Sandrine, On 11 March 2018 at 17:46, Sandrine Blazy wrote: > Hi, > > I would like to define a type invariant related to an array type. > If I write for example : > type myarray = array int > invariant { forall i:int. 0 <=i< length self -> my_predicate self[i]

[Why3-club] defining a type invariant

Hi, I would like to define a type invariant related to an array type. If I write for example : type myarray = array int invariant { forall i:int. 0 <=i< length self -> my_predicate self[i] } then I get the following error message: type aliases cannot have invariants. So, I changed