From e5c563f98cbfec7d5e58d83cf712960b708c2792 Mon Sep 17 00:00:00 2001
From: Derek Dreyer <dreyer@mpi-sws.org>
Date: Fri, 7 Oct 2016 15:59:43 +0200
Subject: [PATCH] deleted an errant lambda
---
docs/program-logic.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index d9ffd5d3b..ca8042cc1 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -130,7 +130,7 @@ The fragment will then be available to the user of the logic, as their way of ta
It turns out that weakest precondition is actually quite convenient to work with, in particular when perfoming these proofs on paper.
Still, for a more traditional presentation, we can easily derive the notion of a Hoare triple:
\[
-\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \wpre{\expr}[\mask]{\lambda\Ret\val.\propB})}
+\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \wpre{\expr}[\mask]{\Ret\val.\propB})}
\]
\subsection{Lost stuff}
--
GitLab