Skip to content

Instantly share code, notes, and snippets.

View qnighy's full-sized avatar

Masaki Hara qnighy

View GitHub Profile
@qnighy
qnighy / arith.pegjs
Created April 18, 2015 09:37
PEG.js parser example
View arith.pegjs
// PEG.jsによる数式パーサーのサンプル
// 次の構文をサポート
// - 二項演算子 : "+" "-" "*" "/" "**"
// - 単項演算子 : "-"
// - 演算子の優先度と結合順
// - 括弧 ( )
// - 空白
// - ネストするコメント (* *)
// - ネストしないコメント /* */
// - 行コメント //
@qnighy
qnighy / KDtips.md
Last active December 23, 2023 08:53
Kinky Dungeon知見
View KDtips.md

Kinky Dungeon とは

こちらの入門情報を参照してください https://gist.github.com/qnighy/393b132ef431023653b6098a91602830

拘束の外し方

  • 錠を外す
    • 普通の錠 …… 鍵かピックを使うのが一般的です。ピックは壊れるまで再利用できますが、解錠に時間がかかる上に、条件が悪いとどんどん壊してしまうので使い所を選ぶ必要があります。また、シンプルな鍵は再利用可能です。これは持っていればメニューから使えます。
    • 丸い錠 …… 普通の錠に近いですが、普通のピックでは開けられず、専用アイテムと組み合わせて使う必要があります。
  • 頑丈な錠 …… ピックが使えない?
@qnighy
qnighy / KDintro.md
Last active December 23, 2023 08:29
Kinky Dungeon入門
View KDintro.md

Kinky Dungeonとは

Kinky Dungeonとは拘束具をテーマにしたローグライクです。 ※性的な内容を含むため注意

https://ada18980.itch.io/kinky-dungeon/

Kinky Dungeonのバージョン

v4系とv5系があります。

@qnighy
qnighy / README.md
Last active December 17, 2023 03:16
X(Twitter)のリンク制限回避テスト
View README.md

リンク先はこちら

https://www.pixiv.net/artworks/114116251

(リンク先は適当に選んだもので他意はありません)


背景

2023年現在、X(Twitter) は外部リンクに対して強い制限を課しています。特に特定の外部SNS (YouTube, Instagram など) やセンシティブコンテンツの多いサイト (DLsiteなど) ではペナルティがあると言われています。

@qnighy
qnighy / sprintf.v
Created August 12, 2012 02:14
Coqでsprintf
View sprintf.v
Require Import Ascii String.
Require Import List.
Require Import Arith NArith ZArith Omega.
Require Import Recdef Program.Wf.
Require Import Zdiv.
(* Local Notation "a :: b" := (String a b) : string_scope. *)
Definition Z_to_digit(n:Z):ascii :=
match n with
@qnighy
qnighy / steam_deck.md
Last active September 30, 2023 06:04
Steam Deck Memo
View steam_deck.md
@qnighy
qnighy / README.md
Created July 23, 2023 15:10
ティアキン白龍素材集め
View README.md

ティアキン白龍素材集め

ティアキン には白龍という大型の魔物が出現する。この魔物からは高価な素材が取得できるが、うまくやるとゲームを半分放置しながら「ながら」作業で金策ができるので、そのルートをメモしておく。

白龍とは

白龍はドラゴンの一種で、ハイラル上空をゲーム内時間で約4日 (実時間で約1.5時間) かけて周回している。

白龍は攻撃をせず接触ダメージもないため、そのまま乗り続けることができる。

@qnighy
qnighy / Quotients.v
Created November 28, 2012 12:10
いま話題の9÷0=0をCoqで証明
View Quotients.v
Require Import Coq.ZArith.ZArith.
Require Import Coq.QArith.QArith.
(* テーマ: Coqで 9÷0=0を証明する *)
(* 整数上の除算 *)
Theorem Quotient_1: (9 / 0 = 0)%Z.
Proof.
@qnighy
qnighy / modal_mu.v
Last active May 11, 2023 18:23
Modal mu calculus in Coq
View modal_mu.v
Require Import Coq.Classes.SetoidClass.
Program Instance Iff1Setoid{A:Type} : Setoid (A->Prop) := {|
equiv := fun P Q => forall x, P x <-> Q x
|}.
Next Obligation.
split.
- intros P x; reflexivity.
- intros P Q H x; symmetry; exact (H x).
- intros P Q R H0 H1 x; transitivity (Q x); [exact (H0 x)|exact (H1 x)].
@qnighy
qnighy / hott-coq-oboegaki.md
Last active April 22, 2023 04:27
HoTT/Coq 覚書
View hott-coq-oboegaki.md

はじめに

HoTT(ホモトピー型理論) はホモトピー論や∞圏論を型システムの上で展開しようという考え方である。この体系は既にCoqで形式化が進んでいる。これはその使い方の覚書である。

HoTTの参考資料

まず、HoTT/Coqではなく、HoTT全般に関係する資料について述べる。

  • HoTTの本家サイト http://homotopytypetheory.org/ に情報がたくさんある。この分野は数学の他分野に比べて、インターネット上に情報がより集約されているという特徴がある。
  • HoTTについて紙面で勉強するならば、上のサイトにあるHoTT Bookを読むのが最も適切である。