diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-09-22 00:41:13 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-09-22 00:41:13 -0400 |
| commit | e9fb194f228321f9477a26bf18617047722fd42a (patch) | |
| tree | 1d6f2bb9da1717a32b97c1735d92d955c4bfc851 /src/Util | |
| parent | 1628cb14799db7af9eb13e49ae89f50d8f527301 (diff) | |
Fix LockedLet
We want beta-iota-delta to leave behind a zeta-redex (a let-in), even
when unfolding locked_let.
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/LockedLet.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/LockedLet.v b/src/Util/LockedLet.v index 088e914fb..386b1789c 100644 --- a/src/Util/LockedLet.v +++ b/src/Util/LockedLet.v @@ -1,7 +1,7 @@ (** * A version of [let] that doesn't disappear under βδζ unless you also have ι and remove opacity *) Require Import Crypto.Util.Notations. -Definition locked_let {A} (x : A) : bool * A := (true, x). +Definition locked_let {A} (x : A) : bool * A := let y := x in (true, y). Definition unlock_let {A} (x : A) : locked_let x = (true, x) := eq_refl. Global Opaque locked_let. Global Arguments locked_let : simpl never. |