--- Day changed Wed Feb 14 2018
nayru25I'm having a problem getting Agda to accept an argument is okay, anyone know how to fix this? http://lpaste.net/61419814314731110414/02 06:04
{AS}nayru25: you have to pattern match on f14/02 08:01
{AS}F g a == F f a is not the same as F g a \== F f a14/02 08:01
{AS}the first one is internal :)14/02 08:01
nayru25{AS}: aha, thank you; that explains what's going on14/02 08:56
nayru25I moved it down into an equation so I could pattern match on the functor records, and put the ≡ proofs into an Sg and it works now14/02 09:00
{AS}nayru25: good to hear :914/02 09:15
{AS}:)*14/02 09:15
nayru25I found out Conor McBride already did this (see here https://github.com/pigworker/CS410-17/, Lec2Done) and now I'm just working out why it works14/02 09:32
nayru25*Lec3Done   -_-14/02 09:32
trikl[m]is it possible to output the quoted version of a term? `debugPrint` accepts  terms, but these get unquoted when  printed. I'd like to see what one of my example terms looks like when quoted14/02 23:06

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