From 4bc6d6cdd1287e576ea93f64d8778e4e908b1635 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Fri, 1 Nov 2024 13:13:05 -0500 Subject: [PATCH] chore: fixup memory aliasing --- Proofs/Experiments/MemoryAliasing.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean index 002dde0d..eecd3ee2 100644 --- a/Proofs/Experiments/MemoryAliasing.lean +++ b/Proofs/Experiments/MemoryAliasing.lean @@ -226,6 +226,12 @@ info: [simp_mem.info] ⚙️ Processing 'hab' : 'a ≤ a + 1' mem_omega -- by default, process all hyps /-- +warning: unused variable `h'` +note: this linter can be disabled with `set_option linter.unusedVariables false` +--- +warning: unused variable `hab` +note: this linter can be disabled with `set_option linter.unusedVariables false` +--- info: [simp_mem.info] ⚙️ Processing 'hab' : 'a ≤ a + 1' [simp_mem.info] ⚙️ Matching on ⊢ a ≤ a + 1 [simp_mem.info] Adding omega facts from hypotheses @@ -244,6 +250,9 @@ example (h' : a ≤ 100) (hab : a ≤ a + 1) : a ≤ a + 1 := by /-- +warning: unused variable `h'` +note: this linter can be disabled with `set_option linter.unusedVariables false` +--- warning: unused variable `hab` note: this linter can be disabled with `set_option linter.unusedVariables false` ---