Logs: liberachat/#haskell
| 2021-08-14 18:59:22 | → | supersven joins (uid501114@charlton.irccloud.com) |
| 2021-08-14 18:59:22 | × | artem quits (uid512590@highgate.irccloud.com) (Ping timeout: 272 seconds) |
| 2021-08-14 18:59:30 | × | bradparker quits (sid262931@id-262931.highgate.irccloud.com) (Ping timeout: 258 seconds) |
| 2021-08-14 18:59:30 | × | gaze___ quits (sid387101@id-387101.brockwell.irccloud.com) (Ping timeout: 258 seconds) |
| 2021-08-14 18:59:38 | <sm> | ah, (+(-1)) works and is in the spirit of the OQ |
| 2021-08-14 18:59:39 | × | parseval quits (sid239098@id-239098.brockwell.irccloud.com) (Ping timeout: 276 seconds) |
| 2021-08-14 18:59:42 | → | christiaanb joins (sid84827@id-84827.tooting.irccloud.com) |
| 2021-08-14 18:59:42 | × | gonz__ quits (sid304396@id-304396.tooting.irccloud.com) (Ping timeout: 245 seconds) |
| 2021-08-14 18:59:44 | → | iphy joins (sid67735@tooting.irccloud.com) |
| 2021-08-14 18:59:48 | → | carter joins (sid14827@brockwell.irccloud.com) |
| 2021-08-14 18:59:49 | → | NemesisD joins (sid24071@tooting.irccloud.com) |
| 2021-08-14 18:59:49 | → | artem joins (uid512590@id-512590.highgate.irccloud.com) |
| 2021-08-14 18:59:52 | → | bw joins (sid2730@user/betawaffle) |
| 2021-08-14 18:59:52 | → | stevenxl joins (uid133530@highgate.irccloud.com) |
| 2021-08-14 18:59:53 | → | feepo joins (sid28508@id-28508.brockwell.irccloud.com) |
| 2021-08-14 18:59:53 | → | S11001001 joins (sid42510@id-42510.charlton.irccloud.com) |
| 2021-08-14 18:59:53 | × | SethTisue__ quits (sid14912@id-14912.charlton.irccloud.com) (Ping timeout: 258 seconds) |
| 2021-08-14 18:59:54 | × | sclv quits (sid39734@haskell/developer/sclv) (Ping timeout: 240 seconds) |
| 2021-08-14 18:59:54 | × | parisienne quits (sid383587@id-383587.brockwell.irccloud.com) (Ping timeout: 240 seconds) |
| 2021-08-14 18:59:54 | × | JSharp quits (sid4580@id-4580.tooting.irccloud.com) (Ping timeout: 240 seconds) |
| 2021-08-14 18:59:56 | → | bradparker joins (sid262931@id-262931.highgate.irccloud.com) |
| 2021-08-14 18:59:58 | × | idnar quits (sid12240@debian/mithrandi) (Ping timeout: 256 seconds) |
| 2021-08-14 18:59:58 | × | grfn quits (sid449115@id-449115.brockwell.irccloud.com) (Ping timeout: 256 seconds) |
| 2021-08-14 18:59:58 | → | totbwf__ joins (sid402332@id-402332.highgate.irccloud.com) |
| 2021-08-14 18:59:58 | → | vito joins (sid1962@user/vito) |
| 2021-08-14 18:59:59 | → | davetapley joins (sid666@highgate.irccloud.com) |
| 2021-08-14 19:00:02 | → | aria joins (sid380617@id-380617.tooting.irccloud.com) |
| 2021-08-14 19:00:02 | → | tapas joins (sid467876@id-467876.charlton.irccloud.com) |
| 2021-08-14 19:00:03 | → | hsiktas joins (sid224847@tooting.irccloud.com) |
| 2021-08-14 19:00:04 | <[exa]> | hololeap: people love to enumFromTo |
| 2021-08-14 19:00:12 | → | aarchi joins (sid486183@highgate.irccloud.com) |
| 2021-08-14 19:00:12 | → | gmc joins (sid58314@id-58314.charlton.irccloud.com) |
| 2021-08-14 19:00:14 | → | alanz joins (sid110616@id-110616.highgate.irccloud.com) |
| 2021-08-14 19:00:18 | × | caasih quits (sid13241@id-13241.charlton.irccloud.com) (Ping timeout: 240 seconds) |
| 2021-08-14 19:00:18 | → | hendi joins (sid489601@id-489601.tooting.irccloud.com) |
| 2021-08-14 19:00:18 | → | nrr joins (sid20938@id-20938.tooting.irccloud.com) |
| 2021-08-14 19:00:22 | <hpc> | hololeap: actually, maybe just start from https://wiki.portal.chalmers.se/agda/Main/GettingStarted |
| 2021-08-14 19:00:23 | → | dsal joins (sid13060@id-13060.tooting.irccloud.com) |
| 2021-08-14 19:00:23 | → | cln joins (sid336875@id-336875.charlton.irccloud.com) |
| 2021-08-14 19:00:24 | → | kaizen joins (sid501599@brockwell.irccloud.com) |
| 2021-08-14 19:00:25 | → | scav joins (sid309693@id-309693.brockwell.irccloud.com) |
| 2021-08-14 19:00:25 | → | angerman joins (sid209936@charlton.irccloud.com) |
| 2021-08-14 19:00:28 | → | truckasaurus joins (sid457088@id-457088.brockwell.irccloud.com) |
| 2021-08-14 19:00:30 | → | mrianbloom joins (sid350277@id-350277.charlton.irccloud.com) |
| 2021-08-14 19:00:32 | → | dpratt_ joins (sid193493@id-193493.brockwell.irccloud.com) |
| 2021-08-14 19:00:32 | → | jonrh joins (sid5185@charlton.irccloud.com) |
| 2021-08-14 19:00:33 | → | b20n joins (sid115913@id-115913.highgate.irccloud.com) |
| 2021-08-14 19:00:33 | → | NiKaN joins (sid385034@id-385034.brockwell.irccloud.com) |
| 2021-08-14 19:00:36 | → | ephemient joins (uid407513@id-407513.tooting.irccloud.com) |
| 2021-08-14 19:00:39 | → | integral joins (sid296274@user/integral) |
| 2021-08-14 19:00:40 | → | gaze___ joins (sid387101@id-387101.brockwell.irccloud.com) |
| 2021-08-14 19:00:42 | × | teehemkay quits (sid14792@id-14792.tooting.irccloud.com) (Ping timeout: 240 seconds) |
| 2021-08-14 19:00:42 | × | rune quits (sid21167@id-21167.charlton.irccloud.com) (Ping timeout: 240 seconds) |
| 2021-08-14 19:00:46 | <hololeap> | hpc: thanks |
| 2021-08-14 19:00:49 | → | fvr joins (uid503686@id-503686.highgate.irccloud.com) |
| 2021-08-14 19:00:50 | → | bjs joins (sid190364@user/bjs) |
| 2021-08-14 19:00:52 | <hpc> | but build your way up to curry-howard, since that's ultimately the principle that makes it work in the first place |
| 2021-08-14 19:00:53 | → | gregberns__ joins (sid315709@id-315709.brockwell.irccloud.com) |
| 2021-08-14 19:01:00 | → | Pent joins (sid313808@id-313808.tooting.irccloud.com) |
| 2021-08-14 19:01:04 | → | Adeon joins (sid418992@id-418992.tooting.irccloud.com) |
| 2021-08-14 19:01:13 | → | astra` joins (sid289983@user/amish) |
| 2021-08-14 19:01:14 | → | parseval joins (sid239098@id-239098.brockwell.irccloud.com) |
| 2021-08-14 19:01:21 | × | T_S_ quits (sid501726@highgate.irccloud.com) (Ping timeout: 248 seconds) |
| 2021-08-14 19:01:35 | → | grfn joins (sid449115@id-449115.brockwell.irccloud.com) |
| 2021-08-14 19:01:37 | → | rune joins (sid21167@id-21167.charlton.irccloud.com) |
| 2021-08-14 19:01:38 | <mikko> | i guess there's no way around the outer parens in (+(-1)) |
| 2021-08-14 19:01:42 | → | T_S_ joins (sid501726@id-501726.highgate.irccloud.com) |
| 2021-08-14 19:01:43 | → | sclv joins (sid39734@haskell/developer/sclv) |
| 2021-08-14 19:01:44 | → | idnar joins (sid12240@debian/mithrandi) |
| 2021-08-14 19:01:45 | → | parisienne joins (sid383587@id-383587.brockwell.irccloud.com) |
| 2021-08-14 19:01:49 | → | SethTisue__ joins (sid14912@id-14912.charlton.irccloud.com) |
| 2021-08-14 19:01:50 | → | JSharp joins (sid4580@id-4580.tooting.irccloud.com) |
| 2021-08-14 19:01:57 | → | caasih joins (sid13241@id-13241.charlton.irccloud.com) |
| 2021-08-14 19:02:02 | → | teehemkay joins (sid14792@id-14792.tooting.irccloud.com) |
| 2021-08-14 19:02:27 | → | gonz__ joins (sid304396@id-304396.tooting.irccloud.com) |
| 2021-08-14 19:02:32 | → | PotatoGim joins (sid99505@tooting.irccloud.com) |
| 2021-08-14 19:02:39 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-08-14 19:02:47 | × | hendursa1 quits (~weechat@user/hendursaga) (Remote host closed the connection) |
| 2021-08-14 19:03:13 | → | hendursa1 joins (~weechat@user/hendursaga) |
| 2021-08-14 19:05:00 | <c_wraith> | :t (-1+) |
| 2021-08-14 19:05:02 | <lambdabot> | Num a => a -> a |
| 2021-08-14 19:05:05 | → | aplainzetakind joins (~johndoe@captainludd.powered.by.lunarbnc.net) |
| 2021-08-14 19:05:09 | <c_wraith> | that's a horrible hack. don't use it. |
| 2021-08-14 19:05:17 | <c_wraith> | :t (subtract 1) |
| 2021-08-14 19:05:18 | <lambdabot> | Num a => a -> a |
| 2021-08-14 19:05:19 | <hpc> | alternatively, use it everywhere |
| 2021-08-14 19:05:22 | <c_wraith> | use that |
| 2021-08-14 19:05:29 | <mikko> | c_wraith: but i love it already >:D |
| 2021-08-14 19:05:44 | <tomsmeding> | hololeap: frame challenge: have you heard of |
| 2021-08-14 19:05:48 | <tomsmeding> | @hackage quickcheck-classes |
| 2021-08-14 19:05:48 | <lambdabot> | https://hackage.haskell.org/package/quickcheck-classes |
| 2021-08-14 19:05:51 | <c_wraith> | note that it's only the same if addition is commutative in your Num instance |
| 2021-08-14 19:05:52 | → | tritlo joins (sid58727@user/tritlo) |
| 2021-08-14 19:06:05 | → | hnOsmium0001 joins (uid453710@id-453710.stonehaven.irccloud.com) |
| 2021-08-14 19:06:05 | → | joel135 joins (sid136450@id-136450.stonehaven.irccloud.com) |
| 2021-08-14 19:06:09 | → | Firedancer joins (sid336191@id-336191.stonehaven.irccloud.com) |
| 2021-08-14 19:06:24 | × | fabfianda quits (~fabfianda@37.183.255.57) (Ping timeout: 258 seconds) |
| 2021-08-14 19:06:33 | → | SanchayanMaity joins (sid478177@id-478177.stonehaven.irccloud.com) |
| 2021-08-14 19:06:35 | → | fabfianda joins (~fabfianda@mob-5-91-116-37.net.vodafone.it) |
| 2021-08-14 19:06:36 | → | jakesyl joins (sid56879@id-56879.stonehaven.irccloud.com) |
All times are in UTC.