summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--docs/users_guide/ghci.rst9
1 files changed, 9 insertions, 0 deletions
diff --git a/docs/users_guide/ghci.rst b/docs/users_guide/ghci.rst
index 857a03aecd..72e2d66e12 100644
--- a/docs/users_guide/ghci.rst
+++ b/docs/users_guide/ghci.rst
@@ -2994,6 +2994,12 @@ commonly used commands.
The :ghci-cmd:`:uses` command requires :ghci-cmd:`:set +c` to be set.
+.. ghci-cmd:: :: ⟨builtin-command⟩
+
+ Executes the GHCi built-in command (e.g. ``::type 3``). That is,
+ look up on the list of builtin commands, excluding defined macros.
+ See also: :ghci-cmd:`:def`.
+
.. ghci-cmd:: :! ⟨command⟩
.. index::
@@ -3297,6 +3303,9 @@ Here are some examples:
You get ``:type 3`` with your defined macro.
+When giving priority to built-in commands, you can use
+:ghci-cmd:`:: ⟨builtin-command⟩`, like ``::type 3``.
+
.. _dot-haskeline-file:
The ``.haskeline`` file