type Nat < Int;

Int < Rat

op 0 : Nat

op 0 : Rat

forall y : Rat

. (var y : Rat) = (op 0 : Nat) %(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'