diff --git a/src/emacs/lean-info.el b/src/emacs/lean-info.el
index b6e845a23..d8e975488 100644
--- a/src/emacs/lean-info.el
+++ b/src/emacs/lean-info.el
@@ -122,6 +122,47 @@
                     "not (eq one (succ m'))\n→ decidable (eq zero (succ m'))"
                     "not (eq two (succ m'))\n→ decidable (eq zero (succ m'))")))
 
+;; Synth Information
+;; ----------------
+(defun lean-synth-type (synth)
+  (cl-first synth))
+(defun lean-synth-p (synth)
+  (equal (lean-synth-type synth) 'SYNTH))
+(defun lean-synth-pos (synth)
+  (cl-second synth))
+(defun lean-synth-str-p (str)
+  (string-prefix-p "-- SYNTH|" str))
+(defun lean-synth-str-seq-p (seq)
+  (lean-synth-str-p (cl-first seq)))
+(defun lean-synth-parse-header (str)
+  (let ((items (split-string str "|")))
+    (list (string-to-number (cl-second items))
+          (string-to-number (cl-third items)))))
+(defun lean-synth-parse (seq)
+  (let ((header (lean-synth-parse-header (car seq)))
+        (body (cdr seq)))
+    `(SYNTH ,header ,body)))
+(defun lean-synth-body (synth)
+  (cl-third synth))
+(defun lean-synth-body-str (synth)
+  (lean-string-join (lean-synth-body synth) "\n"))
+
+;; -- Test
+(cl-assert (lean-synth-str-p "-- SYNTH|121|2"))
+(cl-assert (equal (lean-synth-parse-header "-- SYNTH|121|2")
+                  '(121 2)))
+(cl-assert (lean-synth-str-seq-p '("-- SYNTH|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
+(cl-assert (equal (lean-synth-parse '("-- SYNTH|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))"))
+                  '(SYNTH
+                    (121 2)
+                    ("not (eq zero (succ m'))"
+                     "→ decidable (eq zero (succ m'))"))))
+(cl-assert (equal
+            (lean-synth-pos
+             (lean-synth-parse '("-- SYNTH|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
+            '(121 2)))
+
+
 ;; Basic
 ;; -----
 (defun lean-info-type (info)
@@ -133,7 +174,8 @@
 (defun lean-info-pos (info)
   (cl-case (lean-info-type info)
     (TYPE     (lean-typeinfo-pos info))
-    (OVERLOAD (lean-overload-pos info))))
+    (OVERLOAD (lean-overload-pos info))
+    (SYNTH    (lean-synth-pos    info))))
 (defun lean-info-line-number (info)
   (cl-first (lean-info-pos info)))
 (defun lean-info-column (info)
@@ -182,7 +224,8 @@ Use \"-- ACK\" as a delim and stop processing when it encounters \"-- ENDINFO\""
              when string-seq
              collect (cond
                       ((lean-typeinfo-str-seq-p string-seq) (lean-typeinfo-parse string-seq))
-                      ((lean-overload-str-seq-p string-seq) (lean-overload-parse string-seq))))))
+                      ((lean-overload-str-seq-p string-seq) (lean-overload-parse string-seq))
+                      ((lean-synth-str-seq-p    string-seq) (lean-synth-parse string-seq))))))
 
 ;; -- test
 (cl-assert
diff --git a/src/emacs/lean-type.el b/src/emacs/lean-type.el
index fd12023ce..b87e6692d 100644
--- a/src/emacs/lean-type.el
+++ b/src/emacs/lean-type.el
@@ -60,15 +60,19 @@ The return valus has the form of '([symbol-string] [start-pos])"
                                             'lean-typeinfo-p)))
           (overload
            (cl-first (lean-filter-info-list info-list-at-pos
-                                            'lean-overload-p))))
-    (list typeinfo overload)))
+                                            'lean-overload-p)))
+          (synth
+           (cl-first (lean-filter-info-list info-list-at-pos
+                                            'lean-synth-p))))
+    (list typeinfo overload synth)))
 
-(defun lean-print-info (typeinfo overload sym-name)
+(defun lean-print-info (typeinfo overload synth sym-name)
   "Given typeinfo, overload, and sym-name, print out information."
   (when typeinfo
     (let* ((overload-names  (lean-overload-names overload))
            (overload-name   (cl-first overload-names))
-           (name            (or overload-name sym-name))
+           (synth-value     (when synth (lean-synth-body-str synth)))
+           (name            (or synth-value overload-name sym-name))
            (type-str        (lean-typeinfo-body-str typeinfo))
            (type-output-str
             (format "%s : %s"
@@ -80,7 +84,7 @@ The return valus has the form of '([symbol-string] [start-pos])"
                       (propertize "overloaded" 'face 'font-lock-keyword-face)
                       (lean-string-join (cdr overload-names) ", "))))
            (output-str (concat type-output-str overload-output-str)))
-      (message output-str))))
+      (message "%s" output-str))))
 
 (defun lean-eldoc-documentation-function ()
   "Show information of lean expression at point if any"
@@ -93,9 +97,9 @@ The return valus has the form of '([symbol-string] [start-pos])"
          (start-pos (cl-second sym-info))
          (start-column (- column (- (point) start-pos)))
          typeinfo overload)
-    (cl-multiple-value-setq (typeinfo overload)
+    (cl-multiple-value-setq (typeinfo overload synth)
       (lean-extract-info-at-pos file-name line-number column start-pos))
-    (lean-print-info typeinfo overload sym-name)))
+    (lean-print-info typeinfo overload synth sym-name)))
 
 (defun lean-before-change-function (beg end)
   "Function attached to before-change-functions hook.