Coalton as a sub-mode in lisp files

content/en/modes/coalton-lang.md

@@ -10,8 +10,27 @@ NEW as of January, 2025.
 
 Lem's Coalton mode provides:
 
-- code highlighting for `.coal` files.
-- indentation support.
-- show autodoc for Coalton functions.
--  its arguments can be different from definitions since the information is from Swank, just like Common Lisp.
-- compilation commands: `coalton-compile-defun` (on the usual `C-c C-c`) and `M-x coalton-compile-region`
+- support for `.coal` files
+- support for Coalton code inside `coalton-toplevel` in lisp-mode
+- code highlighting
+- indentation support
+- show autodoc for Coalton functions
+-  its arguments can be different from definitions since the information is from Swank, just like Common Lisp
+- compilation commands: `coalton-compile-defun` (on the usual `C-c C-c`) and `M-x coalton-compile-region`.
+
+
+`coalton-mode` is enabled as a sub-mode inside the `coalton-toplevel`
+form in lisp-mode: that means that in the following file, the type
+`Integer` is highlighted even in lisp-mode:
+
+~~~lisp
+;; Just for testing: test.lisp
+(defpackage foo
+  (:use :coalton-prelude))
+(in-package :foo)
+
+(coalton-toplevel
+  (declare foo (Integer -> Integer))
+  ...
+  )
+~~~