Skip to content

Commit

Permalink
fix: ShareCommon import
Browse files Browse the repository at this point in the history
  • Loading branch information
tydeu committed Nov 24, 2024
1 parent b6df50b commit 41f2122
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions src/Init/ShareCommon.lean
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Mario Carneiro
-/
prelude
import Init.Util
import Init.Data.UInt.Basic

namespace ShareCommon
/-
Expand Down

0 comments on commit 41f2122

Please sign in to comment.