[02:57:57] *** Quits: ski (~ski@remote11.chalmers.se) (*.net *.split)
[03:01:53] *** Joins: ski (~ski@remote11.chalmers.se)
[03:29:17] *** Quits: proteus-guy (~proteus-l@cm-58-10-208-180.revip7.asianet.co.th) (Ping timeout: 256 seconds)
[09:28:31] *** Joins: proteus-guy (~proteus-l@ppp-171-96-189-255.revip8.asianet.co.th)
[10:05:23] *** Quits: proteus-guy (~proteus-l@ppp-171-96-189-255.revip8.asianet.co.th) (Ping timeout: 256 seconds)
[17:29:51] <daherb> i translated one of my dependent type toy projects to agda
[17:30:24] <daherb> and then i build something like a gf concrete syntax in agda so that i can translate my types into strings
[17:30:37] <daherb> https://github.com/daherb/mulle-spatial/blob/master/grammar/SpatialAbs.lagda.md