入力法は、コマンド "lean4: Show all abbribiations" で表示される。 文字 名前 番号 入力法 用途 “λ” Greek Small Letter Lamda U+03BB \lam ラムダ抽象 “↦” Rightwards Arrow from Bar U+21A6 \map ラムダ抽象の区切り “·” Middle Dot U+00B7 \. 無名ラム…

def main (args : List String) : IO UInt32 := doimport Mathlib.Tactic.LibrarySearch #check library_search%パーセント記号は相変わらず意味不明。名前短縮とは、修飾名を短くすること。ひとつは、open でカレント名前空間に別名前空間の名前をぶちまけ…

def main (args : List String) : IO UInt32 := doimport Mathlib.Tactic.LibrarySearch #check library_search%パーセント記号は相変わらず意味不明。

http://www.omdoc.org/pubs/omdoc1.2.pdf の印刷ページ21（p.37）から：Definition 3.2.5 (Monoid) A monoid is a semigroup $`S = (G, \circ)`$ with an element $`e\in G`$, such that $`e ◦ x = x`$ for all $`x ∈ G`$. $`e`$ is called a left unit of $…

単語： 直積と直和は双対です。 λ記法 有向グラフ 射 閉圏 関手 双対 域・余域 終対象・始対象 錐・余錐 語句・文： 双対的に、関手の余極限からの射 関手の余極限からの射 双対的に、関手の余極限は余錐の圏の始対象の頂点になっている。余極限への射が一意…

モジュール（Leanモジュールと外部・他言語モジュール） 名前空間 セクション キーワード （module は無い、欲しかったが） import namespace section open ： pretectedなら修飾必要、privateは見えない。export は修飾なしになる。 scoped ： 名前空間内に…

数値ランク付きタグの構文は、例えば [s3] のように数字で終わる名前として、[printed 2023-02-11] のようなパラメータを持ったタグも欲しくなる。名前空間を識別する接頭辞付きタグをいれると、構造タグは： 名前空間接頭辞で修飾されたタグ 数値ランク付き…

自然数の具体的リテラルを (nat_lit 3) とか書くが、事情は不明。追記： /-- The `nat_lit n` macro constructs "raw numeric literals". This corresponds to the `Expr.lit (.natVal n)` constructor in the `Expr` data type. Normally, when you write a…

罪も多い。次を混乱させてしまった。 指標とモデル圏 パラメータ付き指標とファイバー付きモデル圏 忘却射影に対するセクション（so-called インスタンス） ひとつのモデル モデル圏／ファイバー付きモデル圏のあいだの関手（構成手続き） 特に、ファイバー…

({foo := "hello"} : Bar) の代わりに、{foo := "hello" : Bar} が使える。 namespace Temp structure Bar where foo : String := "hello" baz : String := foo ++ "world" #check {foo := "hi" : Bar} #check { : Bar} #eval { : Bar}.baz instance : ToStr…

自然数集合から可換モノイドへのインスタンスメーカーが3つあって、 足し算 掛け算 最大値（小さくないほう） 最小公倍数 それとは別に、ベキ等可換モノイド（演算記号 ◇）をジョイン（演算記号 ∨）半束にするインスタンスメーカーがあるとする。インスタン…

指標Σに対して、モデルの集合は |Model[Σ]| となる。適当な集合 K からの写像 K → |Model[Σ]| をインスタンスメーカー〈クリエイター | コンストラクタ | ビルダー〉と呼ぶ。なんらかの忘却射影 U:|Model[Σ]| → K があり、インスタンスメーカーがセクション…

