演習用ファイルの不具合について

既にこれらのファイルに解答を書きこみはじめた人は，お手数ですが， 下記に従って，各自修正の上，解答してください． もし，まだ，これらのファイルをさわりはじめていない人は， あらためて ~kam/coq/CoreML.v や ~kam/coq/Eval.v をコピーしてください．

なお、これらは、稲川裕太君の指摘によるものです。どうもありがとう!

• CoreML.v の問題 e266 と e267 について: 項の型が，「bool」となっていましたが，正しくは「int」です． bool のままでは解答が作れません．

  Theorem e266 : 
    [] |- 
      (_fix z ( x ) 
         _if ((_left x) = %0) then %0
         else _if ((_right x) = %0) then _left x
         else z @ ((_left x) + (%-1), (_right x) + (%-1)))
      @ (%5, %3)
      \in int.  (* <-- it was "\in bool" in the older file *)
  

  Theorem e267 : 
    [w \in int * int -> int] |- 
      (_fix z ( x ) 
         _if ((_left x) = (_right x)) then _left x
         else _if ((_left x) > (_right x)) then 
             z @ (w @ x, _right x)
         else 
             z @ (w @ (_right x, _left x), _left x))
      @ (%10, %3)
      \in int.  (* <-- it was "\in bool" in the older file *)
  

  2015/11/25追記: e267 において w の型が int -> int -> int になっていま したが、正しくは、int * int -> int です。 (これは、高橋君の指摘によるものです。どうもありがとう!)

• Eval.v について： 問題ex524 の計算結果が，「#20」となっていましたが，正しくは「#35」です． #20のままでは解答が作れません．

  Theorem ex524 : initE >> (_lambda (x) x + %30) @ (% 10 + % (-5)) --> (#35).