Stream: Coq users

Topic: Admit in fixpoint?


view this post on Zulip walker (Jul 06 2023 at 13:42):

I want to type check incomplete fix-point without worrying about missing cases, and unfotunately I cannot return trivial cases for the remaining fix point branches because there is no trivial case , what can I do ?

view this post on Zulip Karl Palmskog (Jul 06 2023 at 13:47):

you might be looking for this option

view this post on Zulip Wolf Honore (Jul 06 2023 at 13:53):

You could also try something like

Axiom TODO : forall {A}, A.

Fixpoint f n :=
  match n with
  | O => true
  | S n => TODO
  end.

view this post on Zulip walker (Jul 06 2023 at 14:07):

noted thanks everyone, I think I will move on with the todo.


Last updated: Jun 23 2024 at 04:03 UTC