Closed vbgl closed 2 months ago
It seems that the script $(HOMEEC)/scripts/srctx/keywords < src/ecLexer.mll print the following: bytac: assumption, by, done, exact, reflexivity, smt, solve dangerous: admit, admitted global: Pr, Self, Top, abbrev, abort, abstract, as, axiom, axiomatized, class, clone, const, declare, dump, end, exit, export, from, goal, hint, import, include, inductive, instance, lemma, local, locate, module, nosmt, notation, of, op, pred, print, proof, prover, qed, realize, remove, rename, require, search, section, theory, timeout, type, why3, with internal: debug, fail, pragma, time, undo prog: assert, async, ehoare, elif, else, equiv, exists, for, for, forall, fun, glob, hoare, if, in, is, islossless, let, match, match, phoare, proc, res, return, then, var, while tactic: algebra, alias, apply, auto, beta, byehoare, byequiv, byphoare, bypr, byupto, call, case, cbv, cfold, change, clear, congr, conseq, delta, eager, ecall, elim, eta, exfalso, exlim, fel, field, fieldeq, fission, fusion, gen, have, idtac, inline, interleave, iota, kill, left, logic, modpath, move, outline, pose, pr_bounded, progress, rcondf, rcondt, replace, rewrite, right, ring, ringeq, rnd, rndsem, rwnormal, seq, sim, simplify, skip, sp, split, splitwhile, subst, suff, swap, symmetry, transitivity, trivial, unroll, weakmem, wlog, wp, zeta tactical: do, expect, first, last, try
It seems that the script $(HOMEEC)/scripts/srctx/keywords < src/ecLexer.mll print the following: bytac: assumption, by, done, exact, reflexivity, smt, solve dangerous: admit, admitted global: Pr, Self, Top, abbrev, abort, abstract, as, axiom, axiomatized, class, clone, const, declare, dump, end, exit, export, from, goal, hint, import, include, inductive, instance, lemma, local, locate, module, nosmt, notation, of, op, pred, print, proof, prover, qed, realize, remove, rename, require, search, section, theory, timeout, type, why3, with internal: debug, fail, pragma, time, undo prog: assert, async, ehoare, elif, else, equiv, exists, for, for, forall, fun, glob, hoare, if, in, is, islossless, let, match, match, phoare, proc, res, return, then, var, while tactic: algebra, alias, apply, auto, beta, byehoare, byequiv, byphoare, bypr, byupto, call, case, cbv, cfold, change, clear, congr, conseq, delta, eager, ecall, elim, eta, exfalso, exlim, fel, field, fieldeq, fission, fusion, gen, have, idtac, inline, interleave, iota, kill, left, logic, modpath, move, outline, pose, pr_bounded, progress, rcondf, rcondt, replace, rewrite, right, ring, ringeq, rnd, rndsem, rwnormal, seq, sim, simplify, skip, sp, split, splitwhile, subst, suff, swap, symmetry, transitivity, trivial, unroll, weakmem, wlog, wp, zeta tactical: do, expect, first, last, try