<div dir="ltr">We know that if m≢n : m ≡ n → ⊥, then the ≤′-refl case is impossible, but Agda doesn't know this. However, Agda does know that, in the ≤′-refl case, m ≡ n. So, if you have m≢n, then on the rhs of a clause containing ≤′-refl, you can write something like ⊥-elim (m≢n refl).<br></div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">--<br>Martin Stone Davis<br><div><br>Postal/Residential:<br></div><div style="margin-left:40px"><span>1223 Ferry St</span><span><span><br></span></span></div><div style="margin-left:40px"><span><span>Apt 5<br></span></span></div><div style="margin-left:40px"><span>Eugene, OR 97401</span><br></div>Talk / <span></span>Text / Voicemail: <a href="tel:3106993578" value="+13106993578" target="_blank">(310) 699-3578</a><br>Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a><div><div><div><span></span></div></div></div></div></div><div dir="ltr"><span style="font-size:small">Website: </span><a href="http://martinstonedavis.com/" style="color:rgb(17,85,204);font-size:small" target="_blank">martinstonedavis.com</a></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div>
<br><div class="gmail_quote">On Mon, Feb 1, 2016 at 7:55 PM, Kenichi Asai <span dir="ltr"><<a href="mailto:asai@is.ocha.ac.jp" target="_blank">asai@is.ocha.ac.jp</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">In the standard library, we have:<br>
<br>
data _≤′_ (m : ℕ) : ℕ → Set where<br>
≤′-refl : m ≤′ m<br>
≤′-step : ∀ {n} (m≤′n : m ≤′ n) → m ≤′ suc n<br>
<br>
Suppose we have a value:<br>
<br>
v : m ≤′ n<br>
<br>
for some m and n. From the definition of the type, we see that there<br>
must be only one choice for v: if m = n, then v must be refl, while if<br>
m < n, then v must be step. (And if m > n, v must be ().)<br>
<br>
Thus, I want to refine v according to m and n. Can I do that? Or in<br>
more general, can I write an inversion function that deconstructs v?<br>
If I case split on v, I always obtain the both possibilities and I<br>
don't see any way to remove the impossible case.<br>
<br>
For "less than" without prime:<br>
<br>
data _≤_ : Rel ℕ Level.zero where<br>
z≤n : ∀ {n} → zero ≤ n<br>
s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n<br>
<br>
we can simply case split on the value of this type, because the type<br>
uniquely and evidently shows which constructor to take. I want to do<br>
the same (or similar) thing for "less than" with prime.<br>
<br>
Sincerely,<br>
<span class="HOEnZb"><font color="#888888"><br>
--<br>
Kenichi Asai<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</font></span></blockquote></div><br></div>