Logs: liberachat/#haskell
| 2021-08-17 13:37:24 | <__monty__> | That's pretty cool. The second bullet I figured, but the first one is novel. |
| 2021-08-17 13:38:11 | <__monty__> | Still SMT is a lot less general a method. So really, it depends on what you're interested in. |
| 2021-08-17 13:39:57 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 2021-08-17 13:40:55 | <kuribas> | well, a lot of what is tedious in proving programs correct can be solved with SMT. |
| 2021-08-17 13:41:43 | → | jess joins (~jess@libera/staff/jess) |
| 2021-08-17 13:42:59 | → | chomwitt joins (~chomwitt@2a02:587:dc0c:e200:12c3:7bff:fe6d:d374) |
| 2021-08-17 13:43:02 | × | azeem quits (~azeem@dynamic-adsl-94-34-33-6.clienti.tiscali.it) (Read error: Connection reset by peer) |
| 2021-08-17 13:44:02 | × | ubert quits (~Thunderbi@91.141.37.36.wireless.dyn.drei.com) (Ping timeout: 268 seconds) |
| 2021-08-17 13:44:07 | <__monty__> | Sure, model checking is super useful and practical. |
| 2021-08-17 13:44:51 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 2021-08-17 13:45:36 | → | raehik1 joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2021-08-17 13:46:46 | → | amahl joins (~amahl@dsl-jklbng12-54fbca-64.dhcp.inet.fi) |
| 2021-08-17 13:49:50 | → | ubert joins (~Thunderbi@91.141.37.36.wireless.dyn.drei.com) |
| 2021-08-17 13:50:23 | × | Reyu[M] quits (~reyureyuz@matrix.reyuzenfold.com) (Remote host closed the connection) |
| 2021-08-17 13:51:03 | → | Reyu[M] joins (~reyureyuz@matrix.reyuzenfold.com) |
| 2021-08-17 13:53:05 | → | ub joins (~Thunderbi@91.141.37.36.wireless.dyn.drei.com) |
| 2021-08-17 13:54:09 | × | ubert quits (~Thunderbi@91.141.37.36.wireless.dyn.drei.com) (Ping timeout: 248 seconds) |
| 2021-08-17 13:57:32 | × | ub quits (~Thunderbi@91.141.37.36.wireless.dyn.drei.com) (Ping timeout: 245 seconds) |
| 2021-08-17 13:58:58 | → | slack1256 joins (~slack1256@191.126.43.49) |
| 2021-08-17 13:59:07 | <merijn> | __monty__: Countable infinity is still infinite |
| 2021-08-17 13:59:35 | <merijn> | And even in a constructive setting you have at least countable infinity |
| 2021-08-17 13:59:50 | <__monty__> | merijn: Do note the "even less" though. All this proof assistant stuff is from way back when for me. |
| 2021-08-17 14:00:15 | <merijn> | __monty__: I'd think even in a constructive setting you'll quickly hit countable infinity |
| 2021-08-17 14:00:34 | × | ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 244 seconds) |
| 2021-08-17 14:01:02 | <__monty__> | That's what I suspect. But you'll never catch me speaking confidently about math stuffs. |
| 2021-08-17 14:01:30 | <sshine_> | does megaparsec not have 'brackets', 'braces' and 'parens'? |
| 2021-08-17 14:02:37 | <merijn> | sshine_: You want parsers |
| 2021-08-17 14:02:39 | <__monty__> | @hoogle Control.Applicative.Combinators.between |
| 2021-08-17 14:02:39 | <lambdabot> | Control.Applicative.Combinators between :: Applicative m => m open -> m close -> m a -> m a |
| 2021-08-17 14:02:41 | <merijn> | (the package) |
| 2021-08-17 14:02:51 | <merijn> | or the other one |
| 2021-08-17 14:02:53 | <__monty__> | I think the package is parser-combinators? |
| 2021-08-17 14:02:55 | → | ubert joins (~Thunderbi@91.141.56.213.wireless.dyn.drei.com) |
| 2021-08-17 14:02:57 | <merijn> | ah, yeah |
| 2021-08-17 14:03:23 | <merijn> | Should be re-exported from megaparsec, but they didn't explicitly re-export, so the docs don't show up |
| 2021-08-17 14:04:40 | × | jess quits (~jess@libera/staff/jess) () |
| 2021-08-17 14:05:00 | <__monty__> | I was hoping hoogle would list the package tbh. That's the only reason I qualified. |
| 2021-08-17 14:05:14 | <tomsmeding> | hoogle never lists package names except in the web interface |
| 2021-08-17 14:05:17 | <tomsmeding> | this annoys me every single time |
| 2021-08-17 14:05:30 | <sshine_> | ah, that's why. and yes, I did look in parser-combinators by hitting 's' in hackage. |
| 2021-08-17 14:05:31 | <tomsmeding> | what use is searching for a name in a global list of packages if the search result doesn't show the package name |
| 2021-08-17 14:06:03 | <tomsmeding> | luckily there is 'hoogle server' :p |
| 2021-08-17 14:06:22 | <__monty__> | Yeah, it's suboptimal. The other unfortunate part is it only searches stackage : / |
| 2021-08-17 14:06:23 | <sshine_> | the only reference I find is in megaparsec in this comment: https://hackage.haskell.org/package/megaparsec-9.1.0/docs/Text-Megaparsec-Char-Lexer.html#v:symbol |
| 2021-08-17 14:07:14 | <__monty__> | Tbf that reference does show you exactly what you want though? |
| 2021-08-17 14:07:59 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 2021-08-17 14:08:32 | <sshine_> | __monty__, I'd like to know where to import them from. I don't see that anywhere? |
| 2021-08-17 14:08:40 | × | chomwitt quits (~chomwitt@2a02:587:dc0c:e200:12c3:7bff:fe6d:d374) (Ping timeout: 240 seconds) |
| 2021-08-17 14:09:04 | <sshine_> | I think maybe they're not defined because megaparsec tries to be agnostic about parsing whitespace. |
| 2021-08-17 14:09:32 | → | hnOsmium0001 joins (uid453710@id-453710.stonehaven.irccloud.com) |
| 2021-08-17 14:09:41 | → | vgtw joins (~vgtw@c-9164205c.07-348-756d651.bbcust.telenor.se) |
| 2021-08-17 14:10:15 | <__monty__> | You mean the specific ones or "between"? Because yeah, only the latter is defined. |
| 2021-08-17 14:10:23 | <sshine_> | yes, the specific ones. |
| 2021-08-17 14:18:33 | ← | jakalx parts (~jakalx@base.jakalx.net) (Error from remote client) |
| 2021-08-17 14:22:16 | × | oxide quits (~lambda@user/oxide) (Ping timeout: 268 seconds) |
| 2021-08-17 14:23:45 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 2021-08-17 14:24:26 | × | raehik1 quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Quit: WeeChat 3.2) |
| 2021-08-17 14:24:46 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2021-08-17 14:27:43 | → | nate1 joins (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-08-17 14:28:22 | × | benin036932 quits (~benin@106.198.88.152) (Read error: Connection reset by peer) |
| 2021-08-17 14:29:09 | → | slowButPresent joins (~slowButPr@user/slowbutpresent) |
| 2021-08-17 14:29:27 | → | benin036932 joins (~benin@183.82.178.142) |
| 2021-08-17 14:31:16 | → | lambdap joins (~lambdap@static.167.190.119.168.clients.your-server.de) |
| 2021-08-17 14:31:32 | × | gambpang quits (~ian@207.181.230.156) (Ping timeout: 268 seconds) |
| 2021-08-17 14:37:04 | → | drd joins (~drd@2001:b07:a70:9f1f:1562:34de:f50f:77d4) |
| 2021-08-17 14:38:53 | × | haykam quits (~haykam@static.100.2.21.65.clients.your-server.de) (Remote host closed the connection) |
| 2021-08-17 14:39:08 | → | haykam joins (~haykam@static.100.2.21.65.clients.your-server.de) |
| 2021-08-17 14:39:40 | × | lambdap quits (~lambdap@static.167.190.119.168.clients.your-server.de) (Quit: lambdap) |
| 2021-08-17 14:40:01 | → | lambdap joins (~lambdap@static.167.190.119.168.clients.your-server.de) |
| 2021-08-17 14:42:07 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 2021-08-17 14:44:29 | × | ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 244 seconds) |
| 2021-08-17 14:45:42 | × | glassy quits (~glassy@user/glassy) (Quit: Client closed) |
| 2021-08-17 14:47:58 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.2) |
| 2021-08-17 14:48:09 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-08-17 14:49:10 | × | Obo quits (~roberto@185.76.9.42) (Ping timeout: 240 seconds) |
| 2021-08-17 14:51:52 | × | betelgeuse quits (~john2gb@user/john2gb) (Quit: The Lounge - https://thelounge.chat) |
| 2021-08-17 14:53:32 | → | betelgeuse joins (~betelgeus@94-225-47-8.access.telenet.be) |
| 2021-08-17 14:55:12 | → | gambpang joins (~ishipman@207.181.230.156) |
| 2021-08-17 14:55:41 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 2021-08-17 14:56:06 | → | MidAutumnMoon joins (~MidAutumn@user/midautumnmoon) |
| 2021-08-17 14:59:16 | × | slack1256 quits (~slack1256@191.126.43.49) (Ping timeout: 268 seconds) |
| 2021-08-17 14:59:20 | → | slac47615 joins (~slack1256@181.203.101.233) |
| 2021-08-17 15:06:44 | × | img quits (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2021-08-17 15:08:03 | × | Vajb quits (~Vajb@2001:999:252:4e3c:27f9:d93:655e:583) (Read error: Connection reset by peer) |
| 2021-08-17 15:08:12 | → | chomwitt joins (~chomwitt@ppp-94-67-193-240.home.otenet.gr) |
| 2021-08-17 15:08:31 | × | nate1 quits (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 268 seconds) |
| 2021-08-17 15:09:15 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2021-08-17 15:09:20 | → | Vajb joins (~Vajb@hag-jnsbng11-58c3ab-85.dhcp.inet.fi) |
| 2021-08-17 15:09:26 | × | dolio quits (~dolio@130.44.130.54) (Ping timeout: 272 seconds) |
| 2021-08-17 15:09:49 | → | dolio joins (~dolio@130.44.130.54) |
| 2021-08-17 15:10:28 | × | ec quits (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 2021-08-17 15:10:54 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 2021-08-17 15:11:18 | × | chisui quits (~chisui@200116b864e3ed0025ab38eae95cca2d.dip.versatel-1u1.de) (Quit: Client closed) |
| 2021-08-17 15:12:04 | → | shapr joins (~user@pool-100-36-247-68.washdc.fios.verizon.net) |
| 2021-08-17 15:13:40 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 240 seconds) |
| 2021-08-17 15:15:21 | → | img joins (~img@user/img) |
| 2021-08-17 15:15:23 | → | zebrag joins (~chris@user/zebrag) |
| 2021-08-17 15:15:40 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 2021-08-17 15:18:37 | × | fvr quits (uid503686@id-503686.highgate.irccloud.com) (Quit: Connection closed for inactivity) |
| 2021-08-17 15:20:51 | × | Boomerang quits (~Boomerang@xd520f68c.cust.hiper.dk) (Ping timeout: 268 seconds) |
All times are in UTC.