この論文、参考になる。 https://kwarc.info/people/frabe/Research/KRW_isabelle_19.pdf Making Isabelle Content Accessible in Knowledge Representation Formats Michael Kohlhase, Florian Rabe, Makarius Wenzel 日付はハッキリしないが、2020以降なの…

WindowsのVoltaはかなり変な作りをしているらしい。C:/Program Files/Volta/ にある実行可能ファイルを実行すると、同名のcmdスクリプト/exeファイルを順番に再帰的にプロセス起動して、無限にプロセスを生成してしまう。C:/Program Files/Volta/ 内でプログ…

新しく導入する構文は： 変更可能代入文 副作用付きif文〈手続き的if文〉 キーワードと構文： let mut := 代入の右辺式は純 if-then-else if-then unless-do 翻訳： mutキーワードは、変数が変更可能であることを宣言する。let mut 変数 ← ... は、変更可能…

少しずつ説明。 構文範疇に、式と文〈ステートメント〉がある。 文には式文（式はそのまま文）と副作用let文がある。 do構文は式（do式）、純let式も式 let文といったときは副作用let文で、let式は純let式。 翻訳： do式の翻訳は、そのボディブロックを翻訳…

Voltaをバイナリでインストールした。 which node で C:\Program Files\Volta\node.exe それなら、C:\Program Files\nodejs\node.exe はいらないだろうとアンイストール。 node.exe を起動できなくなった。 どうやら、もともとあった node.js v16.14.0 をVol…

関数の意味： 関数そのもの＝集合圏の射 関数定義 関数{定義}?ヘッド＋関数{定義}?ボディ 関数定義ボディは計算項 定理・証明の意味： 定理（証明）そのもの＝演繹圏の射 定理記述 定理{記述}?ヘッド＋定理{記述}?ボディ 定理記述ボディは証明項 「証明」の…

例によって用語がややこしい。 型述語は、value is string のような構文。タイピング述語、タイピング関係といったほうが良いが、「型述語」。これは、型ガード関数や型アサーション関数の戻り値位置に書く形式。 型ガードが実は述語〈ブール値をとる関数〉…

前提： 条件{節}? conditional clause 事実： 主張 assertive sentence 判断： 証拠付き主張 ／ 証拠 with Evidence 質問： 疑問文 interrogative sentence / Question コンテキスト、項、戻り型〈return type〉がある。 コンテキスト 項 戻り型 記号 知識 …

曲線は入れてない。 M, m ：moveTo x,y 注意： M, mコマンドの後ろに座標を連ねた場合はLコマンドとして扱われる． L, l ：lineTo x,y V, v ：vertical x H, h ：horizontal y Z, z : endPath pathの属性は： stroke="noneか色" ： 描画線の色。noneだと何も…

https://dl.acm.org/doi/pdf/10.1145/3547640 より：

SVGの点線・破線は： 破線と点線の区別はない。幾つかの属性を使用する。 stroke-dasharray stroke-linecap storoke-dashoffset stroke-dasharray="間隔" 間隔は none 、または数値のカンマ区切りリスト、「描く／描かなない」の交代的並びで、繰り返し適用…

定義側： <defs> <symbol id="dogstamp" viewBox="0 0 395 372"> <path d="..."/> </symbol> </defs> 呼び出し側： <svg x="0" y="0" width="192px" height="166px" viewBox="0 0 192 166" > </svg>

総称型も「型」と言ってる。Type u → Type v は宇宙非エンド〈universe non-endo〉な型関数だが、これが単項〈1パラメータ〉の総称型。関手やモナドの台構造はこの種の「型」。広義の“型”上に構造が載るので型クラスになる。 「総称型＝型関数」という“型”上…

https://www.slideshare.net/onoremiz/mmorpg-14352457 より： レベルの要素とは： アイテムの配置 地形や動線の設定 敵の配置／AIの設定 ギミックの配置 クリア条件の設定 レベルデザインとは： ゲーム内の環境や経験をデザインすること。 レベルエディタ〈…

