--- Day changed Fri Jun 02 2017
byorgeyI remember reading a long time ago a blog post or something showing how to write a verified type checker (for e.g. STLC or something) which returned either a typing derivation or an actual *proof* of untypability, rather than just an error message.02/06 22:20
byorgeybut I can't find it now.  Any pointers appreciated.02/06 22:21
acertainso there's https://github.com/agda/agda/issues/2099 , the problem is sometimes you don't know if you need to insert implicit abstractions until you have the value of some metas02/06 22:31
acertaine.g. in `the ({x : a} (y : b) -> c) (\x -> tm x)`, you can't do `the ? (\y -> tm y)` then fill that hole with the type because it's too late to insert `{x}` as an implicit abstraction02/06 22:32
acertainso how to implement this? the obvious thing i think is like telescope/environment variables to represent parts of the env which might get more entries due to implicit quantification02/06 22:32
Eduard_MunteanuLOL, what's that lorem ipsum there?02/06 22:37
acertain(the details might be wrong in that example)02/06 22:40
acertainuh that example isn't even close to working like i described02/06 23:09
acertainworking example https://github.com/agda/agda/issues/2099#issuecomment-30592236102/06 23:21

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