Logs: liberachat/#haskell
| 2021-06-28 15:54:51 | <c_wraith> | which is what was breaking things with (>>) - it was returning the value returned by the right argument |
| 2021-06-28 15:55:36 | <zava> | so what it does it checks that after those hexDigits there are no other digits anymore |
| 2021-06-28 15:55:53 | <c_wraith> | it checks that it used the entire input string |
| 2021-06-28 15:56:00 | <c_wraith> | so yes |
| 2021-06-28 15:56:07 | <zava> | and since there is g it fails. thanks a lot :) my friend just solved it with -> notFollowedBy alphaNum >> return... |
| 2021-06-28 15:56:36 | → | hololeap joins (hololeap@user/hololeap) |
| 2021-06-28 15:56:36 | <c_wraith> | yeah, if you check the docs for eof, it mentions that it's implemented with notFollowedBy |
| 2021-06-28 15:56:48 | <c_wraith> | https://hackage.haskell.org/package/parsec-3.1.14.0/docs/Text-Parsec.html#v:eof |
| 2021-06-28 15:57:26 | <zava> | ah now it all falls into place |
| 2021-06-28 15:57:33 | × | MQ-17J quits (~MQ-17J@8.21.10.15) (Ping timeout: 258 seconds) |
| 2021-06-28 15:58:00 | × | hololeap quits (hololeap@user/hololeap) (Client Quit) |
| 2021-06-28 15:58:51 | <zava> | thanks again! |
| 2021-06-28 15:59:44 | → | hololeap joins (~hololeap@user/hololeap) |
| 2021-06-28 16:01:28 | maex | is now known as mstruebing |
| 2021-06-28 16:02:16 | × | jumper149 quits (~jumper149@80.240.31.34) (Quit: WeeChat 3.1) |
| 2021-06-28 16:02:35 | × | ubert quits (~Thunderbi@p200300ecdf259d13a4bb62e26735ec02.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 2021-06-28 16:05:19 | → | jneira[m] joins (~jneira@211.red-176-87-26.dynamicip.rima-tde.net) |
| 2021-06-28 16:06:25 | → | eight joins (~eight@user/eight) |
| 2021-06-28 16:08:44 | → | werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 2021-06-28 16:09:26 | → | pavonia joins (~user@user/siracusa) |
| 2021-06-28 16:11:01 | → | warnz joins (~warnz@2600:1700:77c0:5610:eca1:bc9d:4345:931f) |
| 2021-06-28 16:13:21 | × | samhh quits (~samhh@90.252.127.54) (Quit: samhh) |
| 2021-06-28 16:14:16 | × | neurocyte quits (~neurocyte@user/neurocyte) (Read error: Connection reset by peer) |
| 2021-06-28 16:14:50 | → | neurocyte joins (~neurocyte@92.119.8.247) |
| 2021-06-28 16:14:50 | × | neurocyte quits (~neurocyte@92.119.8.247) (Changing host) |
| 2021-06-28 16:14:50 | → | neurocyte joins (~neurocyte@user/neurocyte) |
| 2021-06-28 16:15:24 | → | Guest9 joins (~Guest9@103.250.145.230) |
| 2021-06-28 16:15:32 | × | warnz quits (~warnz@2600:1700:77c0:5610:eca1:bc9d:4345:931f) (Ping timeout: 272 seconds) |
| 2021-06-28 16:19:06 | → | safinaskar joins (~safinaska@109.252.90.89) |
| 2021-06-28 16:19:22 | <safinaskar> | give me some examples of logical frameworks, please |
| 2021-06-28 16:19:32 | × | werneta quits (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Ping timeout: 265 seconds) |
| 2021-06-28 16:19:39 | <safinaskar> | i am already aware of metamath, automath, twelf, isabelle/pure |
| 2021-06-28 16:19:49 | × | jneira[m] quits (~jneira@211.red-176-87-26.dynamicip.rima-tde.net) (Remote host closed the connection) |
| 2021-06-28 16:19:54 | <safinaskar> | and ott-lang |
| 2021-06-28 16:20:43 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:48c3:15b7:84fd:d26e) (Remote host closed the connection) |
| 2021-06-28 16:22:07 | <janus> | safinaskar: did you see this table? https://en.wikipedia.org/wiki/Proof_assistant#System_comparison |
| 2021-06-28 16:22:45 | <janus> | doesn't really focus on the libraries though... |
| 2021-06-28 16:22:59 | <safinaskar> | janus: this is provers, i need logical frameworks |
| 2021-06-28 16:23:11 | <safinaskar> | i. e. systems, where i can describe my own logic |
| 2021-06-28 16:26:37 | <janus> | safinaskar: but you can describe your own logic upon any consistent logical calculus, no? |
| 2021-06-28 16:26:44 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2021-06-28 16:27:19 | <safinaskar> | janus: yes, but i want special features for working with arbitrary logics |
| 2021-06-28 16:27:37 | <safinaskar> | janus: for example, proof search, at least for syntax-directed rules |
| 2021-06-28 16:28:44 | <janus> | proof search, isn't that just another word for "code generation" ? ;) |
| 2021-06-28 16:29:39 | <safinaskar> | possibly |
| 2021-06-28 16:29:57 | <safinaskar> | is there some way to find at least one inhabitant of given GADT? GADTs are essentially logics, for example, this GADT https://paste.debian.net/1202729/ (written in agda, but can be trivially rewritten in haskell) represent implicational logic. is there some tool to search inhabitants of such GADTs? (This would mean proof search for arbitrary |
| 2021-06-28 16:29:58 | <safinaskar> | logics) |
| 2021-06-28 16:30:19 | → | warnz joins (~warnz@2600:1700:77c0:5610:eca1:bc9d:4345:931f) |
| 2021-06-28 16:30:44 | × | haykam1 quits (~haykam@static.100.2.21.65.clients.your-server.de) (Remote host closed the connection) |
| 2021-06-28 16:30:56 | → | haykam1 joins (~haykam@static.100.2.21.65.clients.your-server.de) |
| 2021-06-28 16:31:42 | × | haykam1 quits (~haykam@static.100.2.21.65.clients.your-server.de) (Remote host closed the connection) |
| 2021-06-28 16:31:51 | → | yoctocell joins (~user@h87-96-130-155.cust.a3fiber.se) |
| 2021-06-28 16:31:52 | <dolio> | That is an undecidable problem in general. |
| 2021-06-28 16:33:22 | <safinaskar> | yes, but for syntax-directed logics we can do it |
| 2021-06-28 16:33:40 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 2021-06-28 16:33:41 | → | Tuplanolla joins (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) |
| 2021-06-28 16:33:52 | → | mekeor joins (~user@2001:a61:3430:c01:f86:cca7:c1fe:e2b4) |
| 2021-06-28 16:35:19 | <safinaskar> | is there some article on equivalence of GADTs and logics? |
| 2021-06-28 16:36:15 | <safinaskar> | it seems, i can proof isomorphism of two logics by giving functions for converting between GADTs. is there some article (say, blog) on this? am i really first to notice this? :) |
| 2021-06-28 16:37:38 | × | wei2912 quits (~wei2912@112.199.250.21) (Quit: Lost terminal) |
| 2021-06-28 16:38:41 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 2021-06-28 16:38:42 | × | azeem quits (~azeem@dynamic-adsl-94-34-9-28.clienti.tiscali.it) (Read error: Connection reset by peer) |
| 2021-06-28 16:38:49 | <dolio> | I don't know exactly what you mean, but e.g. the proof search in Twelf is just like a logic programming language. It has ways of proving that a search will terminate, but not all searches will be provably terminating. Likely even some searches that do terminate won't be provably terminating in its system. |
| 2021-06-28 16:38:58 | → | hnOsmium0001 joins (uid453710@id-453710.stonehaven.irccloud.com) |
| 2021-06-28 16:40:58 | → | chomwitt joins (~Pitsikoko@athedsl-16082.home.otenet.gr) |
| 2021-06-28 16:42:45 | <safinaskar> | dolio: thanks, i will look at it |
| 2021-06-28 16:43:17 | × | matsurago quits (~matsurago@p0446064-vcngn.tkyo.nt.ngn.ppp.ocn.ne.jp) (Quit: Leaving) |
| 2021-06-28 16:44:06 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:48c3:15b7:84fd:d26e) |
| 2021-06-28 16:44:19 | × | chris_ quits (~chris@81.96.113.213) (Remote host closed the connection) |
| 2021-06-28 16:45:52 | → | fresheyeball joins (~fresheyeb@c-71-237-105-37.hsd1.co.comcast.net) |
| 2021-06-28 16:48:07 | → | killsushi joins (~killsushi@user/killsushi) |
| 2021-06-28 16:48:46 | × | MidAutumnMoon quits (~MidAutumn@user/midautumnmoon) (Quit: Leaving for a break - theLounge) |
| 2021-06-28 16:49:22 | → | MidAutumnMoon joins (~MidAutumn@user/midautumnmoon) |
| 2021-06-28 16:49:47 | × | DNH quits (~DNH@8.44.0.30) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-06-28 16:49:50 | × | neurocyte quits (~neurocyte@user/neurocyte) (Quit: The Lounge - https://thelounge.chat) |
| 2021-06-28 16:50:51 | → | DNH joins (~DNH@2a09:bac0:67::82c:1e) |
| 2021-06-28 16:53:26 | × | xff0x quits (~xff0x@2001:1a81:537a:a200:78:fec8:4e97:b67d) (Ping timeout: 268 seconds) |
| 2021-06-28 16:53:32 | → | neurocyte joins (~neurocyte@92.119.8.247) |
| 2021-06-28 16:53:32 | × | neurocyte quits (~neurocyte@92.119.8.247) (Changing host) |
| 2021-06-28 16:53:32 | → | neurocyte joins (~neurocyte@user/neurocyte) |
| 2021-06-28 16:54:10 | → | xff0x joins (~xff0x@2001:1a81:537a:a200:e696:8622:74d:d095) |
| 2021-06-28 16:55:34 | → | azeem joins (~azeem@dynamic-adsl-94-34-9-28.clienti.tiscali.it) |
| 2021-06-28 16:55:57 | → | haykam1 joins (~haykam@static.100.2.21.65.clients.your-server.de) |
| 2021-06-28 16:56:17 | × | DNH quits (~DNH@2a09:bac0:67::82c:1e) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-06-28 16:56:18 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 272 seconds) |
| 2021-06-28 16:56:18 | → | son0p joins (~ff@181.136.122.143) |
| 2021-06-28 16:56:31 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-06-28 16:57:28 | → | kayprish joins (~kayprish@46.240.143.86) |
| 2021-06-28 16:59:50 | → | chris_ joins (~chris@81.96.113.213) |
| 2021-06-28 17:02:01 | → | neo joins (~neo3@136.144.35.93) |
| 2021-06-28 17:03:41 | → | DNH joins (~DNH@2a09:bac0:48::82b:7a06) |
| 2021-06-28 17:04:32 | × | chris_ quits (~chris@81.96.113.213) (Ping timeout: 272 seconds) |
| 2021-06-28 17:04:45 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection) |
| 2021-06-28 17:04:58 | × | neo1 quits (~neo3@cpe-292712.ip.primehome.com) (Ping timeout: 265 seconds) |
| 2021-06-28 17:05:40 | → | MQ-17J joins (~MQ-17J@8.21.10.15) |
| 2021-06-28 17:07:04 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 272 seconds) |
| 2021-06-28 17:08:31 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-06-28 17:10:25 | → | chris_ joins (~chris@81.96.113.213) |
| 2021-06-28 17:12:40 | × | dhouthoo quits (~dhouthoo@178-117-36-167.access.telenet.be) (Quit: WeeChat 3.1) |
| 2021-06-28 17:13:24 | × | mastarija quits (~mastarija@31.217.22.187) (Ping timeout: 272 seconds) |
All times are in UTC.