※ 2023-01-17に書いたけど投稿忘れ。関数型言語で、デカルト閉圏の射としての関数を表すことはできない。表わされるのは、関数型〈指数型〉の要素。要素をポインター関数とみなしても、表わされるのはポインター関数に限る。2つのポインター関数に対して、ev…

※ 2023-01-17に書いたけど投稿忘れ。演算子の優先度 - (新) 檜山正幸のキマイラ飼育記 メモ編 の続きLeanの場合、まだ調整は必要かも知れない： PrefixSuffixPrecidence 1024 = max ArgumentPrecidence 1023 = arg CompositionPrecedence 90 ($`\circ`$) Exp…

散文化は prosify。 映像作品を、通常の文章に直して伝えること。 映像作品を鑑賞することは誰でも出来るが、ノベライズ／散文化は難しい。

「状況」、「シーン」なども用語候補だが、「ステージ」を使う。コマンドは、ステージ上の判断／質問を操作する。またステージ自体もコマンドで操作する。同じ名前に対して、フォワードコマンド doXxx とバックワードコマンド undoXxx がある。全般的な管理…

型 ←→ 命題 ←→ 対象 関数（要素含む） ←→ 定理（証拠含む） ←→ 射 関数コンビネータ ←→ 定理コネクティブ？（言及も命名もされない） ←→ オペレーター／コンビネータ リーズニング・コマンド 対応物がないゲーム・コマンド 圏論的に整理するなら もの〈シン…

B -A が before, after のオプション。-B 3 -A 3 は単に -3 でも同じ。-C は -2 つまり -B 2 -A 2 と同じ。 mathlib > git branch * master mathlib > git rev-parse master 8618f40d51539454fe06511d5c8504a77f30c598 mathlib > grep -A 3 -B 3 8618 ..\..\…

structure PreOrder where U : Type le : U → U → Prop le_refl : ∀(x : U), le x x le_trans : ∀(x y z: U), (le x y ∧ le y z) → le x z inductive ab where | a | b def ab_le (x : ab) (y : ab) : Prop := match (x, y) with | (.a, _) => True | (.b, .…

set_option pp.notation true in #print Eq.trans set_option pp.notation false in #print Eq.transset_option pp.notation false in #check 1 + 3 set_option pp.notation true in #check 1 + 3