Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] "undefined" can be defined :)

view this post on Zulip Email Gateway (Aug 22 2022 at 18:25):

From: Askar Safin via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
There is no need to introduce "undefined" as "consts/axiomatization" in HOL.HOL. It can be defined. Look here:

definition
undefined :: 'a
where
"undefined = (THE x. True)"

==
Askar Safin
http://vk.com/safinaskar

view this post on Zulip Email Gateway (Aug 22 2022 at 18:26):

From: "Elsa L. Gunter" <egunter@illinois.edu>
Now you know one more thing about undefined than you knew without this
definition.  It is the element to which THE maps %x. True. It is not
always desirable to know this extra fact.

---Elsa

view this post on Zulip Email Gateway (Aug 22 2022 at 18:27):

From: Askar Safin via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>

Now you know one more thing about undefined than you knew without this definition.  It is the element to which THE maps %x. True.   It is not always desirable to know this extra fact.
I agree.

==
Askar Safin
http://vk.com/safinaskar

Last updated: Nov 21 2024 at 12:39 UTC