Isabelleタイプのエラー

Question

私はIsabelleを初めて勉強して、Exercise for Universityをやっています。私はイザベルで逆関数を証明する必要があります。

Haskellでは関数は次のようになります。私は今、イザベルでこの機能「REV」を定義するためにしようと試み

rev [] = [] 
rev (x:xs) = rev xs ++ [x] 

。タイプリストと機能「アプリ」（追加）

エラーイザベルは私を与えるには、次のとおりです。

Type unification failed: Clash of types "_ 
      ⇒ _" and "_ Exercise5.list" 

Type error in application: incompatible operand type 

Operator: app (rev xs) :: 
    'a Exercise5.list ⇒ 'a Exercise5.list 
Operand: Exercise5.list.Cons :: 
    ??'a ⇒ ??'a Exercise5.list ⇒ ??'a Exercise5.list 

どこに問題がありますか？私が理解している限り、Isabelleは「おい、バディアプリは2種類の引数をのリスト 'にする必要がありますが、ここには該当しません」

なぜですか？ xsは明らかにタイプa 'リストであり、私のコンス演算子ではxもリストにしていますか？

ありがとうございました！

Answer 1

括弧を入れたい場所を考えてみましょうapp rev xs Cons x Nil：現在は、引数Nilに関数xを適用しているようです。