--- Day changed Tue Jul 25 2017
glguyI've been playing with this today and thought someone here might think its interesting. The goal is to work toward the automation of proofs about statements like x ≢ F (G x) where F and G are inductive data constructors25/07 03:50
glguyhttps://glguy.net/ord/Ord.html25/07 03:50
{AS}glguy: I think there was a paper by McBride about this25/07 08:41
{AS}glguy: https://link.springer.com/chapter/10.1007/11617990_1225/07 08:42
{AS}It was recently mentioned in one channel, but I can not remember25/07 08:42
{AS}why or who25/07 08:42
mietek{AS}: nice25/07 09:19
glguy{AS}: Thanks for that reference25/07 15:13

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