--- Day changed Sun Feb 12 2017 | ||

SuprDewd | I'm looking to implement comparison of arbitrary Agda terms using reflection | 12/02 13:21 |
---|---|---|

SuprDewd | is that possible? perhaps someone has already done this? | 12/02 13:21 |

SuprDewd | I'm going to use that for sorting | 12/02 13:22 |

SuprDewd | don't really care about the exact order, as long as "definitionally equal" expressions are grouped together | 12/02 13:22 |

adamse | SuprDewd: perhaps https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Deriving/Eq.agda | 12/02 13:22 |

SuprDewd | adamse: thanks, this might be a good starting point | 12/02 13:27 |

SuprDewd | https://github.com/SuprDewd/generate-agda-comparators | 12/02 21:59 |

SuprDewd | in case someone will also find this useful | 12/02 21:59 |

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