Newest at the top
| 2024-11-07 11:32:45 +0100 | kritzefitz | (~kritzefit@debian/kritzefitz) kritzefitz |
| 2024-11-07 11:32:16 +0100 | longlongdouble | (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) |
| 2024-11-07 11:29:36 +0100 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2024-11-07 11:28:43 +0100 | longlongdouble | (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) (Remote host closed the connection) |
| 2024-11-07 11:26:27 +0100 | <kuribas> | tomsmeding: did you mean there is no automation, or that "absent" is an automation feature? |
| 2024-11-07 11:24:21 +0100 | xdminsy | (~xdminsy@117.147.71.147) xdminsy |
| 2024-11-07 11:23:00 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-11-07 11:20:39 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 260 seconds) |
| 2024-11-07 11:19:39 +0100 | <kuribas> | tomsmeding: what about this? https://agda.readthedocs.io/en/latest/tools/auto.html |
| 2024-11-07 11:18:04 +0100 | xdminsy | (~xdminsy@117.147.71.147) (Client Quit) |
| 2024-11-07 11:16:59 +0100 | sroso | (~sroso@user/SrOso) SrOso |
| 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) |