 ignored."
   `(REMOVE ,line-number))
 
-(defun lean-cmd-info (line-number)
+(defun lean-cmd-info (line-number &optional column-number)
   "Extracts typing information associated with line [line-number].
 
 Lean produces a possible empty sequence of entries terminated with '--ENDINFO'"
-  `(INFO ,line-number))
+  `(INFO ,line-number ,column-number))
 
 (defun lean-cmd-check (line-number line)
   "Check whether the text editor and Lean have the 'same view' of the current file + modifications"

                    (concat "REMOVE 42")))
(cl-assert (string= (lean-cmd-to-string (lean-cmd-info 42))
                    (concat "INFO 42")))
(cl-assert (string= (lean-cmd-to-string (lean-cmd-check 42 "∀ (n : nat), ne (succ n) zero"))
                    (concat "CHECK 42" "\n" "∀ (n : nat), ne (succ n) zero")))
(cl-assert (string= (lean-cmd-to-string (lean-cmd-findp 42 "iff_"))

  (cl-second remove-cmd))
(defun lean-cmd-info-get-line-number (info-cmd)
  (cl-second info-cmd))
(defun lean-cmd-info-get-column-number (info-cmd)
  (cl-third info-cmd))
(defun lean-cmd-check-get-line-number (check-cmd)
  (cl-second check-cmd))
(defun lean-cmd-check-get-line (check-cmd)
