Table of Contents
目についたCoqのライブラリ/プラグイン/開発環境などの覚え書き
実用面は気にせず、研究用や無メンテも載せる
yamarten
1. 「依存型に触ったことある」もしくは「TaPLを部分的にでも読んだ」あたりが基準になるだろうか。
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
| (* Coqでアドホック多相 *) | |
| (* Coqで多引数の型クラスを用いた多相関数のサンプル *) | |
| (* 型クラスに性質(定理)が書けるのもCoqらしさではあるが、その辺は他所でも紹介されているので割愛 *) | |
| (* そういった機能については例えば: http://yosh.hateblo.jp/entry/20090904/p1 *) | |
| (* 角括弧でのリスト記法が使いたかっただけなので、コンストラクタ直書きならImport不要 *) | |
| Require Import List. | |
| Import List.ListNotations. | |
| (* 型クラス定義 ここでは関数を一つ持っているだけなので単に多相関数定義と思ってもいい *) |
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
| /* | |
| firequix.jxa | |
| bookmarklet organizer for Firefox with BetterTouchTool inspired by quixapp.com | |
| */ | |
| 'use strict' | |
| function run(argv) { | |
| // Please create bookmark to "javascript:%s" and set keyword. | |
| const keyword = 'javascript' |
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
| // ==UserScript== | |
| // @name YouTube DateTime | |
| // @match https://www.youtube.com/watch* | |
| // @grant none | |
| // @version 1.0.0 | |
| // @description Replace info with absolute datetime | |
| // @description:ja YouTubeの動画投稿・配信開始日時を表示 | |
| // ==/UserScript== | |
| (() => { |
実装はあんまり見ずに、ATPの雰囲気を把握するためのメモ
要素としては以下のような感覚。
- Repository: 署名つきRDB
- データ構造がRDB(というか表)という話で、SQL-likeな操作が規定されてるわけではない