Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 4391 4392 4393 4394 4395 4396 4397 4398 4399 4400 4401 .. 5022
— 502,152 events total
2021-04-13 18:48:27 × rajivr quits (uid269651@gateway/web/irccloud.com/x-zldwlxmsftsxcrzs) (Quit: Connection closed for inactivity)
2021-04-13 18:48:39 × frozenErebus quits (~frozenEre@37.231.244.249) (Ping timeout: 265 seconds)
2021-04-13 18:49:17 <monochrom> I don't know how to negate "the King of France is bald" but I know how to negate "every even prime is even", it's "every even prime is not even".
2021-04-13 18:49:50 <monochrom> So perhaps "the King of France is not bald" is just right.
2021-04-13 18:49:52 → ubert joins (~Thunderbi@77.119.128.21.wireless.dyn.drei.com)
2021-04-13 18:50:45 <monochrom> I still don't know what it means. "means". But I'm just an English room.
2021-04-13 18:51:00 <ski> monochrom : well, one interpretation is ⌜∏ q : (∑ p : ℕ. prime(p) ∧ even(p)). even(π(q))⌝ / ⌜(q :) ((p :) ℕ × Prime p × Even p) → Even (π q)⌝, as apparently noticed by Göran Sundholm in 1986. see e.g. <https://ncatlab.org/nlab/show/dependent+type+theoretic+methods+in+natural+language+semantics>
2021-04-13 18:52:06 × zebrag quits (~inkbottle@aaubervilliers-654-1-2-51.w83-200.abo.wanadoo.fr) (Quit: Konversation terminated!)
2021-04-13 18:52:25 → zebrag joins (~inkbottle@aaubervilliers-654-1-2-51.w83-200.abo.wanadoo.fr)
2021-04-13 18:52:36 → wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2021-04-13 18:52:49 × ukari quits (~ukari@unaffiliated/ukari) (Remote host closed the connection)
2021-04-13 18:53:46 → ukari joins (~ukari@unaffiliated/ukari)
2021-04-13 18:53:58 <ski> Chung-chieh Shan and Chris Barker has also talked about stuff related to this, iirc. see e.g. "Donkey anaphora is in-scope binding" in 2008, at <https://homes.sice.indiana.edu/ccshan/>
2021-04-13 18:57:23 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 246 seconds)
2021-04-13 18:58:18 → stef204 joins (~stef204@unaffiliated/stef-204/x-384198)
2021-04-13 18:58:59 × kini quits (~kini@unaffiliated/kini) (Remote host closed the connection)
2021-04-13 18:59:52 × urdh quits (~urdh@unaffiliated/urdh) (Quit: Boom!)
2021-04-13 18:59:57 × geekosaur quits (930099da@rrcs-147-0-153-218.central.biz.rr.com) (Quit: Connection closed)
2021-04-13 19:00:15 → kini joins (~kini@unaffiliated/kini)
2021-04-13 19:01:11 → geekosaur joins (930099da@rrcs-147-0-153-218.central.biz.rr.com)
2021-04-13 19:03:46 × amiri quits (~amiri@cpe-76-91-154-9.socal.res.rr.com) (Remote host closed the connection)
2021-04-13 19:04:59 <dolio> Isn't that the wrong negation of 'every even prime is even'?
2021-04-13 19:05:56 → amiri joins (~amiri@cpe-76-91-154-9.socal.res.rr.com)
2021-04-13 19:06:07 <monochrom> I would hope so. But English native speakers assured me the negation of "all is lost" is "all is not lost".
2021-04-13 19:08:26 <dolio> Yeah, that phrase doesn't work the logical way.
2021-04-13 19:08:38 <koz_> "Not all is lost" makes sense too?
2021-04-13 19:09:39 <monochrom> Both "everyone is not an expert like you" and "not everyone is an expert like you" circulate and have the same meaning.
2021-04-13 19:09:40 <juri_> not all is lost *yet*.
2021-04-13 19:10:27 <koz_> "Everyone is not an expert like you" implies you're unique, but "not everyone is an expert like you" does not, at least to me.
2021-04-13 19:10:44 <monochrom> and which one is actually used in an instance depends on emphasis, mood, and a coin toss.
2021-04-13 19:11:01 × falafel quits (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) (Ping timeout: 252 seconds)
2021-04-13 19:11:04 × geekosaur quits (930099da@rrcs-147-0-153-218.central.biz.rr.com) (Quit: Connection closed)
2021-04-13 19:11:28 <koz_> This.
2021-04-13 19:11:41 × __minoru__shirae quits (~shiraeesh@109.166.56.189) (Ping timeout: 240 seconds)
2021-04-13 19:11:50 → geekosaur joins (930099da@rrcs-147-0-153-218.central.biz.rr.com)
2021-04-13 19:11:57 <dolio> I guess I probably wouldn't say the first one of those, but because I know the logical meaning.
2021-04-13 19:12:02 → __minoru__shirae joins (~shiraeesh@46.34.206.215)
2021-04-13 19:16:47 × graf_blutwurst quits (~user@2001:171b:226e:adc0:c021:f7f7:82b:a023) (Remote host closed the connection)
2021-04-13 19:18:16 × xprl-gjf quits (~gavin@98.154.147.147.dyn.plus.net) (Remote host closed the connection)
2021-04-13 19:18:39 → xprl-gjf joins (~gavin@98.154.147.147.dyn.plus.net)
2021-04-13 19:21:23 → rekahsoft joins (~rekahsoft@52.129.35.150)
2021-04-13 19:23:22 × geekosaur quits (930099da@rrcs-147-0-153-218.central.biz.rr.com) (Quit: Connection closed)
2021-04-13 19:23:47 × Varis quits (~Tadas@unaffiliated/varis) (Remote host closed the connection)
2021-04-13 19:23:54 → bitmapper joins (uid464869@gateway/web/irccloud.com/x-fibjwudbwypqphxb)
2021-04-13 19:24:45 → geekosaur joins (930099da@rrcs-147-0-153-218.central.biz.rr.com)
2021-04-13 19:27:01 × Sgeo quits (~Sgeo@ool-18b98aa4.dyn.optonline.net) (Ping timeout: 260 seconds)
2021-04-13 19:27:12 → Sgeo joins (~Sgeo@ool-18b98aa4.dyn.optonline.net)
2021-04-13 19:30:51 fendor_ is now known as fendor
2021-04-13 19:33:03 → urdh joins (~urdh@unaffiliated/urdh)
2021-04-13 19:33:16 → alexm_ joins (~alexm_@161.8.254.229)
2021-04-13 19:34:41 × raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 240 seconds)
2021-04-13 19:37:28 → kiweun joins (~kiweun@2607:fea8:2a62:9600:f581:26bd:b1f0:2ed5)
2021-04-13 19:37:32 × alexm_ quits (~alexm_@161.8.254.229) (Ping timeout: 240 seconds)
2021-04-13 19:37:41 × __minoru__shirae quits (~shiraeesh@46.34.206.215) (Ping timeout: 240 seconds)
2021-04-13 19:37:52 × haskellstudent quits (~quassel@213-225-6-101.nat.highway.a1.net) (Ping timeout: 240 seconds)
2021-04-13 19:41:16 × darjeeling_ quits (~darjeelin@122.245.120.156) (Ping timeout: 252 seconds)
2021-04-13 19:41:42 → darjeeling_ joins (~darjeelin@122.245.120.156)
2021-04-13 19:41:49 × kiweun quits (~kiweun@2607:fea8:2a62:9600:f581:26bd:b1f0:2ed5) (Ping timeout: 258 seconds)
2021-04-13 19:42:21 × heatsink quits (~heatsink@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
2021-04-13 19:42:56 → awk joins (~mnrmnaugh@unaffiliated/mnrmnaugh)
2021-04-13 19:45:06 → grimpeux joins (~textual@modemcable153.12-178-173.mc.videotron.ca)
2021-04-13 19:45:41 × mnrmnaugh quits (~mnrmnaugh@unaffiliated/mnrmnaugh) (Ping timeout: 240 seconds)
2021-04-13 19:48:14 × Jello_Raptor quits (~Jello_Rap@li641-12.members.linode.com) (Remote host closed the connection)
2021-04-13 19:48:31 → elfets joins (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de)
2021-04-13 19:50:47 × ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection)
2021-04-13 19:51:23 → Lord_of_Life_ joins (~Lord@unaffiliated/lord-of-life/x-0885362)
2021-04-13 19:52:03 × grimpeux quits (~textual@modemcable153.12-178-173.mc.videotron.ca) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2021-04-13 19:52:06 × zebrag quits (~inkbottle@aaubervilliers-654-1-2-51.w83-200.abo.wanadoo.fr) (Quit: Konversation terminated!)
2021-04-13 19:52:25 → zebrag joins (~inkbottle@aaubervilliers-654-1-2-51.w83-200.abo.wanadoo.fr)
2021-04-13 19:53:51 → nut joins (~user@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr)
2021-04-13 19:54:04 × Lord_of_Life quits (~Lord@unaffiliated/lord-of-life/x-0885362) (Ping timeout: 252 seconds)
2021-04-13 19:54:29 Lord_of_Life_ is now known as Lord_of_Life
2021-04-13 19:58:45 → ddellacosta joins (~ddellacos@ool-44c73afa.dyn.optonline.net)
2021-04-13 19:59:49 → grimpeux joins (~textual@modemcable153.12-178-173.mc.videotron.ca)
2021-04-13 20:00:37 × _ht quits (~quassel@82-169-194-8.biz.kpn.net) (Remote host closed the connection)
2021-04-13 20:00:40 × nut quits (~user@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) (Remote host closed the connection)
2021-04-13 20:00:51 × ClaudiusMaximus quits (~claude@unaffiliated/claudiusmaximus) (Quit: ->)
2021-04-13 20:01:04 × Pickchea quits (~private@unaffiliated/pickchea) (Quit: Leaving)
2021-04-13 20:02:25 → santiacq1 joins (~santiacq@r167-60-199-83.dialup.adsl.anteldata.net.uy)
2021-04-13 20:03:21 × shailangsa quits (~shailangs@host86-185-98-61.range86-185.btcentralplus.com) (Ping timeout: 260 seconds)
2021-04-13 20:04:06 × geekosaur quits (930099da@rrcs-147-0-153-218.central.biz.rr.com) (Quit: Connection closed)
2021-04-13 20:05:11 × santiacq quits (~santiacq@r167-60-229-44.dialup.adsl.anteldata.net.uy) (Ping timeout: 240 seconds)
2021-04-13 20:05:12 × petersen quits (~petersen@redhat/juhp) (Ping timeout: 240 seconds)
2021-04-13 20:07:38 → petersen joins (~petersen@redhat/juhp)
2021-04-13 20:07:46 × KeyJoo quits (~KeyJoo@62.176.30.171) (Ping timeout: 268 seconds)
2021-04-13 20:15:00 → falafel joins (~falafel@pool-96-255-70-50.washdc.fios.verizon.net)
2021-04-13 20:15:55 → sedeki joins (~textual@unaffiliated/sedeki)
2021-04-13 20:15:55 × xprl-gjf quits (~gavin@98.154.147.147.dyn.plus.net) (Ping timeout: 252 seconds)
2021-04-13 20:17:23 → haskellstudent joins (~quassel@213-225-6-101.nat.highway.a1.net)
2021-04-13 20:19:48 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2021-04-13 20:20:09 × DavidEichmann quits (~david@47.27.93.209.dyn.plus.net) (Remote host closed the connection)
2021-04-13 20:20:25 → heatsink joins (~heatsink@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
2021-04-13 20:21:23 → wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2021-04-13 20:24:44 → __minoru__shirae joins (~shiraeesh@46.34.206.215)
2021-04-13 20:24:48 × grimpeux quits (~textual@modemcable153.12-178-173.mc.videotron.ca) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2021-04-13 20:26:31 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 260 seconds)
2021-04-13 20:31:58 → grimpeux joins (~textual@modemcable153.12-178-173.mc.videotron.ca)
2021-04-13 20:33:20 awk is now known as mnrmnaugh
2021-04-13 20:34:37 × alx741 quits (~alx741@181.196.68.37) (Ping timeout: 252 seconds)
2021-04-13 20:34:55 × grimpeux quits (~textual@modemcable153.12-178-173.mc.videotron.ca) (Client Quit)
←Prev  Next→
Page 1 .. 4391 4392 4393 4394 4395 4396 4397 4398 4399 4400 4401 .. 5022

All times are in UTC.