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 Fixpoint
?
You can write an induction principle but it's boring because it just does destruct
/match
.
There seems to be some misconceptions.
Variant
forbids recursive types, which makes it an extremely restrictive form of Inductive
.Unset Nonrecursive Elimination Schemes
), Variant
does not produce an induction principle, because induction principles on non-recursive types are pointless.Fixpoint
is completely unrelated to the existence of an induction principle. You can write the exact same Fixpoint
functions, 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: Oct 13 2024 at 01:02 UTC