[00:11:36] *** Quits: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) (Ping timeout: 250 seconds) [00:24:20] *** Joins: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) [00:53:13] *** Quits: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) (Ping timeout: 258 seconds) [01:06:38] *** Joins: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) [01:36:55] *** Quits: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) (Ping timeout: 258 seconds) [01:50:03] *** Joins: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) [02:03:48] *** Quits: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) (Ping timeout: 245 seconds) [02:03:57] *** Quits: proteus-guy (~proteusgu@node-7ya.pool-180-180.dynamic.totbb.net) (Ping timeout: 240 seconds) [02:16:26] *** Joins: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) [02:16:42] *** Joins: proteus-guy (~proteusgu@node-4qe.pool-101-108.dynamic.totbb.net) [02:34:02] *** Quits: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) (Ping timeout: 258 seconds) [02:47:15] *** Joins: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) [03:38:37] *** Quits: jbalint (~jbalint@unaffiliated/jbalint) (Ping timeout: 244 seconds) [03:56:43] *** Quits: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) (Ping timeout: 245 seconds) [04:02:14] *** Joins: jbalint (~jbalint@24-240-72-190.dhcp.mdsn.wi.charter.com) [04:02:14] *** Quits: jbalint (~jbalint@24-240-72-190.dhcp.mdsn.wi.charter.com) (Changing host) [04:02:14] *** Joins: jbalint (~jbalint@unaffiliated/jbalint) [04:09:14] *** Joins: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) [04:17:26] *** Quits: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) (Ping timeout: 246 seconds) [04:30:00] *** Joins: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) [04:44:36] *** Quits: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) (Ping timeout: 260 seconds) [04:58:08] *** Joins: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) [05:07:55] *** Quits: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) (Ping timeout: 260 seconds) [05:19:37] *** Joins: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) [05:43:24] *** Quits: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) (Ping timeout: 260 seconds) [05:57:37] *** Joins: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) [06:31:32] *** Quits: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) (Ping timeout: 260 seconds) [06:36:24] *** Quits: proteusguy (~proteus-g@183.88.76.112) (Ping timeout: 250 seconds) [06:38:33] *** Quits: JuanDaugherty (~juan@cpe-198-255-197-105.buffalo.res.rr.com) (Quit: Hibernate, reboot, exeunt, etc.) [08:17:52] *** Joins: proteusguy (~proteus-g@183.88.76.112) [08:25:56] *** Quits: proteus-guy (~proteusgu@node-4qe.pool-101-108.dynamic.totbb.net) (Ping timeout: 246 seconds) [08:55:21] *** Joins: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) [09:11:43] *** Quits: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) (Ping timeout: 245 seconds) [09:26:20] *** Joins: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) [09:34:12] *** Quits: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) (Ping timeout: 265 seconds) [09:46:20] *** Joins: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) [09:49:34] *** Joins: fotonzade (~photon@78.189.158.97) [09:56:58] anyone here who has experience of some shadier GF type abuse? [09:57:04] I'm trying to write And : (X : Type) -> X -> X ; [09:57:18] it compiles but says "no normal form of type X" [09:57:34] and I can't use it [09:57:34] CatGram> gr Walk (And ? ?) [09:57:35] Function And is not in scope [09:58:19] *** Quits: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) (Ping timeout: 258 seconds) [09:59:00] if I remove the ": Type) in the first (X : Type), then it, as expected, doesn't compile at all [10:04:40] *** Joins: proteus-guy (~proteusgu@101.108.27.29) [10:09:16] if I change the definition of And into "And : Type -> Type -> Type ;", then it doesn't give the first warning, but then it gives another error [10:09:16] CatGram> gr Walk (And ? ?) [10:09:16] Couldn't match expected type NP against inferred type Type [10:09:17] In the expression: And ?1 ?2 [10:09:30] (this is nothing important, I'm just avoiding grading :-P) [10:11:35] *** Joins: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) [10:19:01] *** Quits: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) (Ping timeout: 258 seconds) [10:33:43] *** Joins: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) [10:52:10] more exciting errors! my current version is And : (X : Type -> S) -> (X -> S) -> (X -> S) ; [10:52:20] and at compile I get warning [10:52:20] Happened in the type of function And [10:52:20] {Type -> S <> Type} [10:52:21] {Type -> S <> Type} [10:52:36] and then [10:52:37] > gr (And Walk Walk) ? [10:52:37] Couldn't match expected type PType against inferred type NP -> S [10:52:38] In the expression: Walk [10:54:45] *** Quits: fotonzade (~photon@78.189.158.97) (Ping timeout: 248 seconds) [11:15:02] *** Quits: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) (Ping timeout: 250 seconds) [11:27:32] *** Joins: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) [11:50:11] *** Quits: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) (Ping timeout: 260 seconds) [12:02:08] *** Joins: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) [12:03:15] *** Quits: proteusguy (~proteus-g@183.88.76.112) (Ping timeout: 260 seconds) [12:06:36] *** Quits: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) (Ping timeout: 250 seconds) [12:51:01] *** Joins: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) [15:45:15] *** Joins: proteusguy (~proteus-g@node-5ct.pool-101-108.dynamic.totbb.net) [17:41:56] *** Quits: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) (Ping timeout: 256 seconds) [18:49:48] *** Joins: fotonzade (~photon@78.189.158.97) [19:44:46] *** Joins: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) [23:11:59] *** Quits: fotonzade (~photon@78.189.158.97) (Ping timeout: 260 seconds) [23:53:52] *** Quits: sirdancealot (~sirdancea@236.152.broadband3.iol.cz) (Remote host closed the connection)