[Agda] Overloaded constructor trouble

[Ulf Norell]

The nicer way to disambiguate is

inj-suc : {m n : ℕ} → ℕ.suc m ≡ suc n → m ≡ n

inj-suc = {!!}


/ Ulf

On Fri, Aug 28, 2020 at 11:28 AM Peter Thiemann <
thiemann at informatik.uni-freiburg.de> wrote:

> Hi Thorsten,
>
> modules are your friend, again.
>
> module _ where
>   open import Data.Nat (suc)
>   inj-suc : {m n : ℕ} → suc m ≡ suc n → m ≡ n
>   inj-suc = {!!}
>
> or you just open Fin for the definitions where you need it.
>
> -Peter
>
> PS I ran into this issue when using ==-Reasoning and ~=-Reasoning in the
> same module
>
>
> On 28. August 2020 at 11:22:30, Thorsten Altenkirch (
> thorsten.altenkirch at nottingham.ac.uk) wrote:
> > Ok, let’s say I want to show that suc is injective:
> >
> > open import Relation.Binary.PropositionalEquality
> > open import Data.Nat
> >
> > inj-suc : {m n : ℕ} → suc m ≡ suc n → m ≡ n
> > inj-suc = {!!}
> >
> > So far so good but at some point I decide to use Fin as well.
> >
> > open import Relation.Binary.PropositionalEquality
> > open import Data.Nat
> > open import Data.Fin
> >
> > inj-suc : {m n : ℕ} → suc m ≡ suc n → m ≡ n
> > inj-suc = {!!}
> >
> > But now things get yellow ☹ Ok agda cannot infer which suc I want to
> use, even though only
> > one actually works.
> >
> > This is annoying, especially if you are writing a book and are reluctant
> to write
> >
> > inj-suc : {m n : ℕ} → _≡_ {A = ℕ} (suc m) (suc n) → m ≡ n
> > inj-suc = {!!}
> >
> > instead (this is ugly).
> >
> > I have two questions: are there any good workarounds? And is there a way
> to fix it?
> >
> > Cheers,
> > Thorsten
> >
> >
> >
> > This message and any attachment are intended solely for the addressee
> > and may contain confidential information. If you have received this
> > message in error, please contact the sender and delete the email and
> > attachment.
> >
> > Any views or opinions expressed by the author of this email do not
> > necessarily reflect the views of the University of Nottingham. Email
> > communications with the University of Nottingham may be monitored
> > where permitted by law.
> >
> >
> >
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200828/0d4e7990/attachment.html>