What is the difference between willundefined and arbitrary? Larry On 2 Oct 2008, at 18:44, Tobias Nipkow wrote:
> "undefined" and "default" are used in a specific way. If you do not > want > that functionality (and accidental equalities), "arbitrary" is a good > alternative. > > Tobias > > Florian Haftmann schrieb: >> Some years ago two further constants were introduces into HOL.thy: >> "undefined" and "default". The idea then was to divide the role of >> classical "arbitrary" on two shoulders: "undefined" should be >> unspecified an could be used to fake partiality, whereas "default" >> would >> be overloaded and could be instantiated on arbitrary types, which is >> useful e.g. for proof extraction. Meanwhile the code dealing with >> unspecified case clauses and missing primrec equations etc. has >> already >> switched from "arbitrary" to "undefined". >> >> I would suggest to walk through and drop any remaining occurence of >> "arbitrary" by "undefined". >> >> But perhaps "arbitrary" is too deep-rooted in HOL tradition to just >> get >> rid of it. Any further arguments against? >> >> Florian >> >> >> >> ------------------------------------------------------------------------ >> >> _______________________________________________ >> Isabelle-dev mailing list >> Isabelle-dev at mailbroy.informatik.tu-muenchen.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > _______________________________________________ > Isabelle-dev mailing list > Isabelle-dev at mailbroy.informatik.tu-muenchen.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
