Cannot derive functional induction principle

[BrunoDutertre]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

In the following fragment, the functional induction principle for function conc fails to be constructed..

abbrev Word := List Nat
abbrev Alphabet := Nat

inductive Regex where
  | none: Regex

def inter: Regexp → (Word → Prop) := sorry
def concatenate (a b: Word → Prop) : (Word → Prop) := sorry
def eps: Word → Prop := sorry

def conc (a: Array Regex) (i: Nat): Word → Prop :=
  if h: i < a.size then
    concatenate (inter a[i]) (conc a (i + 1))
  else
    eps

#check conc.induct

I get this error:

Failed to realize constant conc.induct:
  Cannot derive functional induction principle (please report this issue)
  
    Function conc not defined via WellFounded.fix:
      ⋯.fix (fun i a_1 => if h : i < a.size then concatenate (inter a[i]) (a_1 (i + 1) ⋯) else eps) i a✝

Versions

4.11.0 (also lean-nightly at live.lean-lang.org)

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

Thanks for the report! Today is a holiday, but will debug soon after.

[nomeata]

That was my bad and easy to fix (#5619)