e8700894324940d187d0cc6c4c757781a5985b71Corneliu-Claudiu Prodescutype Nat < Int; Int < Rat

b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescuop 0 : Nat

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elknerop 0 : Rat

24ccc96f8343908e3873eb825f31435410539fd8Christian Maederforall y : Rat

24ccc96f8343908e3873eb825f31435410539fd8Christian Maeder. ((fun __=__[Rat] : forall a : Type . a_v-1 * a_v-1 ->? Unit) :

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu Rat * Rat ->? Unit)

b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescu (var y : Rat, op 0 : Nat) :

24ccc96f8343908e3873eb825f31435410539fd8Christian Maeder Unit

24ccc96f8343908e3873eb825f31435410539fd8Christian Maeder %(divide_def2_Rat)%

24ccc96f8343908e3873eb825f31435410539fd8Christian Maeder%% Type Constructors -----------------------------------------------------

b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuInt : Type < Rat

24ccc96f8343908e3873eb825f31435410539fd8Christian MaederLogical : Type := Unit ->? Unit

b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuNat : Type < Int

c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescuPred : Type -> Type := \ a : Type . a_v-1 ->? Unit

24ccc96f8343908e3873eb825f31435410539fd8Christian MaederRat : Type

24ccc96f8343908e3873eb825f31435410539fd8Christian MaederUnit : Type

24ccc96f8343908e3873eb825f31435410539fd8Christian Maeder__*__ : +Type -> +Type -> Type

24ccc96f8343908e3873eb825f31435410539fd8Christian Maeder__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)

24ccc96f8343908e3873eb825f31435410539fd8Christian Maeder__-->?__ : -Type -> +Type -> Type < __->?__

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu__->__ : -Type -> +Type -> Type < __->?__

275f2a1080c2089e14a1455dbbbb3bc992d8e593cmaeder__->?__ : -Type -> +Type -> Type

0f1878dd1437d61ac62f54ff484ee52c87a43604Christian Maeder%% Assumptions -----------------------------------------------------------

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu0 : Rat %(op)%

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu : Nat %(op)%

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu__/\__ : ? Unit * ? Unit ->? Unit %(fun)%

24ccc96f8343908e3873eb825f31435410539fd8Christian Maeder__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%

24ccc96f8343908e3873eb825f31435410539fd8Christian Maeder__=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

24ccc96f8343908e3873eb825f31435410539fd8Christian Maeder__=>__ : ? Unit * ? Unit ->? Unit %(fun)%

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

24ccc96f8343908e3873eb825f31435410539fd8Christian Maeder__\/__ : ? Unit * ? Unit ->? Unit %(fun)%

24ccc96f8343908e3873eb825f31435410539fd8Christian Maeder__if__ : ? Unit * ? Unit ->? Unit %(fun)%

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu__when__else__

24ccc96f8343908e3873eb825f31435410539fd8Christian Maeder : forall a : Type . a_v-1 * ? Unit * a_v-1 ->? a_v-1 %(fun)%

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederbottom : forall a : Type . a_v-1 %(fun)%

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescudef__ : forall a : Type . a_v-1 ->? Unit %(fun)%

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescufalse : Unit %(fun)%

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescunot__ : ? Unit ->? Unit %(fun)%

24ccc96f8343908e3873eb825f31435410539fd8Christian Maedertrue : Unit %(fun)%

24ccc96f8343908e3873eb825f31435410539fd8Christian Maeder�__ : ? Unit ->? Unit %(fun)%

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu%% Sentences -------------------------------------------------------------

275f2a1080c2089e14a1455dbbbb3bc992d8e593cmaeder((fun __=__[Rat] : forall a : Type . a_v-1 * a_v-1 ->? Unit) :

275f2a1080c2089e14a1455dbbbb3bc992d8e593cmaeder Rat * Rat ->? Unit)

275f2a1080c2089e14a1455dbbbb3bc992d8e593cmaeder (var y : Rat, op 0 : Nat) :

275f2a1080c2089e14a1455dbbbb3bc992d8e593cmaeder Unit %(divide_def2_Rat)%

275f2a1080c2089e14a1455dbbbb3bc992d8e593cmaeder%% Diagnostics -----------------------------------------------------------

275f2a1080c2089e14a1455dbbbb3bc992d8e593cmaeder*** Hint 1.17, redeclared type 'Int'

275f2a1080c2089e14a1455dbbbb3bc992d8e593cmaeder*** Hint 6.14, not a class 'Rat'

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu