参考： MLソースを扱うとき - 檜山正幸のキマイラ飼育記 メモ編 デスクトップにIsabelle2016（少し古い）のアイコンがある。 このアイコンは C:\Installed\Isabelle2016\Isabelle2016.exe を指している。 Isabelle2016.exeの実体は、jEditをフロント、PolyML…

球体状n-圏（globular n-category）において、次元が違う射を、恒等引き上げ（identity pull up）を使ってから結合することをヒゲ操作（whiskering; ウィスカリング）と呼ぶ。このとき、射の次元の差を次元差と呼ぶ。ヒゲ操作は、射を表現するダイアグラムに…

マニュアルによると： Maxima Lisp foo $foo 名詞のfoo %foo ?foo foo しかし、実際にやってみると、 :lisp (setq foo 'bar) :lisp foo /* => BAR */ Lisp側での名前が全部大文字の名前になってしまう。なんだ？？いずれにしても、:lisp $名前 は探索に役に…

基本的なディレクトリは、maxima_userdir と maxima_tempdir 変数に入っている。ファイルの検索位置（ディレクトリ）は、file_search_maxima, file_search_lisp変数に入っている。C:/Users/hiyama/maximaディレクトリがfile_search_maxima変数に入っているの…

wxMaximaがどうも使いにくいのは、コマンドラインシェルではなくて、セルの集まりのワークシートをモデルにしていたのか。コマンドラインとして入力するのではなくて、セルの内容を入力して、セルが評価されるというスプレッドシート方式だったのか。操作モ…

プロットオプション ['same_xy, true], ['same_xyz, true] でスケールが揃う。 wxplot2d([parametric, cos(t), sin(t)], [t, 0, 2*%pi] , [same_xy, true]) ; contour_plot(1/(1+x^2+y^2),[x,-3,3],[y,-3,3], [same_xy, true]); plot3d(10/(1+x^2+y^2),[x,-3…

.lisp, .macファイルのありか $MAXIMA_HOME/share/maxima/5.40.0/src/ の下 $MAXIMA_HOME/share/maxima/5.40.0/share/ の下 ラムダ式 lambda([ローカル変数リスト], 処理本体) block式 Lispのprogn形式やRのlocal式のようなもの。入れ子のブロック構造を作る…

等号の判定には、is(式 = 式), e.g. is( 1 + 1 = 2) 方程式を解くには、solve(方程式, 未知数変数), e.g. solve(x^2 - 1 = 0, x) 微分するには、diff(式, 変数), または diff(式, 変数, 微分回数), e.g. diff(x^2, x), diff(x^2, x, 2) tex(式) でtexのテキ…

2パラメータの3dサーフェイスが基本で、特にカーブ用の関数は用意されてない。2パラメータのうち片方をダミーにして使う。 plot3d([cos(t), sin(t), (1/3)*t], [t, -4*%pi, 4*%pi], [k,0, 1], [grid,500,1])ここで、kはダミー変数で無意味。tだけがパラメー…

edit 関数名 editvar 変数名 Rでもデータフレームの編集に簡易スプレッドシートみたいんがあったけど、似たり寄ったり。

エディタでCtrl-Gでコードナビゲーターが出現する。まーまー便利。

$MIZFILE/mml.larにすべてのアーティクルの名前（list of articlesだろう）。mml.vctにすべてのシンボル。

::> 121: Disagreement of argument types ::> 191: Unknown schemeこれの原因は、environ部の不備だった。schemes NAT_1; だけではスキームのインポートが出来ない。 constructors NAT_1; が必須、これがないとUnknown schemeが出る。registrations NAT_1; …

environがホントに難しいが、environ部を（もし）書けたら、明らかな命題を確認する。 INDUCT2: for n, m being Nat holds n + 1 = m + 1 implies n = m; INDUCT3: for n being Nat holds n + 0 = n; INDUCT4: for n, m being Nat holds n + (m + 1) = (n + …

メニューツリーのパス: [Plugins]-[Plugin Options] タブ: [Plugin Options] ツリーコントロールのパス: /Isabelle/General レコードのフィールド名: Auto Quickcheck UIの種類を無視してパスで示すと Plugins/Plugin Options/Plugin Options/Isabelle/Gener…

impI, assoc, transとかは、誰でもどこでも使いそうな名前なので、まずバッティングするだろう。find_theorems name: で検索して、修飾されたフルネームで指定するのが安全。

やた、やっとデバッガ的なナニカを見つけた。 https://arxiv.org/pdf/1406.0292v1.pdf

tipsつうか、jEditの常識だろうが、 変数 - 青 定数 - 黒 束縛変数 - 緑 型変数 - 紫 型定数 - 黒 キーワード - 薄めの青、緑 コメント - 茶色 内側構文 - 背景：薄い灰色 まだ評価してない - 背景：ピンク 計算中 - 背景：濃いめの紫 エラー - 背景：赤

素直に「ルールXxxを適用する」と読まない！ ルールは常識的な上から下の推論図で描かれる。推論（リーズニング）は逆方向だから、 ルールXxxを逆適用する

C-x 8 RET 221e RET C-x 8 RET infinity RET

print_options 便利。

lemmas（複数形！）というコマンドがある。lemmas G = A B C のように書いて、複数の定理をグルーピングできる。lemmas X = A なら、定理Aに別名Xを与えることが出来る。これを使うと、特定の名前Aの定理の内容を目視できる。ダミーの名前 X を使って、lemma…

これで、-Wall -Wextra でも警告が出ない。 #define UNUSED_VAR(x) (void)x; int main(int argc, char *argv[]) { UNUSED_VAR(argc) UNUSED_VAR(argv) int k; UNUSED_VAR(k) return 0; }

サイズがはっきりした整数を使いたいなら、stdint.h を使え。unit32_t とかある。

クリックでリライトが発生することがあるが、何が起きたか分からないことがある。リライトを引き起こすセルを、そのリライトのトリガーセルと呼ぶことにすると、リライトとトリガーセルの関係は分かりにくい。トリガーセルはあくまでトリガーであって、その…

例： Create A, B, C, D Create f:A->B, g:B->C, h:A->C, k:C->D, j:B->D Create α:: f*g => h : A->C Create β:: j => g*k : B->Dβにヒゲ結合で、fを付ける。 f*β:: f*j => f*g*k f*βのターゲットの右部分 f*g と αのソース全体 f*g が一致する。 βの境界の…

描いた図形を一時的に保存して後で使いたいとき。 Theoremでパレットに入れる。 一時的だから名前を付けなくてもいい。 パレットに入ったサロゲートをSelectする。 サロゲートをクリックすると、リライターが動いて定義が展開される。 Restrictで見えている…

Projectカウンターの番号は、射影のファイバーの次元となる。これは、元図形と射影図形の次元の差。埋め込みではないので余次元というのはオカシイ。適切な言葉がないが、情報がどの程度落ちるかを示す。数が多くなると、それだけ情報が落ちて粗雑になる。Pr…

> search() [1] ".GlobalEnv" "package:stats" "package:graphics" "package:grDevices" [5] "package:utils" "package:datasets" "package:methods" "Autoloads" [9] "package:base" > searchpaths() [1] ".GlobalEnv" [2] "C:/Installed/R/R-3.2.2/library…

x instanceof y の代わりに、inherits(x, "y" ) が使える。