Apply suggestions from code review

Co-authored-by: Siddharth <[email protected]>
leanprover · Oct 15, 2024 · 79d54e2 · 79d54e2
1 parent a78ed5c
commit 79d54e2
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/Proofs/AES-GCM/GCMGmultV8Sym.lean b/Proofs/AES-GCM/GCMGmultV8Sym.lean
@@ -95,8 +95,6 @@ theorem gcm_gmult_v8_program_run_27 (s0 sf : ArmState)
   simp only [←Memory.mem_eq_iff_read_mem_bytes_eq] at *
   simp only [memory_rules] at *
   sym_aggregate
-
-  -- stop
   -- Split conjunction
   repeat' apply And.intro
   · simp_mem; rfl

diff --git a/Tactics/Aggregate.lean b/Tactics/Aggregate.lean
@@ -30,6 +30,8 @@ def aggregate (axHyps : Array LocalDecl) (location : Location)
 
     let config := simpConfig?.getD aggregate.defaultSimpConfig
     let (ctx, simprocs) ← LNSymSimpContext
+        -- https://github.com/leanprover/lean4/blob/94b1e512da9df1394350ab81a28deca934271f65/src/Lean/Meta/DiscrTree.lean#L371
+        -- refines the discrimination tree to also index applied functions. 
         (noIndexAtArgs := false)
         (config := config)
         (decls := axHyps)