タイプクラスインスタンスのFixpoint関数

Question

タイプポイントインスタンスのコンテキストで固定小数点スタイル関数を使用しようとしていますが、動作していないようです。この仕事をするために何か余計なことがありますか？当分の間、タイプクラスの外で関数を移動し、明示的にFixpointとして宣言するハックを使用しました。しかし、これはひどいようです。ここで

は短い例です：

Inductive cexp : Type := 
| CAnd : cexp -> cexp -> cexp 
| COr : cexp -> cexp -> cexp 
| CProp : bool -> cexp. 

Class Propable (A : Type) := { compile : A -> Prop }. 

Instance: Propable cexp := 
    { compile c := 
     match c with 
     | CAnd x y => (compile x) /\ (compile y) 
     | COr x y => (compile x) \/ (compile y) 
     | CProp _ => False 
     end 
    }. 

これはで失敗します。

Error: Unable to satisfy the following constraints: 
In environment: 
c, x, y : cexp 

?Propable : "Propable cexp" 

何一つは、この作品を作るために関係があるのでしょうか？

Answer 1

あなたはそれを行うためにfixを使用することができます。

Instance: Propable cexp := 
    { compile := fix compile c := 
     match c with 
     | CAnd x y => (compile x) /\ (compile y) 
     | COr x y => (compile x) \/ (compile y) 
     | CProp _ => False 
     end 
    }. 

は私が1がそれを考え出すことができる方法を説明しましょう。のは、次のコードを見てみましょう：ここ

Fixpoint silly n := 
    match n with 
    | 0 => 0 
    | S n => silly n 
    end. 

Fixpointは、目の定義が少し簡単になりますが、それはここで何が起こっているか隠し方言のコマンドです。あなたが定義した後Print silly.を使用して、それを確認することができ

Definition silly' := 
    fix self n := 
    match n with 
    | 0 => 0 
    | S n => self n 
    end. 

：それは何コックが実際には、このようなものであることが判明しました。