title | tags | author | slide |
---|---|---|---|
Coq で圏論:随伴、モナド、Kleisli triple |
Coq Coq-8.5 |
mathink |
false |
- Coq 上で随伴とモナドを定義
- Kleisli triple(Haskell でいう Monad)も定義
- 随伴から、モナドを通じて Kleisli triple を構成してみた
---
title: Coq: Set Primitive Projections と injection タクティックのお話
tags: Coq Coq-8.5
author: mathink
slide: false
---
Set Primitive Projections
時は Record
と injection
の相性が悪いよUnset Primitive Projections
するか、 Inductive
で定義してアクセサを別途定義する形にするといいかもね---
title: Coq: 引数にパターンが使えるようになったので試してみた
tags: Coq Coq-8.6
author: mathink
slide: false
---
Coq の 8.6 が出た ので CHANGES を覗いてみたら
title | tags | author | slide |
---|---|---|---|
依存型/\型クラス/\記法 -> (テスト失敗 <-> 型エラー) |
Coq |
mathink |
false |
7日目の記事は fetburner さんの 単一化の証明 でした。
title | tags | author | slide |
---|---|---|---|
Coq で環のイデアルを作ってみる |
Coq |
mathink |
false |