Newest at the top
2024-05-13 21:00:46 +0200 | <mauke> | the solution is clearly that not enough information is given to determine an answer |
2024-05-13 21:00:31 +0200 | <tomsmeding> | possibly a confusion of terminology occurred here |
2024-05-13 21:00:27 +0200 | <mauke> | I don't understand the problem |
2024-05-13 21:00:11 +0200 | <tomsmeding> | the author even quotes Gentzen referring to formalisation of mathematical proofs |
2024-05-13 20:59:41 +0200 | <tomsmeding> | being obviously based on the axioms and thus obviously correct is the point, I thought |
2024-05-13 20:59:27 +0200 | <tomsmeding> | monochrom: the case of the paper is a bit weird though, I think; the author argues that natural deduction is not great because it is inefficient, but efficiency is not really the point of natural deduction, is it? |
2024-05-13 20:58:10 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2024-05-13 20:56:24 +0200 | <tomsmeding> | "associativity of ===" is also a funny statement to make to a constructivist |
2024-05-13 20:55:57 +0200 | <tomsmeding> | "what does that even mean" |
2024-05-13 20:55:43 +0200 | <tomsmeding> | I'm not saying the proof is wrong, but the first step took me embarrassingly long to understand |
2024-05-13 20:55:24 +0200 | <tomsmeding> | it is |
2024-05-13 20:55:20 +0200 | <monochrom> | It is a correct conflation in classical logic. |
2024-05-13 20:54:58 +0200 | <tomsmeding> | feels very weird to read that |
2024-05-13 20:54:54 +0200 | <tomsmeding> | that proof on the first page conflates booleans and truth values |
2024-05-13 20:53:26 +0200 | gawen | (~gawen@user/gawen) |
2024-05-13 20:51:40 +0200 | <tomsmeding> | (hey, a dutchman) |
2024-05-13 20:51:17 +0200 | <monochrom> | https://www.cs.utoronto.ca/~trebla/eq-wiltink.pdf shows how to use how xnor aka (==) as a monoid operator to solve a famous logic puzzle. |
2024-05-13 20:51:13 +0200 | <zzz> | mauke: thath's fun |
2024-05-13 20:48:30 +0200 | <lambdabot> | Foldable t => t Bool -> Bool |
2024-05-13 20:48:29 +0200 | <mauke> | :t foldl' (/=) False |
2024-05-13 20:48:29 +0200 | zzz | (~yin@user/zero) |
2024-05-13 20:47:43 +0200 | <lambdabot> | Bits a => a -> a -> a |
2024-05-13 20:47:42 +0200 | <mauke> | :t xor |
2024-05-13 20:47:31 +0200 | <tomsmeding> | s/xor/nonempty/ |
2024-05-13 20:47:15 +0200 | <glguy> | probably xor had it before getting pulled into base |
2024-05-13 20:46:53 +0200 | zzz | (~yin@user/zero) (Ping timeout: 272 seconds) |
2024-05-13 20:46:29 +0200 | gawen | (~gawen@user/gawen) (Quit: cya) |
2024-05-13 20:44:13 +0200 | <ncf> | why the hell do we have xor :: NonEmpty Bool -> Bool but not [Bool] -> Bool |
2024-05-13 20:43:22 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2024-05-13 20:37:55 +0200 | <tomsmeding> | zzz: tip: cabal-plan dot --hide-builtin |
2024-05-13 20:37:45 +0200 | <zzz> | tomsmeding: ty |
2024-05-13 20:37:29 +0200 | <tomsmeding> | cabal-plan dot |
2024-05-13 20:36:01 +0200 | <zzz> | how can i visualize a dependency graph? cabal-plan? |
2024-05-13 20:34:53 +0200 | <cheater> | like 2-3 screens of code |
2024-05-13 20:34:43 +0200 | <cheater> | the examples i'm thinking of are a little more involved than that |
2024-05-13 20:26:40 +0200 | roboguy_ | (~roboguy_@216.147.124.110) (Client Quit) |
2024-05-13 20:26:34 +0200 | roboguy_ | (~roboguy_@216.147.124.110) |
2024-05-13 20:26:28 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
2024-05-13 20:25:34 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Ping timeout: 260 seconds) |
2024-05-13 20:22:12 +0200 | <glguy> | at least for the cases that are simple enough for doctest to load them |
2024-05-13 20:21:58 +0200 | <glguy> | I do support [Leary]'s suggestion of putting the examples in module comments and using doctest to check them, especially for very limited scope examples: here's how to use just this one function/module |
2024-05-13 20:21:13 +0200 | <cheater> | sometimes my own forgetfulness makes me think our memories are just biological cassette tape |
2024-05-13 20:19:06 +0200 | <cheater> | but what if they forget |
2024-05-13 20:18:53 +0200 | <glguy> | if they are, then just think the examples to them :) |
2024-05-13 20:18:28 +0200 | <cheater> | sometimes i wonder |
2024-05-13 20:18:11 +0200 | <glguy> | presumably those devs aren't forming a hivemend or you wouldn't be making examples in the first place |
2024-05-13 20:17:55 +0200 | <cheater> | hmm |
2024-05-13 20:17:47 +0200 | <glguy> | that's fine |
2024-05-13 20:17:39 +0200 | <cheater> | the only other users are the devs of the monorepo |
2024-05-13 20:17:10 +0200 | <glguy> | In the case the example might be useful to the users as it shows what a mess of build-deps they'll need |