NewtypesResolution.dfy(5,7): Error: Cycle among redirecting types (newtypes, type synonyms): MySynonym -> MyIntegerType_WellSupposedly -> MyNewType -> MySynonym
NewtypesResolution.dfy(12,10): Error: newtypes must be based on some numeric type (got List<int>)
NewtypesResolution.dfy(38,9): Error: arguments must have the same type (got posReal and real)
NewtypesResolution.dfy(44,9): Error: arguments must have the same type (got int32 and int)
NewtypesResolution.dfy(50,13): Error: arguments must have the same type (got posReal and int32)
NewtypesResolution.dfy(51,13): Error: arguments to <= must have the same type (got posReal and int32)
NewtypesResolution.dfy(52,13): Error: arguments to < must have the same type (got int32 and int)
NewtypesResolution.dfy(53,13): Error: arguments to > must have the same type (got posReal and real)
NewtypesResolution.dfy(57,13): Error: first argument to % must be of type int (instead got posReal)
NewtypesResolution.dfy(57,25): Error: first argument to % must be of type int (instead got real)
NewtypesResolution.dfy(75,8): Error: newtype constraint must be of type bool (instead got SmallInt)
NewtypesResolution.dfy(77,10): Error: unresolved identifier: a
NewtypesResolution.dfy(91,31): Error: old expressions are not allowed in this context
NewtypesResolution.dfy(101,24): Error: Wrong number of type arguments (1 instead of 0) passed to newtype: N
NewtypesResolution.dfy(105,10): Error: recursive dependency involving a newtype: _default.BadLemma -> Cycle
NewtypesResolution.dfy(114,10): Error: recursive dependency involving a newtype: SelfCycle -> SelfCycle
NewtypesResolution.dfy(120,21): Error: name of type (N9) is used as a variable
NewtypesResolution.dfy(139,6): Error: RHS (of type int) not assignable to LHS (of type Int)
NewtypesResolution.dfy(140,6): Error: RHS (of type AnotherInt) not assignable to LHS (of type Int)
NewtypesResolution.dfy(156,9): Error: name of type (B) is used as a variable
NewtypesResolution.dfy(157,11): Error: name of type (Syn) is used as a variable
NewtypesResolution.dfy(162,8): Error: member 'U' does not exist in type 'Y'
NewtypesResolution.dfy(162,9): Error: expected method call, found expression
NewtypesResolution.dfy(188,60): Error: incorrect type of datatype constructor argument (found Dt<bool>, expected S)
NewtypesResolution.dfy(219,11): Error: new must use an integer-based expression for the array size (got real for index 2)
NewtypesResolution.dfy(221,13): Error: arguments to < must have the same type (got Even and nat)
NewtypesResolution.dfy(223,13): Error: arguments to < must have the same type (got Even and int)
NewtypesResolution.dfy(227,13): Error: arguments to < must have the same type (got Even and int)
NewtypesResolution.dfy(229,13): Error: arguments to < must have the same type (got Even and int)
NewtypesResolution.dfy(230,13): Error: arguments to < must have the same type (got Even and int)
NewtypesResolution.dfy(238,13): Error: arguments to < must have the same type (got Even and int)
NewtypesResolution.dfy(240,13): Error: arguments to <= must have the same type (got Even and int)
NewtypesResolution.dfy(249,17): Error: multiset update requires integer-based numeric value (got real)
33 resolution/type errors detected in NewtypesResolution.dfy