2020-12-14から1日間の記事一覧

構造体/レコード型

同義語 構造体=レコード。これは便利だ。構造体型は帰納的型だから、データは帰納的データ。帰納的データ(=帰納的型のデータ)は定義によりリテラル表示を持つ。リテラル表示のコンビニエンスとしていくつかの記法がサポートされている。 名前付きレコー…

メタな用語

システムの健全性 システムの十全性 システムの完全性 モデルと文の充足〈満足〉関係 文の充足可能性

論理用語と型用語

論理 型 命題 型 命題Pの証明 型Tの式 証明内の根拠 式内の定数名 含意 関数型 前件 域型〈ソース型〉 後件 余域型〈ターゲット型〉 シーケント プロファイル 仮定 コンテキスト 結論 ターゲット 証明 証拠式 定理記述 オブジェクト定義 公理記述 定数宣言 …

論理用語

論理: 矢印 左 右 含意〈implication〉 ⊃ 前件〈antecedent〉 後件〈succedent〉 伴意〈entailment〉→ 仮定〈assumption〉 結論〈conclusion〉 証明可能性〈be-provable〉判断 仮定〈assumption〉 結論〈conclusion〉 妥当性〈validity〉判断 モデル〈model…

case文の書き方など

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…

Twitterからの検索

検索文字列"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 def

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

Leanのファイル配置、環境変数など

以下は、$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;…