Newest at the top
| 2024-11-07 11:13:38 +0100 | xdminsy | (~xdminsy@117.147.71.147) xdminsy |
| 2024-11-07 11:13:06 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-11-07 11:09:03 +0100 | SlackCoder | (~SlackCode@64-94-63-8.ip.weststar.net.ky) SlackCoder |
| 2024-11-07 11:05:50 +0100 | kritzefitz | (~kritzefit@debian/kritzefitz) (Ping timeout: 255 seconds) |
| 2024-11-07 11:01:48 +0100 | longlongdouble | (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) |
| 2024-11-07 11:00:52 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3318-5646-f579-461f-1ad7-34d7.rev.sfr.net) alexherbo2 |
| 2024-11-07 11:00:32 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3318-5646-f579-461f-1ad7-34d7.rev.sfr.net) (Remote host closed the connection) |
| 2024-11-07 10:58:38 +0100 | comerijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2024-11-07 10:55:40 +0100 | misterfish | (~misterfis@31-161-39-137.biz.kpn.net) misterfish |
| 2024-11-07 10:51:18 +0100 | longlongdouble | (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) (Remote host closed the connection) |
| 2024-11-07 10:49:47 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3318-5646-f579-461f-1ad7-34d7.rev.sfr.net) alexherbo2 |
| 2024-11-07 10:46:37 +0100 | Versality | (~Versality@user/Versality) Versality |
| 2024-11-07 10:46:24 +0100 | Versality | (~Versality@user/Versality) (Remote host closed the connection) |
| 2024-11-07 10:41:11 +0100 | supercode | (~supercode@user/supercode) (Quit: Client closed) |
| 2024-11-07 10:40:30 +0100 | <tomsmeding> | but contrary to Coq, Agda has readable syntax |
| 2024-11-07 10:40:10 +0100 | <tomsmeding> | Coq has fairly good automation, not familiar with HOL; Agda has ~absent automation |
| 2024-11-07 10:38:48 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-11-07 10:37:56 +0100 | <kuribas> | Is it true that dependently typed proof assistants (agda, coq, idris) have worse automation than HOL based (isabella)? |
| 2024-11-07 10:37:26 +0100 | <kuribas> | Which proof assistants have good automation? |
| 2024-11-07 10:32:42 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2024-11-07 10:31:49 +0100 | longlongdouble | (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) |
| 2024-11-07 10:31:37 +0100 | comerijn | (~merijn@77.242.116.146) merijn |
| 2024-11-07 10:28:55 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 2024-11-07 10:21:53 +0100 | misterfish | (~misterfis@h239071.upc-h.chello.nl) (Ping timeout: 248 seconds) |
| 2024-11-07 10:21:15 +0100 | longlongdouble | (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) (Remote host closed the connection) |
| 2024-11-07 10:19:24 +0100 | hgolden_ | (~hgolden@169.150.203.10) (Ping timeout: 252 seconds) |
| 2024-11-07 10:16:49 +0100 | hgolden__ | (~hgolden@146.70.173.229) hgolden |
| 2024-11-07 10:06:05 +0100 | longlongdouble | (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) |
| 2024-11-07 10:05:18 +0100 | longlongdouble | (~longlongd@169.150.196.103) (Ping timeout: 246 seconds) |
| 2024-11-07 10:03:58 +0100 | ubert | (~Thunderbi@77.119.163.56.wireless.dyn.drei.com) ubert |
| 2024-11-07 10:03:31 +0100 | supercode | (~supercode@user/supercode) supercode |
| 2024-11-07 10:01:25 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-11-07 10:00:26 +0100 | longlongdouble | (~longlongd@169.150.196.103) |
| 2024-11-07 09:59:06 +0100 | longlongdouble | (~longlongd@169.150.196.103) (Ping timeout: 272 seconds) |
| 2024-11-07 09:57:57 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2024-11-07 09:56:09 +0100 | petrichor | (~znc-user@user/petrichor) petrichor |
| 2024-11-07 09:54:50 +0100 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) |
| 2024-11-07 09:46:28 +0100 | longlongdouble | (~longlongd@169.150.196.103) |
| 2024-11-07 09:44:55 +0100 | longlongdouble | (~longlongd@169.150.196.103) (Ping timeout: 252 seconds) |
| 2024-11-07 09:44:42 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-11-07 09:43:54 +0100 | turlando | (~turlando@user/turlando) turlando |
| 2024-11-07 09:41:11 +0100 | rvalue- | rvalue |
| 2024-11-07 09:36:17 +0100 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 255 seconds) |
| 2024-11-07 09:36:09 +0100 | euleritian | (~euleritia@77.22.252.56) |
| 2024-11-07 09:35:33 +0100 | euleritian | (~euleritia@dynamic-176-004-249-001.176.4.pool.telefonica.de) (Ping timeout: 248 seconds) |
| 2024-11-07 09:35:20 +0100 | rvalue- | (~rvalue@user/rvalue) rvalue |
| 2024-11-07 09:33:36 +0100 | notzmv | (~daniel@user/notzmv) (Ping timeout: 276 seconds) |
| 2024-11-07 09:31:39 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 276 seconds) |
| 2024-11-07 09:29:19 +0100 | cyphase | (~cyphase@user/cyphase) cyphase |
| 2024-11-07 09:20:42 +0100 | longlongdouble | (~longlongd@169.150.196.103) |