diff --git a/src/emacs/lean-company.el b/src/emacs/lean-company.el index d3858d07bb..09e4fc89fd 100644 --- a/src/emacs/lean-company.el +++ b/src/emacs/lean-company.el @@ -192,7 +192,9 @@ ;; ----- (defun company-lean--need-autocomplete () (interactive) - (cond ((looking-back + (cond ((looking-back (rx "print" (+ white) "definition" (+ white) (* (not white)))) + t) + ((looking-back (rx (or "theorem" "definition" "lemma" "axiom" "parameter" "variable" "hypothesis" "conjecture" "corollary" "open")