[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Instantiating datatypes with subtype of nat (2)



Sorry 'bout the mail-overload (I guess you volunteers have
*plenty* to do besides answer PVS questions), but I see that
my first question (about ambiguous constructors when the
lifted-subtype system springs into action) is similar to Bug #31, 
and my second question is exactly the same as Bug #18, so I'll wait
for solutions - though I still don't know how to coerce
CASES in the correct way.

-- 
+-----------------------------------+-------------------+
+ My brother went to London and all + adridg@sci.kun.nl +
+ I got was this lousy .sig.        +     (Ade)         +