lean / keywords
118 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
- ཆོག_expr let_expr
- ཆོག_དགའ་སྤྲོ let_fun
- ཆོག_tmp let_tmp
- རིམ་ཐོ 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
- byte UInt8
- སྟོང་པ Unit
- མི་ཤེས unknown
- མ་གཏོགས unless
- བར་དུ until
- ཚུལ་མཐུན valid
- འགྱུར་ཚད variable
- ག་པར where
- བར while
- མཉམ་དུ with
- མཉམ་དུ_ཞན་པོ_namespace with_weak_namespace