帰納述語を定義するとき、どのパラメーターを固定し、どのパラメーターを固定しないかを選択できます。不自然な例として、次のことを考慮してください。
inductive foo for P where
"foo P True (Inl x) (Inl x)"
これを、1 つの固定パラメーターと 1 つの非固定パラメーターを持つ帰納的に定義されたセットに変換することは何とか可能ですか?
inductive_set Foo for P where
"(Inl x, Inl x) : Foo P True"
は次のエラー メッセージで拒否されます。
Argument types 'd, bool of Foo do not agree with types'd of declared parameter
帰納述語バージョン (例: ) に基づいてセットを定義できることはわかっていますが、Foo P b = {(x, y). foo P b x x}帰納またはケース分析を適用する前に、常にそれを展開する必要があります (または、対応するルールを導入する必要がありますFoo。これは少し冗長に思えます)。 ）。