From cceb5c12fd1c65da2cdbd19afd314a824c754ad2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 26 Feb 2019 10:18:06 +0100
Subject: [PATCH] expand HeapLang docs a bit

---
 HeapLang.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/HeapLang.md b/HeapLang.md
index b9f2cd112..17c5e144b 100644
--- a/HeapLang.md
+++ b/HeapLang.md
@@ -46,6 +46,11 @@ Noteworthy is the fact that functions (`rec:`, `λ:`) in the value scope (`%V`)
 are *locked*.  This is to prevent them from being unfolded and reduced too
 eagerly.
 
+The widely used `#` is a short-hand to turn a basic literal (an integer, a
+location, a boolean literal or a unit value) into a value.  Since values coerce
+to expressions, `#` is widely used whenever a Coq value needs to be placed into
+a HeapLang term.
+
 ## Tactics
 
 HeapLang comes with a bunch of tactics that facilitate stepping through HeapLang
-- 
GitLab