--- Day changed Thu Jan 05 2017 | ||

stoopkid | does anyone know why i'm getting this error: http://pastebin.com/ubWjCPZ0 | 05/01 02:07 |
---|---|---|

stoopkid | ah duh | 05/01 02:08 |

stoopkid | V is supposed to represent a subset, but agda doesn't know that heh | 05/01 02:09 |

Taneb | If 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 | _ = False | 05/01 15:53 |

wleslie | that 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 equality | 05/01 16:02 |

{AS} | which would require writing most cases explicitly | 05/01 16:02 |

wleslie | that'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 guess | 05/01 16:04 |

{AS} | Taneb: I think agda-prelude allows you to derive it | 05/01 16:05 |

{AS} | https://github.com/UlfNorell/agda-prelude/blob/aeb717535b4376b65a6a5a1e28d93ac60330831f/src/Tactic/Deriving/Eq.agda | 05/01 16:06 |

Taneb | I'd rather not go behind the standard library if I can help it | 05/01 16:08 |

{AS} | Taneb: unfortunately Agda does not keep track of inequality constraints | 05/01 16:12 |

{AS} | so you have to write all cases explicitly or use some kind of reflection as far as I understand | 05/01 16:12 |

Taneb | :( | 05/01 16:16 |

effectfu1 | Taneb: you can prove that there is an injection from your type into Nat and derive equality from that | 05/01 19:00 |

effectfu1 | Taneb: http://stackoverflow.com/questions/30314720/easy-syntactic-equality-in-idris | 05/01 19:01 |

{AS} | effectfu1: your link even points to a standard library function | 05/01 19:32 |

{AS} | https://agda.github.io/agda-stdlib/Data.Nat.html#760 | 05/01 19:32 |

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