- Coq … INRIAが開発した証明支援系。 http://coq.inria.fr/
- ssreflect … INRIAとMicrosoft Researchが開発した代数の証明群および、そのために作られたCoqの拡張文法。 http://www.msr-inria.inria.fr/Projects/math-components
- CoqTop … CoqのREPL。ちょっとした照明を書くときには使えるかもしれないが開発するのにはほぼ使えない。後述するIDEを使うこと。
Eric Sartre siritori
qnighy
/ coq-cheatsheet.md
Last active
April 2, 2018 13:05
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| // Written in the D programming language. | |
| /** | |
| * High peformance downloader | |
| * | |
| * Implemented according to <a href="http://yusukebe.com/archives/20120229/072808.html">this implementation</a>. | |
| * | |
| * Example: | |
| * ----- | |
| * dmd -L-lcurl -run downloader.d |
takkkun
/ gist:1864479
Created
February 19, 2012 16:14
— forked from uneco/gist:1333025
文字数が同じで意味が反対の英単語
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| slow 遅い | |
| fast 速い | |
| above より上に | |
| below より下に | |
| absolute 絶対的な | |
| relative 相対的な | |
| abstract 抽象的な |