Stream: Equations devs & users

Topic: Equations fails with coinductive types?


view this post on Zulip Meven Lennon-Bertrand (Jun 24 2024 at 12:50):

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