11月
22
coqtokyo 第34回Ssreflect勉強会
主催 : yoshihiro503
| 募集内容 |
参加枠 無料
参加者数
自由発表枠 無料
先着順
|
|---|---|
| 申込者 |
|
| 開催日時 |
2022/11/22(火) 19:00 ～ 20:50
|
| 募集期間 |
2022/11/14(月) 18:30
〜 |
| 会場 |
オンライン |
| 参加者への情報 |
(参加者と発表者のみに公開されます)
|
イベントの説明
2020年の名古屋大学での講義資料を読みます。 https://www.math.nagoya-u.ac.jp/~garrigue/lecture/2020_AW/index.html ページ毎にその場で当てられた人が音読します。
第14回 subs_subの証明のつづきから
Lemma subs_sub x t t' : {subset vars (subs x t t') <= union (vars t) (vars t')}.
Proof.
move=> a. elim: t'=> //.
- (* Var *)
move=> v'. rewrite /subs.
rewrite in_union_or.
case: ifPn => [/eqP -> |xv'].
+ by move => ->.
+ move=> ->. by rewrite orbT.
- (* Fork *)
(*ここから 2022 11/8 *)
開催場所
google meetによるオンライン開催です。 URLは参加者と発表者に公開されます。
参加できないなど困ったときは、＠tmiya_ @khibino @eldesh @yoshihiro503にお問い合わせください。
タイムテーブル
19:00 - 20:30 ssreflectの講義資料を読む
5分休憩
20:35 - 20:50 自由発表
持ち物
Coqを動かせるPCなどの端末
参考情報
gistのコードをjscoqで動かす coqban というもあります https://proof-ninja.github.io/coqban/?gisturl=https%3A%2F%2Fgist.github.com%2Fyoshihiro503%2F7163cfa52557cc0a6be39fdf899e19f6
Slack
気軽に質問や雑談を出来るように、coqtokyo.slack.com を試験運用しています。 ＠tmiya_ @khibino @eldesh @yoshihiro503 のうちのだれかに頼んで登録してもらってください。( slack でアカウントとして利用するためのメールアドレスをお知らせください )
資料 資料をもっと見る／編集する
資料が投稿されると、最新の3件が表示されます。
フィード
2022/11/14 18:30
coqtokyo 第34回Ssreflect勉強会 を公開しました！
tmiya_
khibino
yoshihiro503
eldesh
takumi-kato
エンジニアをつなぐ
connpass は株式会社ビープラウドが開発・運営しています