Hi Chun, Waqar,
"Define" does indeed give priority to earlier clauses. Under the hood
pattern compilation takes place. So what is actually is going on for
> val extreal_add_def = Define`
> (extreal_add (Normal x) (Normal y) = (Normal (x + y))) /\
> (extreal_add PosInf a = PosInf) /\
>
Hi Chun,
I'm not sure about your potential conflict question but we are now using an
improved definition of "extreal_add_def"
val extreal_add_def = Define`
(extreal_add (Normal x) (Normal y) = (Normal (x + y))) /\
(extreal_add (Normal _) a = a) /\
(extreal_add b (Normal _) = b) /\
Hi,the version of “extreal” (extended real numbers) in latest HOL4 has a wrong definition for sum:val _ = Hol_datatype`extreal = NegInf | PosInf | Normal of real`;val extreal_add_def = Define` (extreal_add (Normal x) (Normal y) = (Normal (x + y))) /\ (extreal_add PosInf a = PosInf) /\
