Coq： `Function ... with`構文

Question

InductiveとFixpointのように、Functionのw/withを相互に定義できます。あなたは文法やこれの例を教えていただけますか？どこにも何も見つかりませんでした。 Fixpoint （これは何も見つかりませんでした）と同じと思います。非稼働（ただし、ハーフコンパイル - 2つの最後の行は赤でハイライト）例：

Variable ARG:Type. 
Variable phy inf phyinf: ARG. 
Function Phy (x:ARG): ARG := match x with Inf x => phyinf | _ => phy end 
with Inf (x:ARG): ARG := match x with Phy x => phyinf | _ => inf end. (*Error: Unknown constructor: Inf.*) 

Answer 1

さてさて、私は私が最終的にあなたの質問を理解だと思います。

実際にいくつかを定義する方法があります。Fixpointこれは変形部分hereに（軽く）記載されています。

同様に、いくつかのInductiveタイプを相互に定義する方法があります（hereと記載されています）。

また、いくつかを相互に定義する方法があります。Functionしかし、マニュアルは、この機能について作る発言に注意してください。

は

Function建設は相互再帰的な定義を定義することもwith拡張子を楽しんでいます。ただし、この機能は非構造的再帰関数では機能しません。

ハーフワーキングの例で得られるエラーは、構文に関するものではなく、Function ... withの機能に関連していません。エラーは誘導型に対してのみパターンマッチングを使用でき、分岐はコンストラクタで開始する必要があることです。あなたの例では、ARGは誘導型ではなく、Infはコンストラクタではありません。あなたが表現しようとしているものが実際には見えないので、私はあなたの例を本当に「修正」できません。この例はこの質問のためだけに作られたのですか？この場合、あなたはそれをあまりにも少なくしました。

PS：どういうわけか、あなたはinduction-recursion（再帰関数と帰納型を同時に定義する）をしようとしていたのだろうかと思います。これが当てはまる場合は、運がない：Coqにはまだこの機能がない。