Re: [isabelle] undefined & None


Am Mittwoch, den 02.10.2013, 11:26 +0200 schrieb Makarius:
> In 1996, when "undefined" was still called "arbitrary" someone giving a 
> talk about an Isabelle/HOL formalization had it on one of the introductory 
> slides about the logic.  Since the audience was not HOL-istic that started 
> a very long discussion about what it really means, and it was hard to get 
> to the main topic of the talk.

I can confirm this observation from a few weeks ago, when I talked about
a Isabelle formalization of mine to a group that work on the same
proofs, but without a proof assistant. I think I got the idea behind
undefined across, but I’m not sure about that, and it certainly did not
make a good impression on the audience.

I sometimes wish for better support for partially defined things, where
I have the vague idea that when, for example, I write "a ⊔ b" somewhere,
then the compatibility of a and b in their order either comes as an
implicit fact, or an implicit proof obligation. But I’m not even sure
how to detect which of the two I want...


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.