coqtotality

What's the difference between Program Fixpoint and Function in Coq?


They seem to serve similar purposes. The one difference I've noticed so far is that while Program Fixpoint will accept a compound measure like {measure (length l1 + length l2) }, Function seems to reject this and will only allow {measure length l1}.

Is Program Fixpoint strictly more powerful than Function, or are they better suited for different use cases?


Solution

  • This may not be a complete list, but it is what I have found so far: