tips
def f5 (n : Nat) : Nat := by cases n exact 3 -- zero case exact 7 -- succ case #eval f5 0 --> 3 #eval f5 1 --> 7 example : f5 0 = 3 := rfl -- by も要らない！？ example : f5 5 = 7 := rfl example : f5 2 = 7 := by exact Eq.refl 7
() はUnit型の唯一の要素。 (3) は 3 のこと。型 Nat (3, 4) はペア型 Nat×Nat (3, 4, 5) は Nat×Nat×Nat (3, 4, 5) = (3, (4, 5)) 右結合的な二項演算子 .1 は .fst、.2 は .snd ⟨カンマ区切り項目並び⟩ は構造体リテラルの略記。フィールド名を省略できる…
inductiveな型と同名の名前空間を定義して、そのなかにstuffを入れる。以下は実例： structure Parser.Category namespace Parser.Category /- ... ... -/ end Parser.CategoryLeanのキモのひとつは、名前空間／シンボル空間の構造と相互作用を理解すること。
曲線は入れてない。 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だと何も…
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>
戻り値にステータスを返したいなら 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 で指定。ビュー…
戻り値にステータスを返したいなら 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}!"改行は普通に入れられる。エスケープの必要はない。
入力法は、コマンド "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%パーセント記号は相変わらず意味不明。
({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…
[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"）…
shift+? ヘルプ表示 f 全画面トグル t シアターモード・トグル i ミニプレイヤー・トグル space 再生・一時停止 j 10秒巻き戻し k 停止／再生トグル l(small L) 10秒早送り vi風 H←, J↓, K↑, L→ Youtube H J← K■ L→ shift+ shift+> 再生速度早く 数字キー 全…
※ 2023-01-17に書いたけど投稿忘れ。演算子の優先度 - (新) 檜山正幸のキマイラ飼育記 メモ編 の続きLeanの場合、まだ調整は必要かも知れない： PrefixSuffixPrecidence 1024 = max ArgumentPrecidence 1023 = arg CompositionPrecedence 90 ($`\circ`$) Exp…
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 ..\..\…
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
例： attribute [local simp] Nat.add_assoc Nat.add_comm Nat.add_left_commルート名前空間は無名だが、_root_ という名前で参照できる。
npmのpackage-lock.json相当が、Lakeマニフェストファイル。lean_packages/manifes.json と lake-manifest.json がある。注意すべきはマニフェストファイル自体のバージョンで、JSONファイルのトップレベルフィールドとしてバージョン番号が記入されている。…
名前付き引数〈named arguments〉と引数省略時値〈default value〉の指定 def mySub (left right :Nat) : Nat := left - right #check mySub #eval mySub (right := 3) (left := 5) --> 2 def mySub' (left :Nat) (right:Nat := 1) : Nat := left - right #c…
apply は backward apply〈deapply | reverse apply〉の意味。だいぶ困る。 複数のゴールは左〈上〉から順に攻撃する。ツリー辿りは深さ優先再帰かな。 ゴールの固有名はないが、left, right のcaseラベルは付く。並びの順番でも参照できる。 ツリーが構成さ…
#eval で値〈要素〉を表示するには、型が型クラス Repr の型インスタンスでなくてはならない。文字列化できるためには、型が型クラス ToStrng の型インスタンスでなくてはならない。
def f1 : Nat → Nat → Nat := by exact (fun (n m: Nat) => n + m) #check f1 def f2 (n: Nat): Nat → Nat := by intro m exact n + m #check f2 def f3 (n m: Nat): Nat := by exact n + m #check f3
Leanサーバーは、環境変数LEAN_PATHなしでも、./lake-packages/some-package/build/lib/ の下を見ることは知っているようだ。import Foo は ./lake-packages/some-package/build/lib/Foo.olean をロードする。Lean.findOLean が役に立つ。 #eval Lean.findOL…
cat lean-toolchain elan toolchain list elan show だとダウンロードが始まる cat lakefile.lean cat .git/HEAD デタッチされているか？ git branch git rev-parse カレントブランチ git tag git rev-parse $(git tag | tail -1) git log --oneline git rev…
