Re: [isabelle-dev] NEWS: Lexically unsigned numerals for HOL
The situation involving ZF can go either way, as there are hardly any users. How are negative integers written in ZF now? Can one still write #-3 or is it $- #3? The first one. Numerals in ZF are left as they are, *signed*. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Lexically unsigned numerals for HOL
On Sun, 21 Sep 2014, Florian Haftmann wrote: a) Currently, the prefix for (signed!) ZF numerals is »#«. Since operations for integers in ZF are mainly associated with »$« (e.g., »_ $+ _«, »_ $* _«), maybe it would be more consistent to prefer »$« also here. As far as I understand from the sources, ZF numerals are not polymorphic but restricted to set int in ZF. b) The lexical category for signed numerals is named »xnum«. Maybe »signed_num« would be more explicit. The x in xnum can be explained historically as a special marker for something that is a numeral with some extra decoration. The signed vs. unsigned aspect came much later, and was not there in distant past. Looking once again at ZF xnum syntax, I think it can be expressed without the xnum token, and without any syntax change for now -- that may be reconsidered independently. I have presently something that might soon become a changeset to remove the xnum token syntax from Pure. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Lexically unsigned numerals for HOL
On Mon, 22 Sep 2014, Makarius wrote: Looking once again at ZF xnum syntax, I think it can be expressed without the xnum token, and without any syntax change for now -- that may be reconsidered independently. See now: changeset: 58420:37cbbd8eb460 user:wenzelm date:Mon Sep 22 21:28:57 2014 +0200 files: NEWS src/Doc/Isar_Ref/Inner_Syntax.thy src/HOL/Num.thy src/Pure/Syntax/lexicon.ML src/Pure/pure_thy.ML src/ZF/Bin.thy src/ZF/Tools/numeral_syntax.ML description: discontinued old xnum token category; simplified Lexicon.read_num, Lexicon.read_float: no sign here; express ZF numerals via num with mixfix grammar; recovered printing of ZF numerals: one is abbreviation; The last item means that printing of #42 etc. now works again, after many years of being broken by accident. This shows that nobody has used that seriously. Larry can say what # vs. $ is meant to be. With the mixfix grammar around regular num it should be easy to change that -- or leave it unchanged. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Lexically unsigned numerals for HOL
On 21/09/2014 17:04, Florian Haftmann wrote: After realising that HOL and ZF numerals are already separate lexical categories (though the history of this being so ist not clear to me at the moment), I finally took the adventure of turning HOL numerals into unsigned numerals also lexically (logically, this has already been the case for a long time). See now 6d46ad54a2ab. At last I can write n-1 without getting a complaint that n cannot be applied to -1. Hurray, and thanks a lot for that! Tobias Two issues remain left to settle on. a) Currently, the prefix for (signed!) ZF numerals is »#«. Since operations for integers in ZF are mainly associated with »$« (e.g., »_ $+ _«, »_ $* _«), maybe it would be more consistent to prefer »$« also here. As far as I understand from the sources, ZF numerals are not polymorphic but restricted to set int in ZF. b) The lexical category for signed numerals is named »xnum«. Maybe »signed_num« would be more explicit. Awaiting your suggestions and advice, Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
