--- Day changed Thu Feb 16 2017 | ||

wedify | opengl is up and has a working example | 16/02 01:51 |
---|---|---|

wedify | there i've finished splitting agda-bindings-collection into separate packages. now to learn some more proofs | 16/02 01:51 |

wedify | i bought a book called "constructive real analysis". is it any good? i can't wait for it to come in | 16/02 02:22 |

comietek | https://twitter.com/puffnfresh/status/832037599355105280 | 16/02 04:47 |

comietek | This is cool | 16/02 04:48 |

wedify | how do i do lists of key value pairs where the values might be of different types? | 16/02 06:45 |

comietek | wedify: dependent pairs | 16/02 07:10 |

{AS} | comietek: heh :) | 16/02 08:21 |

drdo | Is there a symbol for ≋ with a line through it? | 16/02 19:05 |

drdo | Analogous to ≉ for ≈ | 16/02 19:06 |

roconnor | Does Agda have a standard inductive family that witnesses the difference between two natural numbers? | 16/02 19:21 |

roconnor | I don't suppose pigworker hangs out here. | 16/02 19:22 |

glguy | roconnor: I suppose _≤_ does that | 16/02 19:22 |

roconnor | I want a symmetric difference | 16/02 19:23 |

roconnor | something isomorphic to {i | (S i) + n = m} + {n = m} + {i | n = (S i) + m}. | 16/02 19:25 |

glguy | That's a bit like: total : Total _≤_ | 16/02 19:25 |

glguy | Total _∼_ = ∀ x y → (x ∼ y) ⊎ (y ∼ x) | 16/02 19:25 |

glguy | (Just offering this up because it's the best I know in the stdlib) | 16/02 19:25 |

roconnor | maybe. | 16/02 19:25 |

roconnor | That or trichotomy. | 16/02 19:26 |

glguy | Oh, and _≤_ might be the wrong one, _≤′_ more directly encodes the difference in its constructors | 16/02 19:27 |

roconnor | ah | 16/02 19:27 |

glguy | _≤_ hides it away in the base-case constructor | 16/02 19:27 |

glguy | Neither of these is directly indexed by the actuall difference as a Nat | 16/02 19:28 |

glguy | data Ordering : Rel ℕ Level.zero where | 16/02 19:28 |

glguy | This might be closer to what you wanted | 16/02 19:29 |

glguy | less : ∀ m k → Ordering m (suc (m + k)); equal : ∀ m → Ordering m m; greater : ∀ m k → Ordering (suc (m + k)) m | 16/02 19:29 |

roconnor | oh that looks good. | 16/02 21:22 |

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