diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index aa82505a6e10062d55b81e2d347f36d159f95234..a5f0b688836ee34b189848b05d7444bc9ecb1a32 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -4,6 +4,17 @@ From stdpp Require Export strings.
 From stdpp Require Import gmap.
 Set Default Proof Using "Type".
 
+(** heap_lang.  A fairly simple language used for common Iris examples.
+
+- This is a right-to-left evaluated language, like CakeML and OCaml.  The reason
+  for this is that it makes curried functions usable: Given a WP for [f a b], we
+  know that any effects [f] might have to not matter until after *both* [a] and
+  [b] are evaluated.  With left-to-right evaluation, that triple is basically
+  useless the user let-expands [b].
+
+*)
+
+
 Delimit Scope expr_scope with E.
 Delimit Scope val_scope with V.