mizar.js 825 B

123456789101112131415161718
  1. module.exports = function(hljs) {
  2. return {
  3. keywords:
  4. 'environ vocabularies notations constructors definitions ' +
  5. 'registrations theorems schemes requirements begin end definition ' +
  6. 'registration cluster existence pred func defpred deffunc theorem ' +
  7. 'proof let take assume then thus hence ex for st holds consider ' +
  8. 'reconsider such that and in provided of as from be being by means ' +
  9. 'equals implies iff redefine define now not or attr is mode ' +
  10. 'suppose per cases set thesis contradiction scheme reserve struct ' +
  11. 'correctness compatibility coherence symmetry assymetry ' +
  12. 'reflexivity irreflexivity connectedness uniqueness commutativity ' +
  13. 'idempotence involutiveness projectivity',
  14. contains: [
  15. hljs.COMMENT('::', '$')
  16. ]
  17. };
  18. };