diff --git a/docs/chatgpt_knowledge_doc.txt b/docs/chatgpt_knowledge_doc.txt
index 2ba9cfbc3ea..9c63f5102bb 100755
--- a/docs/chatgpt_knowledge_doc.txt
+++ b/docs/chatgpt_knowledge_doc.txt
@@ -129,18 +129,6 @@ This Markdown content is ready to be uploaded to your fine-tuner!
 (= (if-unify-or-empty $a $b) (empty))
 
 
-;; Public MeTTa
-(@doc unify
-  (@desc "Like Match but allows any sort of container for the first argument. (Match only allows MeTTa spaces.)")
-  (@params (
-	(@param "The collection or space to match")
-	(@param "Second atom to unify with")
-	(@param "Result if two atoms unified successfully")
-	(@param "Result otherwise")))
-  (@return "Third argument when found or forth one otherwise"))
-(: unify (-> Atom Atom Atom Atom Atom))
-;; Implemented from Interpreters
-
 ;; Public MeTTa
 (@doc cons-atom
   (@desc "Constructs an expression using two arguments")
@@ -180,8 +168,8 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "Expression in form (Atom Binding)")))
   (@return "Non-deterministic list of Atoms"))
 ;; superpose-bind because `superpose` doesnt guarentee shared bindings
-(: superpose-bind (-> Atom Atom)) ; We specialize them but leaving the old defs in case
 (: superpose-bind (-> Expression Atom))
+(: superpose-bind (-> Atom Atom)) ; We specialize them but leaving the old defs in case
 ;; Implemented from Interpreters
 
 ; Helper Minimal Metta?
@@ -287,7 +275,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "Tuple of pairs mapping condition patterns to results")))
   (@return "Result which corresponds to the pattern which is matched with the passed atom first"))
 
-;; Dumb MeTTaLog unwill we implent it
+;; Dumb MeTTaLog? will we implement it?
 (: switch (-> Atom Atom Atom))
 (= (switch $atom $list) (case (eval $atom) $list))
 
@@ -349,8 +337,9 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "Type to cast atom to")
     (@param "Context atomspace")))
   (@return "Atom if casting is successful, (Error ... BadType) otherwise"))
+(: type-cast (-> Atom Atom Atom Atom))
 ;; This impl is old and maybe not sufficiant?
-(= (type-cast $atom $type $space)
+(ALT= (type-cast $atom $type $space)
   (function (chain (eval (get-metatype $atom)) $meta
     (eval (if-equal $type $meta
       (return $atom)
@@ -370,6 +359,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "Atom to be returned if types can be unified")
     (@param "Atom to be returned if types cannot be unified")))
   (@return "Third or fourth argument"))
+(: match-types (-> Atom Atom Atom Atom Atom))
 (= (match-types $type1 $type2 $then $else)
   (function (eval (if-equal $type1 %Undefined%
     (return $then)
@@ -792,9 +782,11 @@ This Markdown content is ready to be uploaded to your fine-tuner!
   (@params (
     (@param "Anything")))
   (@return "Unit atom"))
+(: nop (-> Atom (->)))
 ;; Implemented from Interpreters
-(= (nop) ())
-(= (nop $x) ())
+(ALT= (nop $x) ())
+(: nop (-> EmptyType))
+(ALT= (nop) ())
 
 ;; Public MeTTa
 (@doc empty
@@ -803,11 +795,13 @@ This Markdown content is ready to be uploaded to your fine-tuner!
   (@return "Nothing"))
 (: empty (-> %Undefined%))
 ;; Implemented from Interpreters
-(= (empty) (let a b never-happens))
+(ALT= (empty) (let a b never-happens))
+;For testing
+;(= (empty) Empty)
 
-(= (empty-rust1) (let a b never-happens))
+;(= (empty-rust1) (let a b never-happens))
 ; TODO: MINIMAL added for compatibility, remove after migration
-(= (empty-minimal) Empty)
+;(= (empty-minimal) Empty)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ; Documentation formatting functions
@@ -949,7 +943,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
 (: get-doc-function (-> Atom Type Atom))
 (= (get-doc-function $name $type)
   (let $top-space (mod-space! top)
-  (if-unify $top-space (@doc $name $desc (@params $params) $ret)
+  (unify $top-space (@doc $name $desc (@params $params) $ret)
     (let $type' (if (== $type %Undefined%) (undefined-doc-function-type $params) (cdr-atom $type))
     (let ($params' $ret') (get-doc-params $params $ret $type')
       (@doc-formal (@item $name) (@kind function) (@type $type) $desc (@params $params') $ret')))
@@ -999,9 +993,9 @@ This Markdown content is ready to be uploaded to your fine-tuner!
 (= (get-doc-atom $atom)
   (let $top-space (mod-space! top)
   (let $type (get-type-space $top-space $atom)
-    (if-unify $top-space (@doc $atom $desc)
+    (unify $top-space (@doc $atom $desc)
       (@doc-formal (@item $atom) (@kind atom) (@type $type) $desc)
-      (if-unify $top-space (@doc $atom $desc' (@params $params) $ret)
+      (unify $top-space (@doc $atom $desc' (@params $params) $ret)
         (get-doc-function $atom %Undefined%)
         (@doc-formal (@item $atom) (@kind atom) (@type $type) (@desc "No documentation")) )))))
 
@@ -1078,6 +1072,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "Atomspace to add atom into")
     (@param "Atom to add")))
   (@return "Unit atom"))
+(: add-atom (-> hyperon::space::DynSpace Atom (->)))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1085,6 +1080,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
   (@desc "Creates new Atomspace which could be used further in the program as a separate from &self Atomspace")
   (@params ())
   (@return "Reference to a new space"))
+(: new-space (-> hyperon::space::DynSpace Atom))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1094,6 +1090,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "Reference to the space from which the Atom needs to be removed")
     (@param "Atom to be removed")))
   (@return "Unit atom"))
+(: remove-atom (-> hyperon::space::DynSpace Atom (->)))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1102,6 +1099,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
   (@params (
     (@param "Reference to the space")))
   (@return "List of all atoms in the input space"))
+(get-atoms (-> hyperon::space::DynSpace Atom))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1110,6 +1108,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
   (@params (
     (@param "Atom to be wrapped")))
   (@return "Returns (State $value) where $value is an argument to a new-state"))
+(: new-state (-> $tnso (StateMonad $tnso)))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1119,6 +1118,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "State created by new-state function")
     (@param "Atom which will replace wrapped atom in the input state")))
   (@return "State with replaced wrapped atom"))
