period . placeholder _ colon : semicolon ; dcolon :: lparen ( rparen ) llevel_curly .{ lcurly { rcurly } ldcurly ⦃ rdcurly ⦄ lcurlybar {| rcurlybar |} lbracket [ rbracket ] langle ⟨ rangle ⟩ triangle ▸ caret ^ up ↑ down question ? question_lp ?( bang ! slash / plus + star * turnstile ⊢ explicit @ max max imax imax cup \u2294 import import prelude prelude show show have have assert assert assume assume 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 rewrite rewrite proof proof qed qed begin begin begin_plus begin+ end end private private 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] 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