I do not really understand what is going wrong in the following code (it throws an Uncaught exception Not_found.
). Is this because of the coinductive type? (It's a MWE, but the idea is that the subterm order on finite runs is well-founded, and I aim to use that to define the function by well-founded induction)
From Equations Require Import Equations.
CoInductive run : Set :=
| RunO : run (* base for finite runs *)
| RunS : nat -> run -> run.
Inductive pos : Set :=
| PosO : pos
| PosS : nat -> pos -> pos.
Inductive IsFinRun : run -> Prop :=
| RunO_fin : IsFinRun RunO
| RunS_fin n r : IsFinRun r -> IsFinRun (RunS n r).
Equations run_to_pos (r' : {r : run | IsFinRun r}) : pos :=
run_to_pos (exist _ RunO _) := _ ;
run_to_pos _ := _.
Last updated: Oct 13 2024 at 01:02 UTC