--- Day changed Sun Feb 05 2017 | ||

subttle | Hi, 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 |
---|---|---|

subttle | understand the import/namespace techniques to use it. Thanks. | 05/02 00:58 |

mudri | I need to go to sleep now, but I guess I could answer ^ tomorrow. | 05/02 01:59 |

subttle | no worries | 05/02 02:01 |

lpaste | glguy pasted “agda example for subttle” at http://lpaste.net/352093 | 05/02 03:39 |

subttle | glguy: many thanks!!!! | 05/02 04:58 |

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