I was reading
ITrees and came across
Variant, which I understand is an alternative to
Inductive when you don't need the induction principle. What are some use cases for this?
You can't accidentally write a
Fixpoint on a
Variant, apart from that it's just a minimalistic preference.
It's the number 1 FAQ from people who read the itree source code, I almost regret the distraction it causes :)
so without induction principle I can't write
You can write an induction principle but it's boring because it just does
There seems to be some misconceptions.
Variantforbids recursive types, which makes it an extremely restrictive form of
Unset Nonrecursive Elimination Schemes),
Variantdoes not produce an induction principle, because induction principles on non-recursive types are pointless.
Fixpointis completely unrelated to the existence of an induction principle. You can write the exact same
Fixpointfunctions, whether or not there is an induction principle for a given recursive type.
Set Elimination Schemes), Coq generates an induction principle for recursive types. In some cases, it is completely pointless. But since this principle has zero impact on
Fixpoint, one can always use the latter to define the correct induction principle.
fixpoints are forbidden on variants since https://github.com/coq/coq/pull/407 (as a side effect of forbidding fixpoints on records with eta)
Last updated: Jan 29 2023 at 04:05 UTC