+(: change-state! (-> (StateMonad $tcso) $tcso (StateMonad $tcso)))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1127,6 +1127,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
   (@params (
     (@param "State")))
   (@return "Atom wrapped by state"))
+(: get-state (-> (StateMonad $tgso) $tgso))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1135,6 +1136,8 @@ This Markdown content is ready to be uploaded to your fine-tuner!
   (@params (
     (@param "Atom to get type for")))
   (@return "Type notation or %Undefined% if there is no type for input Atom"))
+(: get-type (-> Atom Atom))
+(: get-type (-> Atom Atom Atom))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1145,6 +1148,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "Atom to get type for")))
   (@return "Type notation or %Undefined% if there is no type for input Atom in provided atomspace"))
 ;; Implemented from Interpreters?
+(: get-type-space (-> Atom Atom Atom))
 (= (get-type-space $space $atom)
 	(get-type $atom $space))
 
@@ -1154,6 +1158,19 @@ This Markdown content is ready to be uploaded to your fine-tuner!
   (@params (
     (@param "Atom to get metatype for")))
   (@return "Metatype of input atom"))
+(: get-metatype (-> Atom Atom))
+;; Implemented from Interpreters  
+
+;; Public MeTTa
+(@doc unify
+  (@desc "Like Match but allows any sort of container for the first argument. (Match only allows MeTTa spaces.)")
+  (@params (
+	(@param "The collection or space to match")
+	(@param "Second atom to unify with")
+	(@param "Result if two atoms unified successfully")
+	(@param "Result otherwise")))
+  (@return "Third argument when found or forth one otherwise"))
+(: unify (-> Atom Atom Atom Atom Atom))
 ;; Implemented from Interpreters  
 
 ;; Public MeTTa
@@ -1166,8 +1183,8 @@ This Markdown content is ready to be uploaded to your fine-tuner!
   (@return "If match was successfull it outputs pattern (third argument) with filled variables (if any were present in pattern) using matched pattern (second argument). Nothing - otherwise"))
 (: match (-> Atom Atom Atom %Undefined%))
 ;; Implemented from Interpreters
-;(= (match $space $pattern $template)
-;  (if-unify $space $pattern $template Empty))
+;(ALT= (match $space $pattern $template)
+;  (unify $space $pattern $template Empty))
 
 ;; Public MeTTa
 (@doc register-module!
@@ -1175,6 +1192,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
   (@params (
     (@param "File system path")))
   (@return "Unit atom"))
+(: register-module! (-> Atom (->)))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1183,6 +1201,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
   (@params (
     (@param "Module name")))
   (@return "Space name"))
+(: mod-space! (-> Atom hyperon::space::DynSpace))
 ;; Implement from Interpreter!
 (= (mod-space! top) &self)
 (= (mod-space! corelib) &corelib)
@@ -1193,6 +1212,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
   (@desc "Prints all modules with their correspondent spaces")
   (@params ())
   (@return "Unit atom"))
+(: print-mods! (-> (->)))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1202,6 +1222,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "First expression")
     (@param "Second expression")))
   (@return "Unit atom if both expression after evaluation is equal, error - otherwise"))
+(: assertEqual (-> Atom Atom Atom))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1211,6 +1232,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "First expression (it will be evaluated)")
     (@param "Second expression (it won't be evaluated)")))
   (@return "Unit atom if both expression after evaluation is equal, error - otherwise"))
+(: assertEqualToResult (-> Atom Atom Atom))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1219,6 +1241,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
   (@params (
     (@param "Atom which will be evaluated")))
   (@return "Tuple"))
