lean / keywords
113 entries at this level
- 加_decl_doc add_decl_doc
- 全部 all
- 並且 and
- 數組 Array
- 斷言 assert
- 斷言_非_exists assert_not_exists
- 斷言_非_imported assert_not_imported
- 異步 async
- 屬性 attribute
- 行為 behavior
- 布爾 Bool
- 兩個都 both
- 中斷 break
- 按 by
- 捕 catch
- 字符 char
- 字符 Char
- 類 class
- 比較 compare
- 繼續 continue
- dbg_痕跡 dbg_trace
- declare_syntax_貓 declare_syntax_cat
- decreasing_按 decreasing_by
- 默認_實例 default_instance
- deprecated_模塊 deprecated_module
- 做 do
- docs_至_verso docs_to_verso
- elab_規矩 elab_rules
- 否則 else
- 結束 end
- 結束_本地_作用域 end_local_scope
- 等於 Eq
- 錯誤 error
- 例子 example
- 預咗啦 expected
- 導出 export
- 揭露 expose
- 繼承 extends
- 失敗 failure
- 假 false
- 終 finally
- 浮點數 Float
- 對於 for
- 從 from
- 樂趣 fun
- 索引 get
- 映射 HashMap
- 集合 HashSet
- 有 have
- 如果 if
- 導入 import
- 在 in
- 包括 include
- 實例 instance
- 整數 Int
- 無效 invalid
- 長度 length
- let_延遲咗 let_delayed
- let_樂趣 let_fun
- 列表 List
- 本地 local
- macro_規矩 macro_rules
- 匹配 match
- 匹配_expr match_expr
- 最大 max
- 最小 min
- 模 mod
- 模塊 module
- 互相嘅 mutual
- 名稱 name
- 否_索引 no_index
- 空 none
- 打開 open
- 或 or
- 私有 private
- 元組 Prod
- 公開 public
- 建議_spelling recommended_spelling
- 註冊_錯誤_解釋 register_error_explanation
- 註冊_parser_alias register_parser_alias
- 註冊_tactic_標記 register_tactic_tag
- 重複 repeat
- 返回 return
- 部分 section
- 設置_選擇 set_option
- show_期限_elab show_term_elab
- 從 since
- 長度 size
- 跳過 skip
- 對唔住 sorry
- 字串 String
- 結構 structure
- 符號 symbol
- tactic_延伸 tactic_extension
- tactic_名稱 tactic_name
- tactic_標記 tactic_tag
- 任務 Task
- 期限 term
- termination_按 termination_by
- 然後 then
- 拋 throw
- 真 true
- 試 try
- 字節 UInt8
- 虛 Unit
- 除非 unless
- 直到 until
- 有效 valid
- 變量 variable
- 邊度 where
- 當 while
- 與 with
- 與_弱_namespace with_weak_namespace