[00:04:50] *** Joins: e3928a3bc (~bruno@177-177-109-242.user.veloxzone.com.br) [00:07:39] *** Parts: e3928a3bc (~bruno@177-177-109-242.user.veloxzone.com.br) () [07:38:22] *** Joins: JuanDaugherty (~juan@98.4.124.117) [09:54:11] *** Joins: proteus-guy (~proteusgu@180.183.139.174) [09:57:06] e3928a3bc: that's good to know that you read logs, so I can actually answer you asynchronously! about your git question last week, the thing is just that we switched to github recently and nobody in the core team has a lot of experience, so doing things in any fancy way is just a lot of overhead for them [15:42:47] *** Joins: e3928a3bc (~bruno@177-177-109-242.user.veloxzone.com.br) [15:53:05] *** Quits: e3928a3bc (~bruno@177-177-109-242.user.veloxzone.com.br) (Ping timeout: 248 seconds) [15:58:48] *** Joins: e3928a3bc (~bruno@177-177-109-242.user.veloxzone.com.br) [16:06:55] *** Quits: e3928a3bc (~bruno@177-177-109-242.user.veloxzone.com.br) (Quit: Leaving.) [18:16:01] *** Joins: e3928a3bc (~bruno@177-177-109-242.user.veloxzone.com.br) [21:09:47] hey people [21:09:48] I don't seem to be able to specify a dependent type as a start category in the GF shell [21:09:48] anyone can tell how to do it? [21:09:48] an example: [21:09:48] Arithm> gr -number=10 -cat=Less [21:09:48] Category Less should have 2 argument(s), but has been given 0 [21:25:14] hmm [21:25:24] can you show your whole grammar? [21:26:14] looks like you should give the arguments to Less, like -car=Less Foo Bar [21:26:18] cat* [21:36:06] it's the one in section 6.6 from the book [21:36:07] abstract Arithm = { [21:36:07] cat [21:36:07] Nat ; Less Nat Nat ; [21:36:07] fun [21:36:07] Zero : Nat ; [21:36:07] Succ : Nat -> Nat ; [21:36:08] LessZ : (y : Nat) -> Less Zero (Succ y) ; [21:36:08] LessS : (x,y : Nat) -> Less x y -> Less (Succ x) (Succ y) ; [21:36:09] } [21:36:27] ugh, doesn't IRC have multiline messages? [21:42:27] inariksit: it works! [21:43:07] ur supposed to use a pastebin [21:44:53] yay! [21:45:11] I tried cat = Less, it didn't work [21:45:12] I then tried cat=(Less Zero Zero), but it also didn't work [21:45:13] I didn't think it would be able to tokenize things correctly without the parenthesis! [21:46:15] JuanDaugherty: makes sense! but still, too much work for a few lines of code [21:46:44] i am thinking about doing a value version of xchat [21:46:53] *value added [21:47:15] inariksit: my bad, it did work with gr - cat=Even Zero (another grammar) [21:47:16] but not with Arithm> gr -cat=Less Zero Zero [21:47:16] A function type is expected for the expression Zero instead of type Nat [21:49:09] JuanDaugherty: that would be nice! or we could move to Telegram or some other service like it and use this for backwards compatibility (https://github.com/FruitieX/teleirc) [21:54:17] ty for reminding me of the dominance of the small factors [23:07:16] *** Quits: e3928a3bc (~bruno@177-177-109-242.user.veloxzone.com.br) (Quit: Leaving.)