+(: collapse (-> Atom Atom))
 ;; Implemented from Interpreters
   
 ;; Public MeTTa
@@ -1227,6 +1250,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
   (@params (
     (@param "Function name which space need to be captured")))
   (@return "Function"))
+(: capture (-> Atom Atom))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1236,6 +1260,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "Atom (it will be evaluated)")
     (@param "Tuple of pairs mapping condition patterns to results")))
   (@return "Result of evaluating of Atom bound to met condition"))
+(: case (-> Atom Expression Atom))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1244,6 +1269,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
   (@params (
     (@param "Tuple to be converted")))
   (@return "Argument converted to nondeterministic result"))
+(: superpose (-> Expression %Undefined%))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1253,6 +1279,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "Key's name")
     (@param "New value")))
   (@return "Unit atom"))
+(: pragma! (-> Symbol %Undefined% (->)))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1263,6 +1290,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "Module name")))
   (@return "Unit atom"))
 ;; Implemented from Interpreters
+(: import! (-> Atom Atom (->)))
 
 ;; Public MeTTa
 (@doc include
@@ -1270,6 +1298,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
   (@params (
     (@param "Name of metta script to import")))
   (@return "Unit atom"))
+(: include (-> Atom Atom))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1279,6 +1308,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "Token name")
     (@param "Atom, which is associated with the token after reduction")))
   (@return "Unit atom"))
+(: bind! (-> Symbol %Undefined% (->)))
 ;; Implemented from Interpreters
   
 ;; Public MeTTa
@@ -1288,6 +1318,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "Atom to print")
     (@param "Atom to return")))
   (@return "Evaluated second input"))
+(: trace! (-> %Undefined% $a $a))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1296,6 +1327,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
   (@params (
     (@param "Expression/atom to be printed out")))
   (@return "Unit atom"))
+(: println! (-> %Undefined% (->)))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1305,6 +1337,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "Expression with {} symbols to be replaced")
     (@param "Atoms to be placed inside expression instead of {}")))
   (@return "Expression with replaced {} with atoms"))
+(: format-args (-> String Expresson String))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1314,6 +1347,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
 	(@param "Variable list e.g. ($x $y)")
 	(@param "Atom which uses those variables")))
   (@return "Second argument but with variables being replaced with unique variables"))
+(: sealed (-> Expression Atom Atom))
 ;; Implemented from Interpreters
 
 
@@ -1333,6 +1367,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "Addend")
     (@param "Augend")))
   (@return "Sum"))
+(: + (-> Number Number Number))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1342,6 +1377,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "Minuend")
     (@param "Deductible")))
   (@return "Difference"))
+(: - (-> Number Number Number))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1351,6 +1387,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "Multiplier")
     (@param "Multiplicand")))
   (@return "Product"))
+(: * (-> Number Number Number))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1360,6 +1397,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "Dividend")
     (@param "Divisor")))
   (@return "Fraction"))
+(: / (-> Number Number Number))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1369,6 +1407,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "Dividend")
     (@param "Divisor")))
   (@return "Remainder"))
+(: % (-> Number Number Number))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1378,6 +1417,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "First number")
     (@param "Second number")))
   (@return "True if first argument is less than second, False - otherwise"))
+(: < (-> Number Number Bool))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1387,6 +1427,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "First number")
     (@param "Second number")))
   (@return "True if first argument is greater than second, False - otherwise"))
+(: > (-> Number Number Bool))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1396,6 +1437,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "First number")
     (@param "Second number")))
   (@return "True if first argument is less than or equal to second, False - otherwise"))
+(: <= (-> Number Number Bool))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1405,6 +1447,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "First number")
     (@param "Second number")))
   (@return "True if first argument is greater than or equal to second, False - otherwise"))
+(: >= (-> Number Number Bool))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1414,6 +1457,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "First argument")
     (@param "Second argument")))
   (@return "Returns True if two arguments are equal, False - otherwise. If arguments are of different type function returns Error currently"))
+(: == (-> $t $t Bool))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1422,6 +1466,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
   (@params (
     (@param "Non-deterministic set of values")))
   (@return "Unique values from input set"))
+(: unique (-> Atom Atom))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1431,6 +1476,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "Non-deterministic set of values")
     (@param "Another non-deterministic set of values")))
   (@return "Union of sets"))
+(: union (-> Atom Atom Atom))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1440,6 +1486,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "Non-deterministic set of values")
     (@param "Another non-deterministic set of values")))
   (@return "Intersection of sets"))
+(: intersection (-> Atom Atom Atom))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1449,6 +1496,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
     (@param "Non-deterministic set of values")
     (@param "Another non-deterministic set of values")))
   (@return "Subtraction of sets"))
+(: subtraction (-> Atom Atom Atom))
 ;; Implemented from Interpreters
 
 ;; Public MeTTa
@@ -1457,6 +1505,7 @@ This Markdown content is ready to be uploaded to your fine-tuner!
   (@params (
     (@param "URL to github repo")))
   (@return "Unit atom"))
+(:git-module!(->Atom(->)))
 ;; Implemented from Interpreters
 
 ```