sorts Nat < Int;

Int < Rat

op 0 : Nat

op 0 : Rat

forall y : Rat . y = 0; %(divide_def2_Rat)%

%% Type Constructors -----------------------------------------------------

Int : Type < Rat

Nat : Type < Int

Rat : Type

%% Assumptions -----------------------------------------------------------

0

: Rat %(op)%

: Nat %(op)%

%% Variables -------------------------------------------------------------

y : Rat

%% Sentences -------------------------------------------------------------

y = (op 0 : Nat) %(divide_def2_Rat)%

%% Diagnostics -----------------------------------------------------------

### Hint 1.17, redeclared type 'Int'

### Hint 6.14, not a class 'Rat'