period       .
placeholder  _
colon        :
semicolon    ;
dcolon       ::
lparen       (
rparen       )
llevel_curly .{
lcurly       {
rcurly       }
ldcurly      ⦃
rdcurly      ⦄
lcurlybar    {|
rcurlybar    |}
lbracket     [
rbracket     ]
langle       ⟨
rangle       ⟩
triangle     ▸
caret        ^
up           ↑
down         <d
bar          |
comma        ,
add          +
sub          -
greater      >
question     ?
question_lp  ?(
bang         !
slash        /
plus         +
star         *
turnstile    ⊢
explicit     @
partial_explicit @@
max          max
imax         imax
cup          \u2294
import       import
prelude      prelude
show         show
have         have
assert       assert
assume       assume
suppose      suppose
take         take
fun          fun
match        match
ellipsis     ...
raw          raw
true         true
false        false
options      options
commands     commands
instances    instances
classes      classes
coercions    coercions
arrow        ->
declarations declarations
decls        decls
hiding       hiding
exposing     exposing
renaming     renaming
replacing    replacing
extends      extends
as           as
none         [none]
whnf         [whnf]
wf           [wf]
in           in
at           at
assign       :=
visible      [visible]
from         from
using        using
then         then
else         else
by           by
by_plus      by+
rewrite      rewrite
proof        proof
qed          qed
begin        begin
begin_plus   begin+
end          end
private      private
protected    protected
definition   definition
theorem      theorem
abbreviation abbreviation
axiom        axiom
axioms       axioms
constant     constant
constants    constants
variable     variable
variables    variables
instance     [instance]
trans_inst   [trans_instance]
priority     [priority
unfold       [unfold
unfold_full  [unfold_full]
unfold_hints_bracket [unfold_hints]
unfold_hints unfold_hints
constructor  [constructor]
coercion     [coercion]
reducible    [reducible]
quasireducible [quasireducible]
semireducible [semireducible]
irreducible  [irreducible]
parsing_only [parsing_only]
symm         [symm]
trans        [trans]
refl         [refl]
subst        [subst]
simp_attr    [simp]
congr_attr   [congr]
backward_attr [backward]
recursor     [recursor
attribute    attribute
with         with
class        [class]
multiple_instances [multiple_instances]
prev         prev
scoped       scoped
foldr        foldr
foldl        foldl
binder       binder
binders      binders
precedence   precedence
infix        infix
infixl       infixl
infixr       infixr
postfix      postfix
prefix       prefix
notation     notation
tactic_infix tactic_infix
tactic_infixl tactic_infixl
tactic_infixr tactic_infixr
tactic_postfix tactic_postfix
tactic_prefix tactic_prefix
tactic_notation tactic_notation
call         call
calc         calc
obtain       obtain
persistent   [persistent]
root         _root_
fields       fields
trust        trust
metaclasses  metaclasses
inductive    inductive
this         this
noncomputable noncomputable
theory       theory
