2021-07-27 00:32:29 <siraben     > remexre: have you tried out coq-hammer?
2021-07-27 00:33:00 <remexre     > briefly
2021-07-27 00:33:04 <siraben     > funnily enough they defined program equivalence that might help me take another look at the Forth semantics https://github.com/lukaszcz/coqhammer/blob/7f7356c2d036115a39922a953e8560389e88d5ce/examples/tutorial/sauto/imp.v#L109
2021-07-27 00:33:07 <remexre     > was pretty nice, but when it failed it went into a hole
2021-07-27 00:33:20 <remexre     > oh huh
2021-07-27 00:33:42 <siraben     > Yeah that usually happens with fire-and-forget tactics
2021-07-27 00:33:52 <siraben     > honestly I'm a big fan of ssreflect in that regard
2021-07-27 00:33:55 <siraben     > you iterate in very small steps
2021-07-27 00:34:12 <remexre     > haven't tried it; does it come up in the later SF volumes?
2021-07-27 00:35:07 <siraben     > Nope. You'll have to read the math-comp book
2021-07-27 00:35:28 <remexre     > rip, ok, I'll keep that in mind
2021-07-27 00:35:40 <siraben     > remexre: https://github.com/math-comp/mcb/suites/3296508723/artifacts/77008637 (latest draft with corrections)
2021-07-27 00:35:54 <siraben     > I can compare and contrast a normal proof with one written with ssreflect, one sec
2021-07-27 00:40:00 <siraben     > remexre: http://ix.io/3ub7
2021-07-27 00:40:21 <remexre     > that sure is notation :P
2021-07-27 00:41:00 <remexre     > I think I need to learn ssreflect before I can parse proofs with it lol
2021-07-27 01:07:51 <dave0       > re maw
2021-07-27 08:44:03 <kathe       > hello. :)
2021-07-27 08:44:15 <kathe       > michael! glad to see you here. :)
2021-07-27 08:58:23 <crc         > good morning
2021-07-27 09:01:51 <kathe       > crc: a very good morning to you. :)
2021-07-27 09:02:02 <kathe       > crc: it's actually evening out here. ;)
2021-07-27 09:08:18 <crc         > 9am here :)
2021-07-27 09:11:03 <kathe       > crc: which forth do you use?
2021-07-27 09:17:57 <crc         > retroforth
2021-07-27 09:18:06 <kathe       > ah, okay.
2021-07-27 09:18:27 <siraben     > his own forth, of course :P
2021-07-27 09:18:43 <kathe       > :D
2021-07-27 09:36:26 <crc         > always best to use one's own tools
2021-07-27 09:51:48 <cbridge     > <Crab01> Howdy
2021-07-27 09:52:04 <eris[m]1    > hallo!
2021-07-27 09:52:21 <cbridge     > <Crab01> How are we doing?
2021-07-27 10:04:13 <crc         > Crab01: I'm having a pretty good day so far
2021-07-27 10:07:51 <cbridge     > <Crab01> Glad to hear it
2021-07-27 10:08:00 <cbridge     > <Crab01> I finally have a day off :)
2021-07-27 10:47:10 <cbridge     > <cmtptr> god damn is there anything more infuriating than having to work with someone exhibiting dunning-kruger
2021-07-27 10:49:33 <tangentstorm> having to work *for* them?
2021-07-27 10:51:26 <cbridge     > <cmtptr> well since i'm working in an area that this guy "owns" and so he has the clout to push back against my fixes for strikingly obvious problems, it's approaching that.  but yeah, when i was an intern i had to work for one, and that was frustrating on another level because i didn't have the experience or confidence to know it at the time
2021-07-27 14:00:11 <cbridge     > <veltas> I thank myself for not having worked with someone like that, so far. (Or maybe I'm the one with dunning-kruger?)
2021-07-27 14:00:32 <cbridge     > <veltas> Hmm I was over-confident with a few things earlier in my career lol
2021-07-27 14:01:31 <cbridge     > <veltas> What does that mean "I thank myself" I mean "I am thankful"
2021-07-27 14:06:17 <cbridge     > <Crab01> I would be thanking myself too
2021-07-27 16:40:29 <cbridge     > -!- ChanServ changed mode/#forth -> +o  mark4
2021-07-27 16:41:42 <cbridge     > <mark4> starting a new contract in austin tx!
2021-07-27 16:41:48 <cbridge     > <mark4> as soon as i can get there :)
2021-07-27 19:21:19 <cbridge     > <cmtptr> i've been known to tank myself from time to time
2021-07-27 23:43:30 <dave0       > maw