ステンレスのforallコンストラクトの使用

Question

私はステンレスで証明しようとしていますが、2つのリストの内容が同じで、1つのリストがxで囲まれていれば、もう一方のリストもxで囲まれています。そうするために、私は、構文を使用するように言われている：

forall(x => list.content.contains(x) ==> p(x)) 

補題のように（冗長な方法で）書かれます：問題は、私は次のエラーを得ることである

def lowerBoundLemma(l1: List[BigInt],l2: List[BigInt],x:BigInt) : Boolean = { 
    require(l1.content == l2.content && forall(y => l1.content.contains(y) ==> y <= x)) 
    forall(z => l2.content.contains(z) ==> z <= x) because{ 
     forall(z => l2.content.contains(z) ==> z <= x) ==| l1.content == l2.content | 
     forall(z => l1.content.contains(z) ==> z <= x) ==| trivial     | 
     forall(y => l1.content.contains(z) ==> y <= x) 
    } 
    }.holds 

：

exercise.scala:12:48: error: missing parameter type 
require(l1.content == l2.content && forall(y => l1.content.contains(y) ==> y <= x)) 

私はyにタイプを追加すると、私は（括弧が含まれているの左中括弧を指して）このエラーが出る：

exercise.scala:12:81: error: ')' expected but '(' found. 
require(l1.content == l2.content && forall(y : BigInt => l1.content.contains(y) ==> y <= x)) 

これはなぜ起こっているのですか？

私はまた、構文l.forall(_ <= x)を試みたが、タイプのbecauseと==|のような構造と組み合わせたとき、私はエラーを取得：ブールのメンバーではないので。

Answer 1

あなたが直面している問題は、ScalaコンパイラのフロントエンドからStainlessに移行しています。スカラ座では、（指定されたパラメータの型を持つ）閉鎖のための構文は(x: Type) => bodyです（余分な括弧に注意してください！）

あなたはbecauseと==|を使用する場合は、ソースファイルの先頭にimport stainless.proof._を追加する必要があります。