/home/laney/.irssi/irclogs/Freenode/#agda.log-20170106

--- Day changed Thu Jan 05 2017
stoopkiddoes anyone know why i'm getting this error: http://pastebin.com/ubWjCPZ005/01 02:07
stoopkidah duh05/01 02:08
stoopkidV is supposed to represent a subset, but agda doesn't know that heh05/01 02:09
TanebIf I have a data type with 8 constructors which each take zero arguments, is there an easier way to prove (built-in) equality is decidable than writing out all 64 cases?05/01 15:44
wleslie_ = False05/01 15:53
wlesliethat is, you only need nine cases.  eight true cases, and one false case, with wildcard arguments.05/01 15:55
{AS}wleslie: I think they are looking for decidable equality05/01 16:02
{AS}which would require writing most cases explicitly05/01 16:02
wlesliethat's a total choice, what's not decidable about it?05/01 16:03
{AS}wleslie: Decidable equality as in (x y : A) -> Dec (x \== y)05/01 16:03
{AS}Taneb: you can use reflection I would guess05/01 16:04
{AS}Taneb: I think agda-prelude allows you to derive it05/01 16:05
{AS}https://github.com/UlfNorell/agda-prelude/blob/aeb717535b4376b65a6a5a1e28d93ac60330831f/src/Tactic/Deriving/Eq.agda05/01 16:06
TanebI'd rather not go behind the standard library if I can help it05/01 16:08
{AS}Taneb: unfortunately Agda does not keep track of inequality constraints05/01 16:12
{AS}so you have to write all cases explicitly or use some kind of reflection as far as I understand05/01 16:12
Taneb:(05/01 16:16
effectfu1Taneb: you can prove that there is an injection from your type into Nat and derive equality from that05/01 19:00
effectfu1Taneb: http://stackoverflow.com/questions/30314720/easy-syntactic-equality-in-idris05/01 19:01
{AS}effectfu1: your link even points to a standard library function05/01 19:32
{AS}https://agda.github.io/agda-stdlib/Data.Nat.html#76005/01 19:32

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