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

--- Day changed Thu Feb 16 2017
wedifyopengl is up and has a working example16/02 01:51
wedifythere i've finished splitting agda-bindings-collection into separate packages. now to learn some more proofs16/02 01:51
wedifyi bought a book called "constructive real analysis". is it any good? i can't wait for it to come in16/02 02:22
comietekhttps://twitter.com/puffnfresh/status/83203759935510528016/02 04:47
comietekThis is cool16/02 04:48
wedifyhow do i do lists of key value pairs where the values might be of different types?16/02 06:45
comietekwedify: dependent pairs16/02 07:10
{AS}comietek: heh :)16/02 08:21
drdoIs there a symbol for ≋ with a line through it?16/02 19:05
drdoAnalogous to ≉ for ≈16/02 19:06
roconnorDoes Agda have a standard inductive family that witnesses the difference between two natural numbers?16/02 19:21
roconnorI don't suppose pigworker hangs out here.16/02 19:22
glguyroconnor: I suppose _≤_ does that16/02 19:22
roconnorI want a symmetric difference16/02 19:23
roconnorsomething isomorphic to {i | (S i) + n = m} + {n = m} + {i | n = (S i) + m}.16/02 19:25
glguyThat's a bit like: total : Total _≤_16/02 19:25
glguyTotal _∼_ = ∀ 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
roconnormaybe.16/02 19:25
roconnorThat or trichotomy.16/02 19:26
glguyOh, and _≤_ might be the wrong one, _≤′_ more directly encodes the difference in its constructors16/02 19:27
roconnorah16/02 19:27
glguy_≤_ hides it away in the base-case constructor16/02 19:27
glguyNeither of these is directly indexed by the actuall difference as a Nat16/02 19:28
glguydata Ordering : Rel ℕ Level.zero where16/02 19:28
glguyThis might be closer to what you wanted16/02 19:29
glguy  less    : ∀ m k → Ordering m (suc (m + k));  equal   : ∀ m   → Ordering m m;  greater : ∀ m k → Ordering (suc (m + k)) m16/02 19:29
roconnoroh that looks good.16/02 21:22

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