2020-12-14から1日間の記事一覧
同義語 構造体=レコード。これは便利だ。構造体型は帰納的型だから、データは帰納的データ。帰納的データ(=帰納的型のデータ)は定義によりリテラル表示を持つ。リテラル表示のコンビニエンスとしていくつかの記法がサポートされている。 名前付きレコー…
システムの健全性 システムの十全性 システムの完全性 モデルと文の充足〈満足〉関係 文の充足可能性
論理 型 命題 型 命題Pの証明 型Tの式 証明内の根拠 式内の定数名 含意 関数型 前件 域型〈ソース型〉 後件 余域型〈ターゲット型〉 シーケント プロファイル 仮定 コンテキスト 結論 ターゲット 証明 証拠式 定理記述 オブジェクト定義 公理記述 定数宣言 …
論理: 矢印 左 右 含意〈implication〉 ⊃ 前件〈antecedent〉 後件〈succedent〉 伴意〈entailment〉→ 仮定〈assumption〉 結論〈conclusion〉 証明可能性〈be-provable〉判断 仮定〈assumption〉 結論〈conclusion〉 妥当性〈validity〉判断 モデル〈model…
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;…