Atomコードリーディングメモ
script/build
起動したらsrc/window-bootstrap.coffeeが起動時間のログを出してるので、そいつをgrepすると/src/broweser/atom-application.coffee が引っかかる。
src/broweser/atom-application.coffee は、 src/browser/main.coffee に呼ばれている
theory cantor | |
imports Main | |
begin | |
definition map :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" where | |
"map A B = {f. \<forall>a\<in>A. f a \<in> B}" | |
definition surj where | |
"surj A B f = (f \<in> map A B \<and> (\<forall>b\<in>B. \<exists>a\<in>A. f a = b))" |
definition (in Category) Iso where | |
"Iso f g ≡ (f ∘ g ≈ id (dom g)) & (g ∘ f ≈ id (dom f))" | |
definition Iso_on_objects ("_ [ _ ≅ _ ]" 40) where | |
"𝒞 [ A ≅ B ] ≡ (∃f∈Arr 𝒞. ∃g∈Arr 𝒞. f ∈ Hom[𝒞][A,B] & g ∈ Hom[𝒞][B,A] & Category.Iso 𝒞 f g)" | |
record 'c setmap = | |
setdom :: "'c set" | |
setcod :: "'c set" | |
setfunction :: "'c ⇒ 'c" |