sort 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'