michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(library/extras/latex/lstlean.text): update lists for syntax highlighting

Browse source
This commit is contained in:
Jeremy Avigad 2015-12-21 15:54:00 -05:00
parent 8ccafc4267
commit 8d50405e68
1 changed files with 26 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

49
extras/latex/lstlean.tex
View file

@ -9,49 +9,52 @@ mathescape=true,
% Comments may or not include Latex commands % Comments may or not include Latex commands
texcl=false, texcl=false,
% keywords % keywords, list taken from lean-syntax.el
morekeywords=[1]{ morekeywords=[1]{
import, prelude, tactic_hint, protected, private, definition, renaming, import, prelude, tactic_hint, protected, private, noncomputable, definition, renaming,
hiding, exposing, parameter, parameters, begin, begin+, proof, qed, conjecture, constant, constants, hiding, exposing, parameter, parameters, begin, begin+, proof, qed, conjecture, constant, constants,
hypothesis, lemma, corollary, variable, variables, premise, premises, hypothesis, lemma, corollary, variable, variables, premise, premises, theory,
print, theorem, example, abbreviation, print, theorem, proposition, example, abbreviation, abstract,
open, as, export, axiom, axioms, inductive, with, structure, record, universe, universes, open, as, export, override, axiom, axioms, inductive, with, structure, record, universe, universes,
alias, help, environment, options, precedence, reserve, alias, help, environment, options, precedence, reserve,
match, infix, infixl, infixr, notation, postfix, prefix, match, infix, infixl, infixr, notation, postfix, prefix,
tactic_infix, tactic_infixl, tactic_infixr, tactic_notation, tactic_postfix, tactic_prefix, tactic_infix, tactic_infixl, tactic_infixr, tactic_notation, tactic_postfix, tactic_prefix,
eval, check, coercion, end, reveal, eval, check, coercion, end, reveal, this, suppose,
using, namespace, section, fields, find_decl, using, namespace, section, fields, find_decl,
attribute, local, set_option, add_rewrite, extends, include, omit, classes, attribute, local, set_option, extends, include, omit, classes,
instances, coercions, metaclasses, raw, migrate, replacing, instances, coercions, metaclasses, raw, migrate, replacing,
calc, have, obtains, show, by, by+, in, at, let, forall, fun, calc, have, obtains, show, suffices, by, by+, in, at, let, forall, Pi, fun,
exists, if, dif, then, else, assume, assert, take, obtain, from exists, if, dif, then, else, assume, assert, take,
obtain, from, aliases
}, },
% Sorts % Sorts
morekeywords=[2]{Type, Prop}, morekeywords=[2]{Type, Prop},
% tactics % tactics, list taken from lean-syntax.el
morekeywords=[3]{ morekeywords=[3]{
Cond, or_else, then, try, when, assumption, eassumption, rapply, Cond, or_else, then, try, when, assumption, eassumption, rapply,
apply, fapply, eapply, rename, intro, intros, all_goals, fold, apply, fapply, eapply, rename, intro, intros, all_goals, fold, focus, focus_at,
generalize, generalizes, clear, clears, revert, reverts, back, beta, done, exact, rexact, generalize, generalizes, clear, clears, revert, reverts, back, beta, done, exact, rexact,
refine, repeat, whnf, rotate, rotate_left, rotate_right, inversion, cases, rewrite, esimp, refine, repeat, whnf, rotate, rotate_left, rotate_right, inversion, cases, rewrite,
unfold, change, check_expr, contradiction, exfalso, split, existsi, constructor, left, right, xrewrite, krewrite, blast, simp, esimp, unfold, change, check_expr, contradiction,
injection, congruence, reflexivity, symmetry, transitivity, state, induction, induction_using exfalso, split, existsi, constructor, fconstructor, left, right, injection, congruence, reflexivity,
symmetry, transitivity, state, induction, induction_using, fail, append,
substvars, now, with_options, with_attributes, with_attrs, note
}, },
% attributes % modifiers, taken from lean-syntax.el
% note: 'otherkeywords' is needed because these use a different symbol. % note: 'otherkeywords' is needed because these use a different symbol.
% this command doesn't allow us to specify a number -- they are put with [1] % this command doesn't allow us to specify a number -- they are put with [1]
otherkeywords={ otherkeywords={
[persistent], [notation], [visible], [instance], [class], [parsing-only], [persistent], [notation], [visible], [instance], [trans_instance],
[coercion], [unfold-f], [constructor], [reducible], [class], [parsing-only], [coercion], [unfold_full], [constructor],
[irreducible], [semireducible], [quasireducible], [wf], [reducible], [irreducible], [semireducible], [quasireducible], [wf],
[whnf], [multiple-instances], [none], [whnf], [multiple_instances], [none], [decls], [declarations],
[decls], [declarations], [coercions], [classes], [coercions], [classes], [symm], [subst], [refl], [trans], [simp], [simps], [congr],
[symm], [subst], [refl], [trans], [recursor], [forward], [no_pattern], [notations], [abbreviations], [begin_end_hints], [tactic_hints],
[notations], [abbreviations], [begin-end-hints], [tactic-hints], [reduce_hints], [unfold_hints], [aliases], [eqv], [intro], [intro!], [elim],
[reduce-hints], [unfold-hints], [aliases], [eqv], [localrefinfo] [localrefinfo] [recursor]
}, },
% Various symbols % Various symbols