I am busy formalising a theorem using a library which introduces an indexed datatype. For simplicity one can think of it to have the form data idx (n : ℕ).

Now I want to create a list of elements over this datatype with the parameter fixed, whose length depends on this parameter. I have simplified the whole problem to the example below:

open import Data.Nat using (ℕ ; _+_ ; suc ; zero) public
open import Data.List.Base using (_∷_ ; [] ; List) public

data idx (n : ℕ) : Set where
  num : ℕ → idx n

exampleA : List (idx 4) -- some random list
exampleA = num 12312 ∷ num 4792384 ∷ []

exampleB : List (idx 4) -- list of the form that I want
exampleB = num 1 ∷ num 2 ∷ num 3 ∷ num 4 ∷ []

rev-list : (m n : ℕ) → List (idx (n + m))
rev-list zero n = []
-- I want to put "m" in the first hole and "suc n" in the second hole,
-- but I get the following errors:
-- first hole:  m !=< suc m of type ℕ
-- second hole: suc (n + ?0) !=< n + suc m of type ℕ
rev-list (suc m) n = num (suc m) ∷ rev-list {!!} {!!} 

rev-list' : (m n : ℕ) → List (idx (n + m))
rev-list' m zero = []
-- I want to put "n" in the hole, but I get the following error:
-- n + suc m !=< suc (n + m) of type ℕ
rev-list' m (suc n) =  num (suc n) ∷ rev-list' (suc m) {!!}

I want to write a function func : (m n : ℕ) → List (idx (n + m)) that returns a list num 1 ∷ num 2 ∷ num 3 ∷ num 4 ∷ ... num (n + m) ∷ [] when called with func 0 (n + m) or maybe func (n + m) 0 – whatever would work – (as in exampleB).

It seems to be simpler to first compute the reverse list, which I try to achieve in rev-list and rev-list'.
However, I get the errors indicated in the code above. I have been struggling with this for hours to no avail. If anybody here could help me, it would be much appreciated 🙂