git-issue-1180a.dfy.expect

git-issue-1180a.dfy(7,7): Error: declaration 'Opaque' indicates refining (notation `...`), but does not refine anything
git-issue-1180a.dfy(8,7): Error: declaration 'Opaque'' indicates refining (notation `...`), but does not refine anything
git-issue-1180a.dfy(9,11): Error: declaration 'Datatype' indicates refining (notation `...`), but does not refine anything
git-issue-1180a.dfy(10,13): Error: declaration 'Codatatype' indicates refining (notation `...`), but does not refine anything
git-issue-1180a.dfy(11,10): Error: declaration 'Newtype' indicates refining (notation `...`), but does not refine anything
git-issue-1180a.dfy(12,8): Error: declaration 'Class' indicates refining (notation `...`), but does not refine anything
git-issue-1180a.dfy(13,8): Error: declaration 'Trait' indicates refining (notation `...`), but does not refine anything
git-issue-1180a.dfy(11,10): Info: defaulting to 'int' for unspecified base type of 'Newtype'
git-issue-1180a.dfy(19,7): Error: declaration 'Opaque' indicates refining (notation `...`), but does not refine anything
git-issue-1180a.dfy(20,7): Error: declaration 'Opaque'' indicates refining (notation `...`), but does not refine anything
git-issue-1180a.dfy(21,11): Error: declaration 'Datatype' indicates refining (notation `...`), but does not refine anything
git-issue-1180a.dfy(22,13): Error: declaration 'Codatatype' indicates refining (notation `...`), but does not refine anything
git-issue-1180a.dfy(23,10): Error: declaration 'Newtype' indicates refining (notation `...`), but does not refine anything
git-issue-1180a.dfy(24,8): Error: declaration 'Class' indicates refining (notation `...`), but does not refine anything
git-issue-1180a.dfy(25,8): Error: declaration 'Trait' indicates refining (notation `...`), but does not refine anything
git-issue-1180a.dfy(23,10): Info: defaulting to 'int' for unspecified base type of 'Newtype'
git-issue-1180a.dfy(37,9): Error: abstract type 'Ty' is declared with a different number of type parameters (2 instead of 1) than the corresponding abstract type in the module it refines
git-issue-1180a.dfy(38,15): Error: function 'F' is declared with a different number of type parameters (1 instead of 0) than the corresponding function in the module it refines
git-issue-1180a.dfy(38,15): Error: the result type of function 'F' (Z) differs from the result type of the corresponding function in the module it refines (nat)
git-issue-1180a.dfy(39,13): Error: method 'M' is declared with a different number of type parameters (1 instead of 0) than the corresponding method in the module it refines
git-issue-1180a.dfy(39,35): Error: the type of out-parameter 'r' is different from the type of the same out-parameter in the corresponding method in the module it refines ('Z' instead of 'nat')
git-issue-1180a.dfy(43,13): Error: datatype 'Ty' is declared with a different number of type parameters (0 instead of 1) than the corresponding datatype in the module it refines
git-issue-1180a.dfy(44,15): Error: function 'F' is declared with a different number of type parameters (1 instead of 0) than the corresponding function in the module it refines
git-issue-1180a.dfy(44,15): Error: the result type of function 'F' (Z) differs from the result type of the corresponding function in the module it refines (nat)
git-issue-1180a.dfy(45,13): Error: method 'M' is declared with a different number of type parameters (1 instead of 0) than the corresponding method in the module it refines
git-issue-1180a.dfy(45,35): Error: the type of out-parameter 'r' is different from the type of the same out-parameter in the corresponding method in the module it refines ('Z' instead of 'nat')
git-issue-1180a.dfy[Datatype'](31,12): Error: Duplicate member name: c
git-issue-1180a.dfy[Datatype'](32,15): Error: Duplicate member name: F
git-issue-1180a.dfy[Datatype'](33,13): Error: Duplicate member name: M
git-issue-1180a.dfy(52,15): Error: codatatype 'Ty' is declared with a different number of type parameters (0 instead of 1) than the corresponding codatatype in the module it refines
git-issue-1180a.dfy(53,15): Error: function 'F' is declared with a different number of type parameters (1 instead of 0) than the corresponding function in the module it refines
git-issue-1180a.dfy(53,15): Error: the result type of function 'F' (Z) differs from the result type of the corresponding function in the module it refines (nat)
git-issue-1180a.dfy(54,13): Error: method 'M' is declared with a different number of type parameters (1 instead of 0) than the corresponding method in the module it refines
git-issue-1180a.dfy(54,35): Error: the type of out-parameter 'r' is different from the type of the same out-parameter in the corresponding method in the module it refines ('Z' instead of 'nat')
git-issue-1180a.dfy[Codatatype'](31,12): Error: Duplicate member name: c
git-issue-1180a.dfy[Codatatype'](32,15): Error: Duplicate member name: F
git-issue-1180a.dfy[Codatatype'](33,13): Error: Duplicate member name: M
git-issue-1180a.dfy(61,12): Error: newtype 'Ty' is declared with a different number of type parameters (0 instead of 1) than the corresponding newtype in the module it refines
git-issue-1180a.dfy(62,15): Error: function 'F' is declared with a different number of type parameters (1 instead of 0) than the corresponding function in the module it refines
git-issue-1180a.dfy(62,15): Error: the result type of function 'F' (Z) differs from the result type of the corresponding function in the module it refines (nat)
git-issue-1180a.dfy(63,13): Error: method 'M' is declared with a different number of type parameters (1 instead of 0) than the corresponding method in the module it refines
git-issue-1180a.dfy(63,35): Error: the type of out-parameter 'r' is different from the type of the same out-parameter in the corresponding method in the module it refines ('Z' instead of 'nat')
git-issue-1180a.dfy(67,10): Error: class 'Ty' is declared with a different number of type parameters (0 instead of 1) than the corresponding class in the module it refines
git-issue-1180a.dfy(68,15): Error: function 'F' is declared with a different number of type parameters (1 instead of 0) than the corresponding function in the module it refines
git-issue-1180a.dfy(68,15): Error: the result type of function 'F' (Z) differs from the result type of the corresponding function in the module it refines (nat)
git-issue-1180a.dfy(69,13): Error: method 'M' is declared with a different number of type parameters (1 instead of 0) than the corresponding method in the module it refines
git-issue-1180a.dfy(69,35): Error: the type of out-parameter 'r' is different from the type of the same out-parameter in the corresponding method in the module it refines ('Z' instead of 'nat')
git-issue-1180a.dfy(73,10): Error: trait 'Ty' is declared with a different number of type parameters (0 instead of 1) than the corresponding trait in the module it refines
git-issue-1180a.dfy(74,15): Error: function 'F' is declared with a different number of type parameters (1 instead of 0) than the corresponding function in the module it refines
git-issue-1180a.dfy(74,15): Error: the result type of function 'F' (Z) differs from the result type of the corresponding function in the module it refines (nat)
git-issue-1180a.dfy(75,13): Error: method 'M' is declared with a different number of type parameters (1 instead of 0) than the corresponding method in the module it refines
git-issue-1180a.dfy(75,35): Error: the type of out-parameter 'r' is different from the type of the same out-parameter in the corresponding method in the module it refines ('Z' instead of 'nat')
git-issue-1180a.dfy(79,9): Error: a type synonym (Ty) cannot declare members, so it cannot refine an abstract type with members
git-issue-1180a.dfy(92,9): Error: an abstract type declaration (Ty) in a refining module cannot replace a more specific type declaration in the refinement base
git-issue-1180a.dfy(95,9): Error: an abstract type declaration (Ty) in a refining module cannot replace a more specific type declaration in the refinement base
git-issue-1180a.dfy(102,15): Error: a codatatype declaration (Ty) in a refinement module can only refine a codatatype declaration or replace an abstract type declaration
git-issue-1180a.dfy(105,12): Error: a newtype declaration (Ty) in a refinement module can only refine a newtype declaration or replace an abstract type declaration
git-issue-1180a.dfy(105,12): Info: defaulting to 'int' for unspecified base type of 'Ty'
git-issue-1180a.dfy(108,10): Error: a class declaration (Ty) in a refinement module can only refine a class declaration or replace an abstract type declaration
git-issue-1180a.dfy(111,10): Error: a trait declaration (Ty) in a refinement module can only refine a trait declaration or replace an abstract type declaration
git-issue-1180a.dfy(114,9): Error: a type synonym (Ty) is not allowed to replace a datatype from the refined module (A), even if it denotes the same type
git-issue-1180a.dfy(127,9): Error: an abstract type declaration (Ty) in a refining module cannot replace a more specific type declaration in the refinement base
git-issue-1180a.dfy(130,13): Error: a datatype declaration (Ty) in a refinement module can only refine a datatype declaration or replace an abstract type declaration
git-issue-1180a.dfy(137,12): Error: a newtype declaration (Ty) in a refinement module can only refine a newtype declaration or replace an abstract type declaration
git-issue-1180a.dfy(137,12): Info: defaulting to 'int' for unspecified base type of 'Ty'
git-issue-1180a.dfy(140,10): Error: a class declaration (Ty) in a refinement module can only refine a class declaration or replace an abstract type declaration
git-issue-1180a.dfy(143,10): Error: a trait declaration (Ty) in a refinement module can only refine a trait declaration or replace an abstract type declaration
git-issue-1180a.dfy(146,9): Error: a type synonym (Ty) is not allowed to replace a codatatype from the refined module (A), even if it denotes the same type
git-issue-1180a.dfy(159,9): Error: an abstract type declaration (Ty) in a refining module cannot replace a more specific type declaration in the refinement base
git-issue-1180a.dfy(162,13): Error: a datatype declaration (Ty) in a refinement module can only refine a datatype declaration or replace an abstract type declaration
git-issue-1180a.dfy(165,15): Error: a codatatype declaration (Ty) in a refinement module can only refine a codatatype declaration or replace an abstract type declaration
git-issue-1180a.dfy(169,10): Error: a class declaration (Ty) in a refinement module can only refine a class declaration or replace an abstract type declaration
git-issue-1180a.dfy(172,10): Error: a trait declaration (Ty) in a refinement module can only refine a trait declaration or replace an abstract type declaration
git-issue-1180a.dfy(175,9): Error: a type synonym (Ty) is not allowed to replace a newtype from the refined module (A), even if it denotes the same type
git-issue-1180a.dfy(188,9): Error: an abstract type declaration (Ty) in a refining module cannot replace a more specific type declaration in the refinement base
git-issue-1180a.dfy(191,13): Error: a datatype declaration (Ty) in a refinement module can only refine a datatype declaration or replace an abstract type declaration
git-issue-1180a.dfy(194,15): Error: a codatatype declaration (Ty) in a refinement module can only refine a codatatype declaration or replace an abstract type declaration
git-issue-1180a.dfy(198,12): Error: a newtype declaration (Ty) in a refinement module can only refine a newtype declaration or replace an abstract type declaration
git-issue-1180a.dfy(198,12): Info: defaulting to 'int' for unspecified base type of 'Ty'
git-issue-1180a.dfy(201,10): Error: a trait declaration (Ty) in a refinement module can only refine a trait declaration or replace an abstract type declaration
git-issue-1180a.dfy(204,9): Error: a type synonym (Ty) is not allowed to replace a class from the refined module (A), even if it denotes the same type
git-issue-1180a.dfy(217,9): Error: an abstract type declaration (Ty) in a refining module cannot replace a more specific type declaration in the refinement base
git-issue-1180a.dfy(220,13): Error: a datatype declaration (Ty) in a refinement module can only refine a datatype declaration or replace an abstract type declaration
git-issue-1180a.dfy(223,15): Error: a codatatype declaration (Ty) in a refinement module can only refine a codatatype declaration or replace an abstract type declaration
git-issue-1180a.dfy(227,12): Error: a newtype declaration (Ty) in a refinement module can only refine a newtype declaration or replace an abstract type declaration
git-issue-1180a.dfy(227,12): Info: defaulting to 'int' for unspecified base type of 'Ty'
git-issue-1180a.dfy(230,10): Error: a class declaration (Ty) in a refinement module can only refine a class declaration or replace an abstract type declaration
git-issue-1180a.dfy(233,9): Error: a type synonym (Ty) is not allowed to replace a trait from the refined module (A), even if it denotes the same type
82 resolution/type errors detected in git-issue-1180a.dfy