問題タブ [totality]

私は次のものを持っているとしましょうProgram Fixpoint：

l(この例は、単純な例を示すために、基本的に非常にばかげた方法で返されます)。

fここでは、 (格納されている)への再帰呼び出しがあります。これは、要素が含まれているf_rec場合にのみ使用されます。lf_reclength (tl l)length l

しかし、その義務を解決したいとき

私は必要な仮説を持っていませんhd_error l = Some n。

（なんとなく、 「実際に使われるまで計算を遅らせる」ではなく、「f (tl l)その場で計算する」と理解されている印象があります）。let in

let ... in違いを説明するために、ステートメントを「インライン化」すると、次のようになります。

ここに私はHeq_anonymous : Some n = hd_error []環境にあります。

私の質問は次のとおりです。必要な仮説を持つことは可能ですか、つまり、match ... withステートメントによって仮説を生成することは可能ですか?

注: を移動することletは解決策ですが、移動せずにこれが可能かどうか知りたいです。たとえば、f_recがさまざまなコンテキストで使用されている場合に、重複を避けるために役立つ場合がありf (tl l)ます。