From 8dfda06cb877b8c81592ac056a8785936de8aca0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 22 Jul 2019 11:35:50 +0200
Subject: [PATCH] =?UTF-8?q?mention=20how=20to=20use=20iL=C3=B6b=20for=20re?=
 =?UTF-8?q?cursive=20functions?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

diff --git a/HeapLang.md b/HeapLang.md
index 48a52fac2..254e8a3ab 100644
--- a/HeapLang.md
+++ b/HeapLang.md
@@ -105,6 +105,12 @@ Further tactics:
 
 There is no tactic for `Fork`, just do `wp_apply wp_fork`.
 
+To verify a recursive function, use `iLöb`.  Make sure you do `wp_pures` before
+running `iLöb`; otherwise the induction hypothesis will likely not be applicable
+when you need it.  (This makes sure that all administrative redexes are reduced
+in your induction hypothesis, just like we state our `WP` specifications with
+all of the redexes reduced.)
+
 ## Notation and lemmas for derived notions involving a thunk
 
 Sometimes, it is useful to define a derived notion in HeapLang that involves
-- 
GitLab