TojoQK の投稿
素のGNOMEを知る 〜「集中」のためのデスクトップ環境〜
素のGNOMEを使ってみた感想です。キーワードは「集中」です。
ノートパソコンを冷やすファンを買った話
ノートパソコンを冷やすファン(ELECOM の FAN-U177BK)を買ったところいい感じだったので紹介
骨伝導イヤホンの OpenRun (無印) を購入した感想
骨伝導イヤホンの OpenRun を購入した感想
自由ソフトウェアの話をするのが難しい理由
何故自由ソフトウェアの話がまともにできないのかについて考察しました
Web サイトをリニューアルしてタグを追加した
Web サイトをリニューアルしてタグ機能を追加しました
TojoQKの日記について
公開日記を始めました。上のメニューから日記に遷移できます。
ハフマン符号化して復号すると元に戻ることをACL2で証明した
ハフマン符号化して復号すると元に戻ることをACL2で証明しました。全体的に解説は少なめですが、ACL2 の elim ルールについての説明は詳しいと思います。
ACL2 で自然数の和の剰余と剰余同士の和の剰余の等しさを示す
ACL2 で剰余関連の証明の試みをしたときの個人的な覚え書きです。
腕時計 F-201WA の個人的な用途について
CASIO の腕時計 F-201WA の私の使い方について熱く語ります。
自動定理証明器 ACL2 の入門向けに L-99 の1問目を解きました
ACL2 の入門向けに L-99 の一問目を解きました(動画付き)
RSS の旧 URL を新 URL へリダイレクトしました
以前から RSS で記事を購読されていた方向けの共有です
ACL2 でリストの回文に関する性質を証明した
ACL2 で Lisp のリストの回文に関する証明を試みました
ACL2 で鳩の巣の原理を使ってみた
ACL2 で鳩の巣の原理を使った証明を試みます
ACL2 でリストの回転に関する性質を証明してみた
ACL2 でリストの回転に関する性質を証明してみた(未完)
システム x による支配
システムによる支配について会話劇を用いた解説です。x に色々入れてみよう。
Emacs の時刻表記が日本語から英語に変わる問題の解決法
Emacs の時刻表記が日本語から英語に変わってしまう問題の解決法についての解説
Web サイトをリニューアルしました
Web サイトをリニューアルしました
ACL2 で組み合せの数とその階乗表現の関係について証明してみた
ACL2 で再帰で求める組み合せの数と階乗表記の計算方法で計算結果が同じになることを示しました
ACL2 で全ての組み合わせを求める関数の長さの性質について証明してみた
全ての組み合せを求めてから長さを求めるのと最初から組み合せの数を求めるので同じ値を得られると証明しました。
Nextcloud サーバーを構築しました
Nextcloud のサーバーの運用を始めた動機と構築方法について
開発者による支配から身を守るために自由ソフトウェアを使いましょう
自由ソフトウェアの使用を推奨するための非エンジニア向けの文書
ウェブサイトの見た目を改善しました
Web サイトの見た目をよくしました
org-mode で記事が書けるようになりました
haunt を拡張して org-mode を使って記事を書けるようにしました。
排中律と二重否定除去をTyped Racketで実装する
「排中律と二重否定除去をSMLで実装する」という記事の Typed Racket 版です。
Serverless Frameworkを使ってRacketのプログラムをAWS Lambdaにデプロイしてみた
Serverless Framework を使って Racket のプログラムをデプロイする極端な方法を解説します。
個人用途であっても独自ドメインのメールアドレスを使う理由
個人用途であって独自ドメインを使うことを推奨します
こんにちは、世界!
Webサイト「TojoQK」への最初の投稿です