MATHINK

概要

当 web サイトについて

数学・プログラミングその他についてのメモが主になる予定.

mathink について

  • カジュアル Coq ユーザ
  • 圏論勉強中
  • 絵を描くこともある

という具合.元気です.

Coqのこと

tree@SSReflect
tree 構造を SSReflect 風味で作ったというお話
圏をつくろう(前編) -Why do we use Coq?-
SSReflect 風味に圏を定義する.その動機についての寸劇.
二分探索木を Coq with SSReflect で弄くる
その名の通り.
Coq で Setoid を作る。
Coq で Setoid を作る方法についての解説。と思しきもの。
Setoid の Proper な Map を作る。
Setoid の間の「写像」を作る方法についての解説。そしてとある挫折。
代数的構造と Coq:序
マグマから二通りの方法で群を作るお話 in Coq。破と急はいつになるのでしょうねぇ。

リンク

Service Account
Twitter @mathink
github mathink
Qiita mathink

Author: SDK@mathink

Created: 2015-06-28 Sun 02:42

Emacs 24.5.1 (Org mode 8.2.10)

Validate