Newest at the top
| 2024-11-07 12:13:11 +0100 | xff0x | (~xff0x@2405:6580:b080:900:759a:e3d6:c0c3:b78a) |
| 2024-11-07 12:11:28 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 272 seconds) |
| 2024-11-07 12:10:02 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3318-5646-f579-461f-1ad7-34d7.rev.sfr.net) (Remote host closed the connection) |
| 2024-11-07 12:05:04 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2024-11-07 12:00:42 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.4.2) |
| 2024-11-07 11:57:35 +0100 | Digit | (~user@user/digit) (Ping timeout: 255 seconds) |
| 2024-11-07 11:57:31 +0100 | Digitteknohippie | (~user@user/digit) Digit |
| 2024-11-07 11:53:24 +0100 | mulk | (~mulk@pd95146e9.dip0.t-ipconnect.de) mulk |
| 2024-11-07 11:53:02 +0100 | mulk | (~mulk@pd95146e9.dip0.t-ipconnect.de) (Quit: ZNC - http://znc.in) |
| 2024-11-07 11:52:06 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-11-07 11:49:56 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 272 seconds) |
| 2024-11-07 11:46:28 +0100 | tomsmeding | doesn't know much about idris |
| 2024-11-07 11:46:17 +0100 | <kuribas> | idris has a proof search algorithm, but it's also fragile. |
| 2024-11-07 11:45:23 +0100 | <tomsmeding> | agda-presburger can do it but it's doubly-exponential so it runs out of memory once you have 8 variables in your formula |
| 2024-11-07 11:44:58 +0100 | <tomsmeding> | and for inequalities, well, you're on your own with the basic lemmas |
| 2024-11-07 11:44:49 +0100 | <tomsmeding> | there is an integer _equality_ solver in agda-stdlib, but you have to explicitly write out the equality that you want it to solve |
| 2024-11-07 11:44:42 +0100 | <kuribas> | ah right :) |
| 2024-11-07 11:43:53 +0100 | <tomsmeding> | and 'omega' is not considered "fancy" in coq world |
| 2024-11-07 11:43:16 +0100 | <tomsmeding> | kuribas: I meant "no automation", but that's indeed not strictly true. 'auto' is useful for constructing simple lambda calculus terms, but it's multiple leagues below e.g. coq's 'omega' which just solves integer arithmetic stuff for you |
| 2024-11-07 11:43:09 +0100 | notzmv | (~daniel@user/notzmv) notzmv |
| 2024-11-07 11:39:42 +0100 | longlongdouble | (~longlongd@2405:201:5c16:135:1989:242:cab1:419a) (Ping timeout: 276 seconds) |
| 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)? |