Stream: Coq users

Topic: coqpl well founded recursion

view this post on Zulip Gaëtan Gilbert (Jan 20 2024 at 14:24):

with Fix_F I think if you do Definition bla args := Eval cbv beta delta [Fix_F] in Fix_F ... you get basically the same definition as with directly recursing on the Acc (I think this simplification is probably what extraction does to get what it produces)
OTOH it's probably easier to write the direct Acc recursion so this is not very useful

view this post on Zulip Dominique Larchey-Wendling (Jan 20 2024 at 15:19):

Fix_F is precisely structural induction on Acc but with _delayed_ pattern matching on it via Acc_inv.

Last updated: Jun 22 2024 at 15:01 UTC