termination proofs with fuel

Stream: lean4

[Vadim Zaliva]

I have a problem with a termination proof in Lean4. I have a group of
mutually recursive functions, using fuel. They are in a mutual block
and each of them has at the end:

termination_by fuel
decreasing_by
  repeat exact Nat.pred_lt_of_ne_zero ‹fuel ≠ 0›

I can see in the IDE that these tactics discharge all termination
goals for each function. However, I am getting the following message
at the mutual:

Cannot derive typecheckExpr._mutual.eq_def
  tactic 'simp' failed, nested error:
  (deterministic) timeout at `simp`, maximum number of heartbeats (200000) has been reached
  Use `set_option maxHeartbeats <num>` to set the limit.

  Additional diagnostic information may be available using the `set_option diagnostics true` command.

PANIC at _private.Lean.Environment.0.Lean.AsyncConsts.add Lean.Environment:443:4: duplicate normalized declaration name typecheckExpr vs. typecheckExpr
backtrace:
/home/lord/.elan/toolchains/leanprover--lean4---v4.20.1/lib/lean/libleanshared.so(lean_panic+0xf5) [0x7200f0f0e0a5]
...

I am a new Lean user and appreciate any advice on how to tackle this.

[Aaron Liu]

Can you provide a #mwe?

[Vadim Zaliva]

I can try to trim it down. I will post one little later.

[Kenny Lau]

Can you define the functions together in one def?

[Vadim Zaliva]

Kenny Lau said:

Can you define the functions together in one def?

Not sure how to do that. I thought you need "mutual" block for mutually recursive functions

[Vadim Zaliva]

Also, my functions are returning Except String monad, if that relevant. (I am reading about partial_fixpoint which I do not fully comprehend yet)

[Vadim Zaliva]

The solution was as simple as set_option maxHeartbeats 400000 :)