From d793408751b053a5ce05e5ccabb37f92f4afd898 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 5 Oct 2018 08:58:52 +0200
Subject: [PATCH] explain RTL

---
 theories/heap_lang/lang.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index aa82505a6..a5f0b6888 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.
 
-- 
GitLab