[Agda] Overloaded constructor trouble

[Peter Thiemann]

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
>