まず、Leanコミュニティでも用語の個人差がある。object, term, value, element なんかは要注意。型クラスのパラメータは、相対指標の部分指標の指定なので、ファイバー付き圏のベース圏を指定する。C が1パラメータの型クラスとして、固定したξに対して (C …

クラスBindは、">>=" または bind を持っている構造のクラス。 クラスPureは、pure を持っている構造のクラス。 クラスFunctorは、map を持っている構造のクラス。mapしてから適用するのを <$> で表す？？ 型クラスのベース〈パラメータ〉は型関数＝総称型だ…

Constructor Assignment と呼ぶようだ。いつもの決まりきった書き方を短く書ける。 interface Container { context : Bunch; outcome : Wire | null; } class Stage implements Container { constructor(public context : Bunch, public outcome: Wire | nul…

戻り値にステータスを返したいなら IO UInt32 とする。戻り値不要なら Unit でもよい。 def main(args : List String) : IO Unit := do let len := List.length args IO.println s!"length of args is {len}" for i in [0:len] do IO.println (List.get! arg…

s!を前置するとテンプレート文字列になる。他にもナントカビックリがあるのか？ s!"Hello, {hello}!"改行は普通に入れられる。エスケープの必要はない。

SVGの寸法単位（ピクセルやインチ）は意味がない、だってスケーラブルだから。SVG図形が描画される空間は仮想的・理想的な $`{\bf R}^2`$ だと思っていいので、寸法はすべて無次元数で書く。仮想キャンバスから表示に切り出す部分を viewBox で指定。ビュー…

Listはなぜかモナドから外されて単なる関手扱い。 白が“クラス”で青が“インスタンス”ということだろう。 矢印はクラス間の extends と、インスタンス-クラス間の member-of モナドの末尾は M というネーミングルールだが、守られてはいない。 Pure と Bind …

戻り値にステータスを返したいなら IO UInt32 とする。戻り値不要なら Unit でもよい。 def main(args : List String) : IO Unit := do let len := List.length args IO.println s!"length of args is {len}" for i in [0:len] do IO.println (List.get! arg…

s!を前置するとテンプレート文字列になる。他にもナントカビックリがあるのか？ s!"Hello, {hello}!"改行は普通に入れられる。エスケープの必要はない。

ステージと知識シーケントは同じもの。ステージは内部にシーケントをホストする。 ステージのコンテキストはステージ矩形の上部にだけ描いて、内部には貫入しない。 ステージのコンテキスト部のレイアウトは知識シーケントと同じ。 ステージは、コンテキスト…

基本的にステージクリア型ゲーム。ビジュアルノベル（選択式アドベンチャーゲーム）の要素も入る。 ステージはツリー状に配置される。親ステージと子ステージ〈サブステージ〉がある。 ステージツリーは、状態遷移により動的に変化する。 ステージにコンテキ…

Ident 公理 Cut オペラッド結合 Weak 水増し Cont 冗長性縮約 contraは矛盾 Perm 交換 CtxAndIntroL CtxAndIntroR CtxtOrIntro CtXImpIntro （LJ変形） CtxNotIntro CtxUnivIntro CtxExIntro TrgAndIntro TrgOrIntroL TrgOrIntroR TrgImpIntro TrgNotIntro T…

等式の種類： definitional equality ： Leanカーネルが判定する項の同一性。システムレベルで「同じ」とみなす。 propositional equality ： 等値性を意味する命題（真か偽の文）。証明がないと保証されない。システムレベルで事前に成立している同一性では…

型付きJSON（むかし、XIONとかXJSON呼んでいたヤツ）をマクロで実装する。 ベキ等可換モノイドからジョイン半束を作る。 乗法ベキ等可換環のスペクトル理論（昔のブログ記事にある） 距離連続写像は位相連続写像である。 定義・証明だけでなくて組織化を注意…

型と計算 命題と証明 型演算／構成子 命題結合子 依存型構成子 限量子 型ファミリー (命題ファミリー) インデックス域 論域 インデックス 個体 インデックス変数 限量束縛変数 関数 保証 戻り型 結論命題 ターゲット型 ターゲット命題（質問の） 引数リスト …

Coqの宇宙は {Set, Prop} → Type → Type → ... Leanの宇宙は Prop → Type → Type → ...Typeには番号が付く。別にどっちでもいい。圏論的には次の圏を準備する。$`\newcommand{\mrm}[1]{\mathrm{#1}} `$ $`{\bf Ded}`$ $`{\bf Set}`$ $`{\bf SET}`$ $`{\bf CA…