Newest at the top
| 2025-01-14 17:22:50 +0100 | euleritian | (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) |
| 2025-01-14 17:22:37 +0100 | euleritian | (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-01-14 17:21:34 +0100 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2025-01-14 17:21:14 +0100 | Square2 | (~Square4@user/square) (Ping timeout: 248 seconds) |
| 2025-01-14 17:20:45 +0100 | <haskellbridge> | <Bowuigi> The note on erasure is correct tho IIRC |
| 2025-01-14 17:20:26 +0100 | euleritian | (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) |
| 2025-01-14 17:20:16 +0100 | <haskellbridge> | <Bowuigi> kuribas re:dependent-type-forall even from a dependent type viewpoint, foralls are not lambdas, but it unifies type lambdas and term lambdas (both term level constructs) into one |
| 2025-01-14 17:19:46 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-01-14 17:15:12 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 2025-01-14 17:10:07 +0100 | Digit | (~user@user/digit) Digit |
| 2025-01-14 17:04:34 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-14 17:04:16 +0100 | euleritian | (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-01-14 17:00:34 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-14 16:59:24 +0100 | jespada | (~jespada@2800:a4:31:b00:a974:16da:8c45:e3b4) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2025-01-14 16:56:40 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2025-01-14 16:52:41 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-01-14 16:44:32 +0100 | inedia | (~irc@2600:3c00:e000:287::1) dove |
| 2025-01-14 16:41:43 +0100 | <merijn> | I don't really go to more frequent things than NL-FP :p |
| 2025-01-14 16:41:06 +0100 | Digit | (~user@user/digit) (Remote host closed the connection) |
| 2025-01-14 16:41:03 +0100 | <__monty__> | Either way, my info dates back 7-ish years. So I don't have current info. |
| 2025-01-14 16:40:11 +0100 | <__monty__> | [exa]: I think the Leuven HUG kinda stopped meeting? And if people were coming from Gent to Leuven I kinda feel like the answer is no, at least for Flanders. I don't know about the NeLux part of that though, Merijn and tomsmeding might know for NL? |
| 2025-01-14 16:38:14 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-01-14 16:36:26 +0100 | turlando | (~turlando@user/turlando) turlando |
| 2025-01-14 16:35:58 +0100 | alexherbo2 | (~alexherbo@2a02-8440-e501-2041-d1c5-ba5b-2b42-3c3f.rev.sfr.net) (Remote host closed the connection) |
| 2025-01-14 16:35:10 +0100 | turlando | (~turlando@user/turlando) (Quit: No Ping reply in 180 seconds.) |
| 2025-01-14 16:34:24 +0100 | <haskellbridge> | <Morj> Coq can extract programs to multiple languages, including ocaml and haskell. Coq itself is writte in ocaml |
| 2025-01-14 16:34:14 +0100 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-01-14 16:31:25 +0100 | ft | (~ft@p4fc2a354.dip0.t-ipconnect.de) ft |
| 2025-01-14 16:31:21 +0100 | <kuribas> | coq compiles to ocaml, doesn't it? |
| 2025-01-14 16:27:43 +0100 | <kuribas> | Maybe I should find a job in France... |
| 2025-01-14 16:27:36 +0100 | <kuribas> | haskellbridge: They were secretly using coq instead? |
| 2025-01-14 16:25:36 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-14 16:23:20 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) chexum |
| 2025-01-14 16:22:00 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2025-01-14 16:20:11 +0100 | remedan | (~remedan@ip-62-245-108-153.bb.vodafone.cz) remedan |
| 2025-01-14 16:18:23 +0100 | <hellwolf> | It doesn't seem to have been actioned! |
| 2025-01-14 16:17:57 +0100 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2025-01-14 16:17:41 +0100 | remedan | (~remedan@ip-62-245-108-153.bb.vodafone.cz) (Quit: Bye!) |
| 2025-01-14 16:17:26 +0100 | <hellwolf> | https://coq.discourse.group/t/coq-community-survey-2022-results-part-iv-and-itp-paper-announcement… |
| 2025-01-14 16:15:33 +0100 | <[exa]> | oh I see: The Coq team has decided that Coq will be renamed into 'The Rocq Prover'. |
| 2025-01-14 16:15:33 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 2025-01-14 16:14:33 +0100 | <haskellbridge> | <Morj> > Coq got renamedThe website is still coq.inria.fr |
| 2025-01-14 16:13:54 +0100 | <[exa]> | ayay. |
| 2025-01-14 16:13:54 +0100 | <[exa]> | *bIgger |
| 2025-01-14 16:13:54 +0100 | <[exa]> | __monty__: there are any bugger haskell user groups in benelux? are there any links/sites? (I failed googling that) |
| 2025-01-14 16:13:54 +0100 | xdminsy | (~xdminsy@117.147.71.200) (Ping timeout: 272 seconds) |
| 2025-01-14 16:12:32 +0100 | <[exa]> | I read some memes that Coq got renamed, is that true? (didn't really check) |
| 2025-01-14 16:11:56 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.4.2) |
| 2025-01-14 16:11:54 +0100 | <haskellbridge> | <Morj> I was looking for ocaml positions in France recently, and they were all secretly for coq |
| 2025-01-14 16:11:24 +0100 | <hellwolf> | (not from belgium, sorry, just ranting) |