core.lean 内の定義： @[inline] def band : bool → bool → bool | ff _ := ff | tt ff := ff | tt tt := tt notation x && y := band x y[inline] というアトリビュートがある。その場で展開されるのかな？アンダスコアは無名変数〈匿名変数〉で、パターン…

ハブは： https://leanprover.github.io/documentation/ → Lean4のマニュアル作業中、現状は参考になっても参照はしないだろう。 → Learning Lean すぐ下 https://leanprover-community.github.io/learn.html https://leanprover.github.io/publications/ ht…

検索文字列"from:m_hiyama leanprover"で、Twitter検索をすればいい。 https​:​//twitter.com/search?q=from%3Am_hiyama%20leanprover&src=typed_query

Haskellで「アクション」という言い方があるが、どうもクライスリ射のことらしい。IOアクションは、IOモナドのクライスリ射という具合に。となると、Leanのtacticモナドのクライスリ射はtacticアクションとなるが、「tacticアクション＝タクティク」だから、…

import system.io #eval io.print_ln "hello world"try it!

privateな名前は、名前空間の内部しか使用できない。外部からのアクセスが禁止される。protectedな名前は、アクセスは可能だが、openして外部にばらまくことができない。 private -- 外部からのアクセスは不可能。 protected -- 接頭辞付きでならアクセス可…

以下は、$USERPROFILE/.elan/toolchains/stable/bin/leanpkg.bat @ECHO OFF SET LEANDIR=%~dp0%../ SET LIBDIR=%LEANDIR%\lib\lean IF NOT EXIST "%LIBDIR%" SET LIBDIR=%LEANDIR% SET LEAN_PATH=%LIBDIR%\library;%LIBDIR%\leanpkg SET PATH=%LEANDIR%\bin;…

inductive foo : Type := | bar : foo | baz : foo と書きたくなるが、:= は要らない。なぜなのだろう？[追記]match/with/end の省略と同じみたいだ。[/追記]

section funcomp variables {X Y Z:Type} def comp (f:X → Y) (g:Y → Z) :X → Z := λ x:X, g (f x) end funcomp #check comp infix `;` := comp constants A B C D:Type constants (f:A → B) (g:B → C) (h:C → D) #check comp #check comp f g #check f;g;h …

https://leanprover-community.github.io/install/windows.html MicrosoftリサーチはMicrosoft社の研究部門ではなく、 マイクロソフトリサーチ ： 完全に独立した研究機関であり、そこで行われる研究内容については、たとえマイクロソフト本社の首脳陣であっ…

整理はされてないが列挙： ガッカリ・ウンザリするところがない。 しがらみの無さ 単一言語 構文の一貫性 → 予測可能性 将来性・期待感 歴史上初の汎用プログラミング言語へ Unicode文字キーワード → 可読性、視認性 薄いシンタックスシュガー（甘さ控えめ）…

CTRL+CLICK でリンクをたどって。 さくら（sakura）とGMO - (保存用) 檜山正幸のキマイラ飼育記 メモ編 GMO VPSの契約管理 - (保存用) 檜山正幸のキマイラ飼育記 メモ編 再度ドメイン設定 - (保存用) 檜山正幸のキマイラ飼育記 メモ編 GMO VPSの設定 - (保存…