I'd say one of the stronger ways to get "undefined" is to add an element to your type representing undefinedness, e.g., make it (/) : real option -> real option -> real option, where NONE represents "undefined". But then you will have a lot of bookkeeping to deal with... I don't suggest this seriously in the case of division -- I would rather suggest accepting the usual treatment of these partial functions as a small price for the benefits of working in a logic of (only) total functions.
On Wed, 20 Feb 2019 at 12:00, Lawrence Paulson <l...@cam.ac.uk> wrote: > None of these attempts make any sense. In HOL and similar systems > (including Isabelle/HOL), it’s *impossible* to arrange for x/0 to be > undefined in any strong sense. Fortunately, it’s consistent and harmless to > put x/0 = 0. > > Larry Paulson > > > > On 20 Feb 2019, at 05:48, hol-info-requ...@lists.sourceforge.net wrote: > > > > I run some experiments so to check if it is violating any fundamental > rule. > > So far it went good. > > > > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info >
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
