--- Day changed Tue Jan 31 2017
imodehi, is agda's type system turing complete?31/01 05:11
Caleno.31/01 05:11
CaleOr at least we hope not.31/01 05:11
CaleAgda safety: we last proved false on May 2nd 2015.31/01 05:12
Cale^^31/01 05:12
CaleSometimes it is, but that's an unhappy circumstance31/01 05:12
stoopkidmeaning: agda doesn't accept general recursive functions as proofs31/01 05:12
imodenot asking either of you.31/01 05:12
stoopkidyou'll find that nobody else is gonna give you any different answers31/01 05:13
stoopkidat best they'll just get you closer to an actual encoding of the halting problem in Agda....31/01 05:13
imodeI'll wait for a third party.31/01 05:13
stoopkidfeel free31/01 05:13
stoopkidwhen you get the same answers from everyone here, try ##dependent next31/01 05:14
stoopkidor maybe see what the folks in #coq have to say about it31/01 05:14
imodeagain, I'll wait for a third party.31/01 05:15
Caleimode: https://pdfs.semanticscholar.org/3399/fdf152471b2802c02ed13d6cacc0070de37f.pdf31/01 05:16
imodereading now.31/01 05:16
stoopkidnice link, thanks for finding that31/01 05:17
CaleIt's weird that they use \in rather than :31/01 05:24
mietekPretty sure we proved false a couple times in 201631/01 06:18
mietekWhat’s with the attitude of that guy?31/01 06:19
wlesliethe two times I remember it being proven (within the last year and a bit) include one time where lem had been postulated - which is an unfortunate result, but not proving false in an absolute sense31/01 08:25
wlesliethe other involved constructors that were not really injective due to a size problem31/01 08:25
wlesliebut I suspect that was late 2015ish?31/01 08:26
wleslieAugust?31/01 08:27
tomjackI proved false a month ago using irrelevance: https://github.com/agda/agda/issues/2170#issuecomment-26993144631/01 23:40

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!