chore: fixup memory aliasing

leanprover · Nov 1, 2024 · 4bc6d6c · 4bc6d6c
1 parent 94c4bc8
commit 4bc6d6c
Showing 1 changed file with 9 additions and 0 deletions.
diff --git 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`
 ---