Agda-stdlib: Duplicate <-wellFounded in Induction.Nat

[oisdk]

When I try to typecheck the file Induction.Nat I get the following error:

/Users/doisinkidney/Developer/agda-stdlib/src/Induction/Nat.agda:13,1-38
Multiple definitions of <-wellFounded. Previous definition at
/Users/doisinkidney/Developer/agda-stdlib/src/Data/Nat/Induction.agda:83,1-14
when scope checking the declaration
  open import Data.Fin.Induction public

It seems like this was introduced in this commit: #1172

[EdNutting]

Induction.Nat is deprecated. You should import Data.Nat.Induction or Data.Fin.Induction separately. The old Induction.Nat module imports both which is evidently causing the conflict but Induction.Nat will be removed in the future.

[oisdk]

Got it! I was compiling it as part of a "generate everything" type thing, but unfortunately I can't use the generate everything scripts in this repo because I'm using github actions.

[EdNutting]

because I'm using github actions

Out of interest, what is it about Github Actions that stops you using the GenerateEverything script?

[oisdk]

It's just that I don't have the dependencies for GenerateEverything.hs installed. Also github actions seems to have weird restrictions about bash scripts so I haven't been able to get the travis/index.sh script to work either.

[MatthewDaggitt]

Hmm it should still type check though. We need to hide the new <-wellFounded for Fin

[oisdk]

Should the travis script not skip the deprecated files then? I think there are probably some other errors in deprecated files, this was just the first one I ran in to.

[umazalakain]

@oisdk https://github.com/agda/agda-stdlib/pull/1261 should solve this