theorem ext {a b : Set α} (h : ∀ (x : α), x ∈ a ↔ x ∈ b) : a = b := funext (fun x ↦ propext (h x))事実 半形式的：$`\text{Fact ext}\\ \text{For } a, b : \mathrm{Set}\: \alpha \\ \text{When } \forall (x : α),\, x \in a \iff x \in b \\ \text{…

https://m-hiyama.hatenablog.com/entry/20161210/1481350849 の昔のコード、以前は問題なかった。 <img width="600" src="http://www.chimaira.org/img3/Mizar.jpg" >((画像は https://it.wikipedia.org/wiki/Mizar より)) 今は、行内のHTMLコメントで…

対応表： 定理記述 関数定義 定理のステートメント 関数{定義}?のヘッド 証明項 計算項 定理記述する 関数定義する から導出された定理 から定義された定理 構文と意味は混同される。 関数そのもの（型の圏の射）と関数定義という構文対象 定理そのもの（命…

検索と移動関係： [alt+x] コマンドパレット、先頭'>'を消して"go to file"、 '@', '#', ':' を先頭に打つと、ファイルのシンボル、ワークスペースのシンボル、行数と桁数などの検索・移動ができる。スーパー・キーボードインターフェイス。 [ctrl+x ctrl+x]…

[f6] を押してタブフラップにフォーカスを移動する。 [tab] と [shift+tab] でタブを移動できる。 [enter] でタブを表示できる。 グループタブフラップにフォーカスがある状態で、[space] OR [enter] でグループを開閉できる。 [ctrl+arrow] でタブ位置を移…

メニューバー兼タイトルバー 上境界 アクティビティバー 左境界 ステータスバー 下境界 プライマリ・サイドバー 左 セカンダリ・サイドバー 右 パネル 下 （パネルの上部はパネルバー） エディターグループ エディタータブ タブごとのエディターエリア 各種…

twitterで： 2022-12-29 Windowsのコンソールアプリケーションは、windows terminal 上で実行されるように変更されたようだ。 コンソールウィンドウが統合されるのは別にいいのだが、ショートカットキーの挙動が変わって困っている。 今までフォーカス切り替…

デフォルトでは、キー[Ctrl-P]は QuickOpen（"go to file"）に割り当てられている。 EmacsBindingsが、QuickOpenを[Ctrl-X, Ctrl-F]に再束縛している。 [Ctrl-F]は、AutoHotKeyにより[→]に変換される。 したがって、キーボードからQuickOpen（"go to file"）…

まだ未整理だが、とりあえず備忘メモ。まず、対称性がある操作達。 無制限タプル構成 無制限コタプル構成（無制限タプル構成の双対） 有限タプル構成（無制限から制限） 有限コプル構成（有限タプル構成の双対） 依存カリー化 カリー化（依存カリー化の非依…

フォワード・リーズニング用に、ステージと同じコンビネータ・コマンドがある： 連言導入用コンビネータ： 既存のn個の証明から連言への証明を作る。 全称導入用コンビネータ： 既存のパラメータ付き証明から全称への証明を作る。 選言除去用コンビネータ： …

Leanでは 対応する閉じ括弧をハイライトするとか、"go to bracket"コマンド（[ctrl+shift+\]）がうまく動かない。なにしろ、begin/endの括弧を使わない方針だから。

ステージ内に居るシーケントは： 事実シーケント 質問シーケント〈問題シーケント | ゴール〉 やること： 事実シーケントの構成（味方を増強する） 質問シーケントの分解（敵を衰弱させる／消滅させる） ステージの種類は： 連言導入用ステージ（連言成分〈…

shift+? ヘルプ表示 f 全画面トグル t シアターモード・トグル i ミニプレイヤー・トグル space 再生・一時停止 j 10秒巻き戻し k 停止／再生トグル l(small L) 10秒早送り vi風 H←, J↓, K↑, L→ Youtube H J← K■ L→ shift+ shift+> 再生速度早く 数字キー 全…

次のようなキーワードの名前スコープと使い方について考える。 def, theorem let in, let return providing return where section module package 名前とスコープに関する概念： イミュータブル名〈プログラム定数〉とミュータブル名〈プログラム変数〉 公理…

$`f`$ のフルカリー化を $`f^\wedge`$ として次が意味的には同じであること。 $`f(a_1, \cdots, a_n)`$ $`f^\wedge(a_1) \cdots (a_n)`$ $`(\cdots(f^\wedge\triangleleft a_1) \cdots )\triangleleft a_n`$ $`f^\wedge\: a_1\: \cdots\: a_n`$ これをストリ…

https://www.cs.vu.nl/~jbe248/lv2017/10x4.pdf より：the {type checking | proof verification} problem Γ |-? t:A the {typability | type {synthesis | inference}} problem Γ |- t:? the {{type | proposition} inhabitation | proposition provability…

コンテキストと指標は、構文的には区別できないのだが、次の違いがある。 指標はインスティチューション的な意味での指標である。 指標のあいだの射は指標射で、モデル圏のあいだのリダクト関手を定義する。 コンテキストは、固定した指標に対する構文的圏の…