   (cl-second check-cmd))
 (defun lean-cmd-check-get-line (check-cmd)
   (cl-third check-cmd))
+(defun lean-cmd-set-get-option-name (set-cmd)
+  (cl-second set-cmd))
+(defun lean-cmd-set-get-option-value (set-cmd)
+  (cl-third set-cmd))
+(defun lean-cmd-eval-get-lean-cmd (eval-cmd)
+  (cl-second eval-cmd))
 
 ;; -- Test
 (cl-assert (string= (lean-cmd-load-get-file-name (lean-cmd-load "nat.lean"))

(defun lean-cmd-check (line-number line)
  "Check whether the text editor and Lean have the 'same view' of the current file + modifications"
  `(CHECK ,line-number ,line))

;; Type
;; ====

(cl-assert (string= (lean-cmd-check-get-line
                     (lean-cmd-replace 34 "∀ (n : nat), ne (succ n) zero"))
                    "∀ (n : nat), ne (succ n) zero"))
(cl-assert (string= (lean-cmd-set-get-option-name
                     (lean-cmd-set "pp.implicit" "true"))
                    "pp.implicit"))
(cl-assert (string= (lean-cmd-set-get-option-value
                     (lean-cmd-set "pp.implicit" "true"))
                    "true"))
(cl-assert (string= (lean-cmd-eval-get-lean-cmd
                     (lean-cmd-eval "print 3"))
                    "print 3"))

;; to-string functions
;; ===================
