Skip to content

Commit

Permalink
perf: improve elaboration performance of Std.Data.DHashMap.Internal.R…
Browse files Browse the repository at this point in the history 
…awLemmas (#6814)

This PR optimizes the proofs in the internal file
`Std/Data/DHashMap/Internal/RawLemmas.lean` so that the file is quicker
to elaborate.
  • Loading branch information
@TwoFX
TwoFX authored Jan 28, 2025
1 parent e4364e7 commit f9d3dea
Showing 1 changed file with 224 additions and 215 deletions.
Loading

0 comments on commit f9d3dea

Please sign in to comment.