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

--- Day changed Sun Feb 05 2017
subttleHi, I have what I hope is an easy/quick question. I'm using the agda-stdlib 0.13 and I need a proof of refl for ℕ's _≤_ relation. Obviously it's easy enough to make one but how can I use the one given in the library? i.e. I'd like to know how to use the one defined here: https://github.com/agda/agda-stdlib/blob/e3893da0ebca8f80ca2919426529b544503d2010/src/Data/Nat.agda#L33 if possible. I'm not sure I 05/02 00:58
subttleunderstand the import/namespace techniques to use it. Thanks.05/02 00:58
mudriI need to go to sleep now, but I guess I could answer ^ tomorrow.05/02 01:59
subttleno worries05/02 02:01
lpasteglguy pasted “agda example for subttle” at http://lpaste.net/35209305/02 03:39
subttleglguy: many thanks!!!!05/02 04:58

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