ハマリ所
def toNum (b : Bool) : Nat := by cases b with | true => exact 1 | false => exact 0 #print toNum #print Bool.casesOn #eval toNum true --> 1 def toNum' (b : Bool) : Nat := by cases b exact 1 exact 0 #eval toNum' true --> 0 def toNum'' (b : B…
() はUnit型の唯一の要素。 (3) は 3 のこと。型 Nat (3, 4) はペア型 Nat×Nat (3, 4, 5) は Nat×Nat×Nat (3, 4, 5) = (3, (4, 5)) 右結合的な二項演算子 .1 は .fst、.2 は .snd ⟨カンマ区切り項目並び⟩ は構造体リテラルの略記。フィールド名を省略できる…
関数適用は必ず空白が必要。空白類が適用演算子の記号だから。一方、x.2 や x[3] のようなタプル／リスト／配列へのアクセスは、空白を入れてはダメ。空白が適用演算子なので、適用として解釈されてエラーになる。だいぶハマる。
WindowsのVoltaはかなり変な作りをしているらしい。C:/Program Files/Volta/ にある実行可能ファイルを実行すると、同名のcmdスクリプト/exeファイルを順番に再帰的にプロセス起動して、無限にプロセスを生成してしまう。C:/Program Files/Volta/ 内でプログ…
Voltaをバイナリでインストールした。 which node で C:\Program Files\Volta\node.exe それなら、C:\Program Files\nodejs\node.exe はいらないだろうとアンイストール。 node.exe を起動できなくなった。 どうやら、もともとあった node.js v16.14.0 をVol…
※ 2023-01-17に書いたけど投稿忘れ。関数型言語で、デカルト閉圏の射としての関数を表すことはできない。表わされるのは、関数型〈指数型〉の要素。要素をポインター関数とみなしても、表わされるのはポインター関数に限る。2つのポインター関数に対して、ev…
npmのpackage-lock.json相当が、Lakeマニフェストファイル。lean_packages/manifes.json と lake-manifest.json がある。注意すべきはマニフェストファイル自体のバージョンで、JSONファイルのトップレベルフィールドとしてバージョン番号が記入されている。…
#eval で値〈要素〉を表示するには、型が型クラス Repr の型インスタンスでなくてはならない。文字列化できるためには、型が型クラス ToStrng の型インスタンスでなくてはならない。
Powershell では、foo |& bar も foo 2>&1 | bar も効かない。標準エラー出力を tee でファイルに落とすのは現状分からない。bashなら次が出来るが、Powershellの代替は見つからないでいる。 lake build -v |& tee $(date +%Y-%m-%d_%H-%M-%S).lake-build.log
lakeはnpmほどには洗練されてないみたいだ。現状では完全な自動ビルドは無理な気がする。原因不明な失敗をすることがある。ビルドの手順は、原理的には次のようなことだと思う。 ./lean-toolcahin を見て、ツールチェーンがインストールされてなければ、elan…
プロジェクトディレクトリ内で elan show すると、そのプロジェクトのツールチェーンがダウンロードしてないと即座にダウンロードをはじめる。困ったもんだ。elan toolchain list を使うべし！lake build しても必要ならダウンロードして、elanツールチェー…
Lean 4ではキーワードを整理したらしく。 constantが廃止されて、axiomのみを使うようになった。 Πが廃止されて、∀のみを使うようになった。 assumeが廃止されて、funまたはλのみを使うようになった。 variables は廃止。variable が使える。 parameter, par…
Leanマニュアルでは "object" も使っているが、混乱のもとなので「要素〈element〉」を使う。「インスタンス」も混乱のもとなので使わない。「型の要素」を使う。型の要素が命題の証拠〈witness〉に対応する。次はセクションの定義： variable (F : Type → T…
def f1 (n:Nat) (m:Nat) : Nat := n + m def f2 (n:Nat) : Nat → Nat := fun (m:Nat) => n + m def f3 : Nat → Nat → Nat := fun (n :Nat) => fun(m:Nat) => n + m def f4 : Nat → Nat → Nat := fun (n m:Nat) => n + m #check f1 #check f2 #check f3 #chec…
wt.exe が2箇所にあった。 C:\Users\m-hiyama\AppData\Local\Microsoft\WindowsApps\wt.exe C:\Program Files\WindowsApps\Microsoft.WindowsTerminal_1.15.3466.0_x64__8wekyb3d8bbwe\wt.exe が、C:\Users\m-hiyama\AppData\Local\Microsoft\WindowsApps\wt…
variable b:Bool はダメで、variable (b:Bool) 。そもそも「変数」は通常の意味の変数ではない。共通に予約された暗黙束縛変数のこと。
図のタイトルをYAMLフロントマターにするのは使えねー。 統一性がない。 構文： flowchart sequence diag. ID[ラベル] タイプ ID as ラベル ソース アロー ラベル ターゲット ソース アロー ターゲット: ラベル 次のようにすれば、統一的だった。 ノードは …
Objectはオブジェクト型だけでなくて、ボクシングしてオブジェクトになるものも含まれる。null以外なんでもいい。{} が Object と同義なのは、どうかしている。object は {[key: (string|number)] : any} と同義かな？ たぶん。いずれにしても整合性がない。
flowchart と subgraph の構文が一致しない。flowchart id[title] direction TB なら良かった。 辺へのスタイリングが番号指定でカス
区別しにくいかも。 射としての関係 射をレイフィケーション（射 → 対象 変換）した集合（対象） ホムセットとしての全関係空間 ホムセットの部分集合としての制約された関係空間 全関係空間／制約された関係空間をレイフィケーションした集合（対象） 射の…
npmをアップデートしたら動かなくなった。エラーは TypeError: cleanUrl is not a functioncleanUrlを呼ぼうとして無いというもの。fixするには、 ~\AppData\Roaming\npm\node_modules\npm\node_modules\npm-registry-fetch\lib\index.js の最後に module.ex…
素のディレクトリでまだハマっている所がある。サンプルコードは var map:Map<number, string>; map = new Map<number, string>(); map.set(3, "hello"); console.log(map.get(3)); map.set(5, "world"); console.log(map.get(5)); for (let [key, val] of map) { console.log(`${key} = ${va</number,></number,>…
TypeScriptで、CommonJS設定なら export = fooFun; は使える。module.exports = fooFun; にコンパイルされる。 JavaScriptの exports 変数 JavaScriptの module.exports プロパティ TypeScriptの export 変数 TypeScriptの export キーワード これはハマるだ…
npm i generator-code とすべきを npm i generate-code とやってしまって、ダメだった。綴り間違い。[追記]npm i repl も間違いだった。https://www.npmjs.com/package/repl は小さいテンプレート処理関数、replace の意味だろう。Node付属のREPLのライブラ…
基本的なコマンドラインツール。 パケットが届くかは ping シェルアクセスは ssh 名前が引けるかは nslookup、digはbind-utilsというパッケージに含まれる。 WebページがGETできるかは curl、情報だけは curl -I アプリケーションレベルでアクセス確認は ftp…
セットアップスクリプトで ~hiyama/.forward を作ったが、chownしないとhiyamaが変更できない。パーミッションに色々と注意。 smtp のポートを開けてなかった。ネットワークソフトウェアは必ずポート確認。firewall-cmd --list-all コマンド。 他に、設定フ…
サーバーの設定・確認・テストにはやっぱりコマンドラインツールだな。 パケットが届くかは ping シェルアクセスは ssh 名前が引けるかは nslookup WebページがGETできるかは curl アプリケーションレベルでアクセス確認は ftp ブラウザはDNSキャッシュが邪…
マトリックスでエントリーを省略できるが、このときは不在エントリーとなる。不在エントリーはそこにオブジェクトがないとみなされる。{} で空エントリーを作れる。空エントリーは、内容が空なだけで存在する。不在エントリーへのアローは引けない。
constantは、域が単位対象＝空リストである射を宣言する。図では三角ノードになる。variableは、名前付きのワイヤーを準備する。意図としては、その名前付きワイヤーはラムダ束縛するつもりだから、事実上束縛変数の選言。変数名は混乱の原因になるから、で…
Leanの定義構文のプロファイル部は完全なシンタックスシュガーで、無視されて、内部的にはフルカリー化版が記憶される。そそもそも、内部の還元エンジン〈reductione engine〉がフルカリー化されたポイント射しか扱えない。これが、圏論的解釈とラムダ計算的…
