--- Day changed Sat May 20 2017
jonsterlingmietek: I tried to do it a few years back, I don't think I got very far. There's a lot of infrastructure you need to build up (e.g. setoids).20/05 01:53
subttlejonsterling: interesting, what approach did you try, if you don't mind me asking20/05 01:54
jonsterlingsubttle: I can't quite remember, but I think it was something fairly naïve. A think I did it based on cauchy sequences.20/05 01:55
subttlejonsterling: cool!20/05 01:56
acertainkinddoes agda do implicit quantification?20/05 01:56
jonsterlingI didn't get around to proving anything about it. I bet it is easier to work axiomatically with reals in Agda than with concrete ones, but I haven't tried it.20/05 01:56
akr[m]I haven't seen a constructive formalization of reals without axioms (and I'd like to see one)20/05 09:23
akr[m](also see ##dependent)20/05 09:24
shachafjonsterling: Quickly-converging Cauchy sequences?20/05 09:24
mietekjonsterling: aren’t setoids in the stdlib?20/05 11:23
mietekjonsterling, subttle, shachaf: I found a couple papers on approaches equivalent to Cauchy sequences, including coinductive formalisations in Coq: https://users.dimi.uniud.it/~pietro.digianantonio/papers/ — more in ##dependent20/05 11:24
acertainhow often do you need to do implicit abstraction to deal w/ permutation of implicits?20/05 21:42
acertainor how often do you need to insert (\{x} -> a) at all?20/05 21:43
acertainfor reasons other than getting it in scope on top-level definitions20/05 21:44

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