<div dir="ltr">The nicer way to disambiguate is<br><br><p class="MsoNormal" style="margin-left:36pt"><span style="font-size:11pt">inj-suc : {m n :
</span><span style="font-size:11pt;font-family:"Cambria Math",serif">ℕ</span><span style="font-size:11pt">} → </span><span style="font-size:11pt;font-family:"Cambria Math",serif">ℕ</span><span style="font-size:11pt">.suc m ≡ suc n → m ≡ n</span></p>
<p class="MsoNormal" style="margin-left:36pt"><span style="font-size:11pt">inj-suc = {!!}</span></p><p class="MsoNormal" style="margin-left:36pt"><font size="2"><span style="font-family:arial,sans-serif"><span><br></span></span></font></p><p class="MsoNormal" style="margin-left:6.24pt"><span style="font-size:11pt"><font size="2"><span style="font-family:arial,sans-serif">/ Ulf</span></font><br></span></p></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Aug 28, 2020 at 11:28 AM Peter Thiemann <<a href="mailto:thiemann@informatik.uni-freiburg.de">thiemann@informatik.uni-freiburg.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi Thorsten,<br>
<br>
modules are your friend, again.<br>
<br>
module _ where<br>
  open import Data.Nat (suc)<br>
  inj-suc : {m n : ℕ} → suc m ≡ suc n → m ≡ n<br>
  inj-suc = {!!} <br>
<br>
or you just open Fin for the definitions where you need it.<br>
<br>
-Peter<br>
<br>
PS I ran into this issue when using ==-Reasoning and ~=-Reasoning in the same module<br>
<br>
<br>
On 28. August 2020 at 11:22:30, Thorsten Altenkirch (<a href="mailto:thorsten.altenkirch@nottingham.ac.uk" target="_blank">thorsten.altenkirch@nottingham.ac.uk</a>) wrote:<br>
> Ok, let’s say I want to show that suc is injective:<br>
>  <br>
> open import Relation.Binary.PropositionalEquality<br>
> open import Data.Nat<br>
>  <br>
> inj-suc : {m n : ℕ} → suc m ≡ suc n → m ≡ n<br>
> inj-suc = {!!}<br>
>  <br>
> So far so good but at some point I decide to use Fin as well.<br>
>  <br>
> open import Relation.Binary.PropositionalEquality<br>
> open import Data.Nat<br>
> open import Data.Fin<br>
>  <br>
> inj-suc : {m n : ℕ} → suc m ≡ suc n → m ≡ n<br>
> inj-suc = {!!}<br>
>  <br>
> But now things get yellow ☹ Ok agda cannot infer which suc I want to use, even though only  <br>
> one actually works.<br>
>  <br>
> This is annoying, especially if you are writing a book and are reluctant to write<br>
>  <br>
> inj-suc : {m n : ℕ} → _≡_ {A = ℕ} (suc m) (suc n) → m ≡ n<br>
> inj-suc = {!!}<br>
>  <br>
> instead (this is ugly).<br>
>  <br>
> I have two questions: are there any good workarounds? And is there a way to fix it?<br>
>  <br>
> Cheers,<br>
> Thorsten<br>
>  <br>
>  <br>
>  <br>
> This message and any attachment are intended solely for the addressee<br>
> and may contain confidential information. If you have received this<br>
> message in error, please contact the sender and delete the email and<br>
> attachment.<br>
>  <br>
> Any views or opinions expressed by the author of this email do not<br>
> necessarily reflect the views of the University of Nottingham. Email<br>
> communications with the University of Nottingham may be monitored<br>
> where permitted by law.<br>
>  <br>
>  <br>
>  <br>
>  <br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">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>
>  <br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">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>
</blockquote></div>