coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] newlines misparsed as space in emacs+proof-general+company-coq
- Date: Fri, 14 Jun 2024 14:18:39 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr1-f53.google.com
- Ironport-data: A9a23:unIUFKPIShoHwqDvrR0Vk8FynXyQoLVcMsEvi/4bfWQNrUog1GEOz TNJXzqDb62IZWqmKIpxbIm19EJS6JXUxoI1HHM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8mk/vgqoPUUIbsIjp2SRJvVBAvgBdin/9RqoNziLBVOSvU0 T/Ji5OZYA/NNwJcaDpOt/rd8U835pwehRtB1rAATaAT1LPhvyJNZH4vDfnZB2f1RIBSAtm7S 47rpF1u1j6xE78FU7tJo56jGqE4aua60Tum1hK6b5Ofbi1q/UTe5EqU2M00Mi+7gx3R9zx4J U4kWZaYEW/FNYWU8AgRvoUx/4iT8sSq9ZeeSUVTv/B/wGXHIkW339pDNXoVAoYYxvxXWjBhp ewXfWVlghCr34pawZq+Q+how9s5dYzlYdhZtXZnwjXUS/0hRPgvQY2QvY4ejGp23JoXW6uFD yYaQWIHgBDoahdPO0wXBZF4leGhgHW5cjxEp3qaoKM25y7YywkZPL3FaYWNJYLTH58I9qqej nPb/zTyL01BCNO8yzC6yCqdv/DAkAquDer+E5Xjq6cy3wzNroAJMzUdUkL+qv2kgGalStdHI goV/DAvpO487iSWosLVWhS5pDubpEdZVYcLVeI97w6Jx+zf5APx6nU4oiBpaY0Y79MZaAUR9 WCCn+/zJWc+n+2FRifInluLlg+aNS8QJG4EQCYLSwoZ/tXuyL3faDqfHr6P94bl3rXI9SHM/ tyckMQpa1wuYSMj0qy6+RXYmWvpqMWSCAEy4QrTUySu6QYRiG+Zi26AuAOzARVoddnxory9U J4sxZH2AAcmU8jlqcB1aL9RdIxFHt7cWNEmvXZhHoM66xOm8GO5cIZb7VlWfRgwYp1cImO3P B+D52u9AaO/2lP6PcebhKrhW6wXIVTITImNug38N4YQMsgsLVXvEN9GPx7BgjmFfLcQfVEXY srCKZn9Ux72+Ixoyz25Q+pV0LkggEgDKZD7FPjGI+Cc+ePGPha9EO9bWHPXN7xRxP3e/G39r Y0EX+PUkEU3bQELSnOImWLlBQtacyZT6FGfg5A/S9Nv1SI6QT97VaKJm+x6E2Gn9owM/tr1E riGchcw4DLCabfvcG1ms1g6MO+1D6Vs52k2JzItNluO0n0uK9TnpqQGepd9OfFt+OV/xLQmB 7MIaueRMMRpEz7nwjU6aYWijYpAcB/wuxmCERD4axcCfrlhZTfzxPnaQiXV+hIjNBGH7fkFn +X41yfwY4YyeAB5PcOHNNOt1wyQuFYeqsJTXmzJAN9ZR2v0+qM3KSar1v4TCOMPICXl2TG1+ Vu3AxAZhO+VuK4z0oDDqp6lpreTMdlVPxRlDUiCyp2pJwz2w3GF/bZQdMqpIRXMSznS6oi5Q Odk39XQEaYgog5RkoxeF71L8/oP1+H3reUH8jU+TWT5UVu7L5hBfFyU1tZrnY9QzOZ7vQCWZ Bq+yuNCM+/UBPK/QU8jHyt7XOGtzvpOpyLz684yK0DE5CNa2rqLfEFRHhuUghxmM7pHH9I58 NglpfIpxVSzujgyPvaCqxJkxWCGA3gDcqcg77UxIovgjCg1wVBjP73YLALL46+0VtYdCXlyf weoh5fDiY9MmWvEUX44TkbW0cRn2J8hhRFtzX05HWqvpObrvPEN4UBuwWwFdTgNlhRj+MBvC 1dvLHxwdPmv/S83pc1tXFKMOgBmBT+f8HPf01EiyW/TFRGpckfvL2QNH/mH025E0mBbfxldp Kq5zkS8WxnUXcjB5AkAcm87lO7CFPta6R/ntP28Ofi8D70WQGbAk7D0Q3glsD7lMNMVqGycg tcy58d2S6nwFRBIkp0BE4PAiIghEkGVFlJNUdRK3f0sD2rDXBqQxDLXCUS6Wv0VFszw6UXiV vBffJNeZS+fihSLgCsQX5MXArlOm/Us2toOV5XrKUMCsJqdtjBZi43RxAevmF4UR8hSruhlJ rPzbz6iFkmitUlQkULJr+hGPTOcSvsAbwvewuu00bsoE7QujeJSSnwxg4CE5yitDAha/hyvr FziYY3SxLdc0ohCpdbnPZhCIASWEunNctq03jq9iPlwSO/eENzvsloVo2b3Pg4NMro2Xc92p Iu3s9X2/R3kue82Wl/Gh5XaNrlt2vTrefsKNMitfX9QshafaZW9/zoC5GGKBphbm/xN5sScZ lWZaenhUfU3Stti1HluRCwGKCkkCoPzdbXFiRKmifaHGjwx8FXgAou81HnLaWp7SHc5C6fmA FWph8f0t8FqkotcITQlWddkOsZcC33+U/IEc9bRi2GpPlOwiAnfhoq4xAsS0hCVOHyqC82g3 InkQCL5fxGMuK3l6tFVnohxnx8PBkZGnugCURMByuFylgyFIjYKHcYFPbUCL6NkoCj4+ZX7R TPKNU8JKyH2WxZaehTdvvXneCqiBdI1B9SoHQxxonuoaBq3Cr3ZUfElvm1l7mxtczTu8PC/J JtMsjfsNxy22ddySfxV+vW/hvx9y+jHwm4Tv3rwiNH2Hw1UFIBiOKaNx+aRfXev/wDxeET3y awdQGlFRASkUxe0H5s7PXFSHx4dsXXkyDBAgeJjBjrAk93z8QGC4KSX1yLPPnkrY8EDJbpIT nTyL4dIy37DwWQd4MPFpPpw6ZKZypu38gySI6rqRAlUlKa1goji0wXuggJXJPwfFMVj/58xW 9ViD7XSxKhIFayJ5ICr9A==
- Ironport-hdrordr: A9a23:YP1gAasRmlye29xbjLd+v7om7skDhtV00zEX/kB9WHVpm6yj/P xGUs516faUskdzZJhOo7q90cW7LE80lqQU3WByB9mftWDd0QOVxepZjLcKtgeQfhEWgdQtsZ uIHZITNDSJNykZse/KpDKjCt4lzZ2u+r2pg+C29QYUcShaL5p79g98B0KiDkFrSE1nCPMCZe Ohz/sCnCC4cXAbKv62HWYIRIH41rr2vaOjWwcPAxNi0wWVkTa0gYSKdSSl4g==
- Ironport-phdr: A9a23:CXOU3Bz11vphV3TXCzLRw1BlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z h2Zvqw8xwaTBc3y0LFttan/i+PaZSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQF cVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHNZwhEnjSwba52I Rm5sAndqNUaipZ+J6gszRfEvnRHd+NKyG1yIl6dgwjy7dqq8p559CRQtfMh98peXqj/Yq81U 79WAik4Pm4s/MHkugXNQgWJ5nsHT2UZiQFIDBTf7BH7RZj+rC33vfdg1SaAPM32Sbc0WSm+7 6puVRTlhjsLOyI//WrKjcN+kb9boAm5pxNh34HUfI+bNP17fqzHfNMaQ3dKUsJeWiFFB4+xa ZYEAegcMuZCt4TyqFsAoxW9CwexGu3g1iRFiWXq0aAgyektDR3K0Q4mEtkTsHrUttL1NKIKX O2p16bIzTTDb+hW2Tjj64jDbwwsofeWUrJ2bMXa1E4iGBnegVWQqIzlJDOV2foOs2SB9eVgU /igi2g6pA1rozivx9ssiobSi4Iaz1DL7yR5wIIvKdKkT057ZMepHZ1NvC6VK4V4WNktQ310u Ckk0L0Gv4a2cSwLxZklyBDSa/2KfpaK7x/tSeudPDR1iXxqdby/iRi/80itxOLyWMS731tHo SVLn9bQu30QyhDe6cyKR/Rj80qnxD2B2QfT6uReLkA1k6rWM4AhzaAqlpUPr0vDGjX6lF/sg 6+ObkUo4vao5Pr9Yrr6uJCcM5V4hRvmMqQ2gsCwHeM4MhIIX2eF/eS80Kfv8lPkT7VXiPA9j 6rXsIjCKMgFuqK0BxVZ34Uj5hqlETuqzskUkWMHIV9Lfh+MkpbkO1XTIPDjEfewnU6snipqx /HHILLsGonBI37em7n7Z7l98VRTyA8rwNBf+Z1UDrYBLer2WkDrtdzYCgY1MgKuw+r6Edl92 IMTVGyVDq+WN6PStlCI5uYxLOWWeIAVvzP9J+Ak5/7ok3A5hUcQcbe10ZYTcny1HfRrL1+Hb Xbyn9sNC2cHswQmQOzvklKCUDpTZ3ioX6I74zE2EJipApzDRoCsm7yB3Dm0Hp5Mam9cDFCDC 3HoeJieV/cNaSKSPsBhnycLVbikUYAh1BWuuBXmxLpgK+rY4isYuon729hv++LTjQ0y9SBzD 8mFzm2BV3t0kX8QRz8qwKB/plRwxUuE0ahhmvBXCdhT5+5SXQohLp7dz+l6C8joVQ7bf9eJT kymQtS8Dj0rQNIx2YxGX0EoENK7yxvHwiDiV7QSjvmAAIE+2qPaxXn4YchnnSXozq4k2nAsQ spUNWClzod5/g7fT9rAmUWYjKanduIV2ifL+CGCzHaBlE5dWQ90F67CWCZMNQPtsd3l6xaaH PeVArM9P14dmKZqS4NPY9zt1xBdQev7fc7ZaCS3knuxAhCBwvWNapDrciMTxnaVE1AKxiYU+ 3vOLg0iHmG5uWuLBTZuFEnvbkCq+O93rn/9T04owCmFakRg0/y+/RtGzeeERaYr16kf8Dwkt y0yGV+829zMDN/VrgBhfb5cbNB76VFO026ftg1hMbSvKqljghgVdAEk91j22UBRDYNN2dMvs GtszAd2LveA10hdcjqDwZ3qErjeK2234wr2LqCLgRfR19GZ/qpJ4/M9w7n6lCeuEEdqs3Bu0 t0PlmCZ+o2PFg0ZF5T4Tkcw8RF+4bDceCg0oY3OhzVqNuGvvznO1shMZqNtwwu8f9pZLKKPF RPjW8wcCc+0LeU2ml+vJhsaNeFW/aQwMouobfyDkKKsOe9hmnqhgwElqMh02EKN7CpxSajB2 Z8Dz7eZ3xeIfzj5hVal9MvwnMEMZD0fGHa+1TmxHJRYNcgQNc4ADWajJdHyx80r3ca8HS4Fs gT5XhVbg5zMG1LadVH20AxO2F5CpHWmnXH91Dloi3QzqaHZ2iXSwuPkfR5BO2hRRWAkg02/R Or8x90cQkWsaBAk0RW/4kOvjaFRpKVkL2TQB05Odi76aWBjTqSYub+LYsoJ45Qt+3YyMqz0c RWBR7jxrgFPmSrpH2pFxD04MTiss5P12R17lG21I3N6rX6fcsZ1j0S6hpSUVbta2TwIQzN9g D/cCw2nPtWnyt6Tko/KruG0U2/JuoR7SSDw1svAsSK64TcvGhijh7WpndahFwEm0Cj93t0sV CPSrR+6bJO5n6i9NOtmeAFvCjqeo4JzEIF/iYs9h9cZ33EcitOU/GYIuWj2ONRfn6n5aTIBS CUKzNjc/AX+kBc7fzTZmsSjDCzbn5ApbsLfACtewi8n6sFWFKqYpKdJmyd4uBvwrA7cZ+R8g iZIzPIv7HAAhORa8AEpzyibHvUTBRwCZX2qx0nOtYrn6vgMNwPNOfCq2UFznM6sFuSHqwBYA jPif4s6WDV35YN5OU7N13v67sflfsPRZJQdrE7x8V+Igu5LJZY2jvdPizBgPDe3tHclyvU7g B8o1JezuoTBKmRx84q2BxdZMnv+YMZZqVSPxe5O292b2YyiBMArEz8LXYDoQPHuGTQbs/ihN geSHxUzr36aHfzUGgrVuyIE5zrfVpusMX+QPnwQy95vEQKcKEJoiwcRRDwmn5Q9G1Pi1In7f Ux+/DxU+k/gp04G1LdzLxemGDS6xk/genIuRZOYNhYT8gxS+xKfL5mF9uwqVyBAos/68UrUe zTdPVgXSzlOABDMBki/bOfyo4ObqK7BWLL4d7yXMNDs4aRfT6vam8zpi9M8uW7KboLVZjFjF 6FphBQFBywoXZSB3W1IEXRfljqRPZHB4k7gvHQm9Ibnt627PWCnrYqXV+kNbZM2oU3w2eHbc LfOzCdhdWQBjsNKnCCXjuhZhBlI0mlvb2X/SOtb83ecEOSI3PcQVkB+CWs7NdMUvfhkj08dZ IiC0IOzjvkh0bY0EwsXDwW/3Jz5I5VbeSflcwqWTEeTaObcfGONmZqmJ/jmD+UX1bQx1VX4r z+fFwWL0i2rsT7vWljvNOhNiHveJxlCoMSndR0rD2H/TdXgYxn9MdltjDRwz6dmznXNfXURN zRxaSYv5vWZ8D9Yj/NjGmdA8mstLO+KnDyc5vXZLZBeuOViAyB9neZXqHogzL4d4CZBTf1z0 Czcy7wm60mhifWKwyF7XQBmrz9KgMeUpxwnN/iCsJZHXnnA8VQG6mDRQxUGqt15C8H+7qBdz t+c8cC7YDxG8t/S4Y4dH52OcJPBYCdna0CwXmOPX25nBXaxOGrShlJQiqSX/3yR9N0hr4T03 YAJQfldXUA0EfUTDgJkGsYDKdF5RGBB8/bTgcgW6H65tBSUSt9du8WNX/iSAO7vJTXfhL9NY RdOwLLkIqwcM4T63wppbVwwz+GoUwLAGMtApCFsdFp+uEJW7H13VXE+wWrgYwKppWAJTLu6w 0VwhQx5buAgsjzr5h1kQziC7Dt1m043l9L/hDmXezOkN6a8U7ZdDC/svlQwOJf2K+6QRQK3l E1gcjzDQuAJ51OPXW9ugQ7Y/5BIHKwFJUWlSBoZxPXSeO9xlFoB8WOowkhI4eaDApxnxlNCT A==
- Ironport-sdr: 666c89a5_w5ypr/l5P5TdmZfpwZirZPXxVQb0iGxwMZ2oxMXx3L842zi iXBZswZeC1aisvTm+iZO8xCmuuqZ4+i+QGAUtew==
When I enter the following in a new file, I get:
Require Import Coq.Strings.String.
Definition foo: string :=
" a
".
Set Printing All.
Compute foo.
(*
= String (Ascii.Ascii false false false false false true false false)
(String (Ascii.Ascii true false false false false true true false)
(String (Ascii.Ascii false false false false false true false false) EmptyString))
: string
*)
The last character of foo is a newline but it is parsed as a space (ascii 32 (0x20)).
However, when I compile it using coqc, or interactive run it in jscoq (https://coq.vercel.app/), I get the correct answer:
=
String
(
Ascii.Ascii false false false false false true false false
)(
String
)(
Ascii.Ascii true false false false false true true false
)(
String
EmptyString
)(
Ascii.Ascii false true false true false false false
false
)false
EmptyString
: string
-- Abhishek
http://www.cs.cornell.edu/~aa755/- [Coq-Club] newlines misparsed as space in emacs+proof-general+company-coq, Abhishek Anand, 06/14/2024
- Re: [Coq-Club] newlines misparsed as space in emacs+proof-general+company-coq, Erik Martin-Dorel, 06/14/2024
Archive powered by MHonArc 2.6.19+.