タグ

関連タグで絞り込む (1)

タグの絞り込みを解除

ProofCafeに関するmzpのブックマーク (2)

  • はてなグループの終了日を2020年1月31日(金)に決定しました - はてなの告知

    はてなグループの終了日を2020年1月31日(金)に決定しました 以下のエントリの通り、今年末を目処にはてなグループを終了予定である旨をお知らせしておりました。 2019年末を目処に、はてなグループの提供を終了する予定です - はてなグループ日記 このたび、正式に終了日を決定いたしましたので、以下の通りご確認ください。 終了日: 2020年1月31日(金) エクスポート希望申請期限:2020年1月31日(金) 終了日以降は、はてなグループの閲覧および投稿は行えません。日記のエクスポートが必要な方は以下の記事にしたがって手続きをしてください。 はてなグループに投稿された日記データのエクスポートについて - はてなグループ日記 ご利用のみなさまにはご迷惑をおかけいたしますが、どうぞよろしくお願いいたします。 2020-06-25 追記 はてなグループ日記のエクスポートデータは2020年2月28

    はてなグループの終了日を2020年1月31日(金)に決定しました - はてなの告知
    mzp
    mzp 2010/07/17
    今週末は、栄でProofCafe!
  • Proof Cafe - rfなブログ

    4/25に、Proof Cafe (栄)に参加してきました。 Coq 初体験。 最初は、id:yoshihiro503 さんから資料に沿って Coq の解説が。 Vernacular が分かれば Coq が分かる? Coq のファイルの拡張子は .v Checkで 型を調べる。 ガリナ(Gallina):ラムダ式 nat : 型を表すラムダ式 (自然数) - Gallina 、この型はSet。 Set : 型を表すラムダ式 (型)、この型はType。 Type : 型を表すラムダ式 (型)、この型はType。 Prop : 命題の型 Eval compute in 〜 で、〜を評価できる。 その後、これをやってみる。 ↓書いたやつ。 (* listの定義 *) Inductive list (A: Type) : Type := | nil : list A | cons : A -> l

    Proof Cafe - rfなブログ
  • 1