--- Log opened Thu Jan 21 00:00:23 2021
07:45 < real_or_random> aj: ah fun, this is an example that I explained just yesterday to someone who has never seen how coq before 
07:45 < real_or_random> the case analysis over the empty type is really elegant
07:46 < real_or_random> i didn't know you work in coq?
08:50 -!- jeremyrubin [~jr@2601:645:c200:14:91a5:d8cb:fe32:d136] has joined #bitmetas
11:01 < aj> real_or_random: i mess around with it and lurk on the irc channel, nothing that counts as work
16:41 -!- Netsplit *.net <-> *.split quits: sipa
17:12 -!- sipa [~pw@gateway/tor-sasl/sipa1024] has joined #bitmetas
17:55 -!- jeremyrubin [~jr@2601:645:c200:14:91a5:d8cb:fe32:d136] has quit [Ping timeout: 264 seconds]
20:09 -!- jeremyrubin [~jr@2601:645:c200:14:91a5:d8cb:fe32:d136] has joined #bitmetas
--- Log closed Fri Jan 22 00:00:23 2021