一応できた。sectionは要らないみたい。 /-! 写像と関係 -/ namespace My /- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> -/ section Logic def MP {A B: Prop} (p:A → B) (a: A) : B := p a def Inst {X: Type} {P: X → Prop} (w: ∀(x: X), P x) (a : X) : P a := w a …

視点移動とフットワーク： 階層的宇宙のなかで自分がどこのいるのか？ 区別する／区別しない（同一視する／しない）、どちらの立場か？ 例： 引数なし関数名と定数名 名前が定数名〈固有名〉か変数名〈不定名〉か？ スコープに依存（事項）。 名前のスコープ…

/- 用語： スタブ： from https://e-words.jp/w/%E3%82%B9%E3%82%BF%E3%83%96.html スタブとは、切り株、半券、（何かが減ったり短くなった）残り、などの意味を持つ英単語。ITの分野では、本物が用意できないときに動作に支障が無いようにとりあえず置いて…

/-! 写像と関係 -/ namespace My /- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> -/ section Logic def MP {A B: Prop} (p:A → B) (a: A) : B := p a def Inst {X: Type} {P: X → Prop} (w: ∀(x: X), P x) (a : X) : P a := w a def Cut {A B C : Prop} (p: A → B) (q: …

最後の行がエラー。 /-- 記法クラス -/ class LE (X : Type) where le : X → X → Prop scoped infix:50 "≦" => LE.le #check LE section LE_Test variable -- セミローカルコンテキストの導入 (A: Type) [LE A] (a b:A) #check a≦b end LE_Test /-- 全順序集…