The Coq mailing list

["Lukasz Stafiniak" <l_stafiniak AT hoga.pl>]

Hi List,

Can the following equality be decided?

Inductive typterm : Set->Set :=
   tybool : (typterm bool)
 | tynat : (typterm nat)
 | tyfun : (a, b : Set)(typterm a)->(typterm b)->(typterm (a->b)).

Definition deceq : (a,b:Set)(typterm a)->(typterm b)->
{a==b}+{~a==b}.

Is it anyway true, that ~nat==bool? Do you know any other means to decide
type equality (computationally)?

Thank You, Best Regards,
Lukasz





Uwaga! Do koñca sierpnia przed³u¿yli¶my promocje, do pakietów
wielostanowiskowych dok³adamy PenDrive  Sprawd¼:
http://www.mks.com.pl/promocja-mobile.html