From fc67298392977826ad3ca15d1bf317fab7f79077 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Mon, 16 Sep 2024 05:54:53 +0100 Subject: [PATCH] Update src/Init/Data/BitVec/Lemmas.lean Co-authored-by: Kim Morrison --- src/Init/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 12e4261737e6..32d4ed25532d 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -528,7 +528,7 @@ theorem getElem_truncate (m : Nat) (x : BitVec n) (i : Nat) (hi : i < m) : simp [getElem?_eq, getElem_zeroExtend] theorem getElem?_truncate (m : Nat) (x : BitVec n) (i : Nat) : - (truncate m x)[i]? = if i < m then some (x.getLsbD i) else none := + (truncate m x)[i]? = if h : i < m then some x[i] else none := getElem?_zeroExtend m x i theorem getLsbD_truncate (m : Nat) (x : BitVec n) (i : Nat) :