c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancetype s, t

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceop snd : s � t -> t

5d801400993c9671010d244646936d8fd435638cChristian Maederprogram snd(x : _var_1, y : _var_2) = (var y : _var_2)

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceprogram snd(x : _var_3, y : _var_4) = (var y : _var_4)

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceprogram snd(x : _var_5, y : _var_6) = (var y : t) : t

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceprogram snd(x : _var_7, y : _var_8) : t = (var y : _var_8)

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceprogram snd(x : _var_9, y : _var_10) : t = (var y : _var_10)

5d801400993c9671010d244646936d8fd435638cChristian Maederprogram snd(x : s, y : t) : t = (var y : t)

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceprogram (x : s, y : s) = (x : s, y : s)

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Manceop a : s

aa0ca44e856c87db27e61687cbb630f270976da1Felix Gabriel Manceprogram b : s = a

5d801400993c9671010d244646936d8fd435638cChristian Maederop b : s

5d801400993c9671010d244646936d8fd435638cChristian Maederprogram b : s = (op a : s)

5d801400993c9671010d244646936d8fd435638cChristian Maederop x : s; y : t

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceop c : t = (op snd : s � t -> t) ((op x : s) : s, (op y : t) : t)

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance%% Type Constructors -----------------------------------------------------

097bc9f18b722812d480df0f5c634d09cbca8e21Felix Gabriel MancePred : Type -> Type := \ a : Type . a ->? Unit

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceUnit : Type := Unit

852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeders : Type

dc8c83e9922e4746c192916565f3522418534f3aFelix Gabriel Mancet : Type

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance%% Assumptions -----------------------------------------------------------

feab1106bbee4f2ea2fd48bca7106dd041e4211dFelix Gabriel Mance__/\__ : Unit � Unit ->? Unit

18ff56829e5e99383ee6106584d55bcbd8ed45e7Felix Gabriel Mance__<=>__ : Unit � Unit ->? Unit

668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance__=__ : forall a : Type . a � a ->? Unit

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder__=>__ : Unit � Unit ->? Unit

668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance__=e=__ : forall a : Type . a � a ->? Unit

863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance__\/__ : Unit � Unit ->? Unit

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancea : s

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceb : s

668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mancec : t = (op snd : s � t -> t) ((op x : s) : s, (op y : t) : t)

668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mancedef__ : forall a : Type . a ->? Unit

668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Manceif__then__else__ : forall a : Type . Unit � a � a ->? a

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancenot__ : Unit ->? Unit

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancesnd : s � t -> t

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancex : s

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancey : t

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance%% Diagnostics -----------------------------------------------------------

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceError (line 14, column 10) no toplevel pattern '(x : s, y : s)'

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceError (line 17, column 9) no toplevel pattern 'b : s'

668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance