leanprover-community · lzy0505 · Mar 2, 2026 · Mar 2, 2026 · Mar 2, 2026 · Mar 2, 2026
diff --git a/src/Iris.lean b/src/Iris.lean
@@ -1,7 +1,9 @@
-import Iris.Algebra
-import Iris.BI
-import Iris.Examples
-import Iris.Instances
-import Iris.ProofMode
-import Iris.Std
-import Iris.Tests
+module
+
+public import Iris.Algebra
+public import Iris.BI
+public import Iris.Examples
+public import Iris.Instances
+public import Iris.ProofMode
+public import Iris.Std
+public import Iris.Tests
diff --git a/src/Iris/Algebra.lean b/src/Iris/Algebra.lean
@@ -1,15 +1,17 @@
-import Iris.Algebra.Agree
-import Iris.Algebra.CMRA
-import Iris.Algebra.COFESolver
-import Iris.Algebra.DFrac
-import Iris.Algebra.Excl
-import Iris.Algebra.Frac
-import Iris.Algebra.GenMap
-import Iris.Algebra.LocalUpdates
-import Iris.Algebra.IProp
-import Iris.Algebra.OFE
-import Iris.Algebra.Updates
-import Iris.Algebra.UPred
-import Iris.Algebra.Heap
-import Iris.Algebra.View
-import Iris.Algebra.HeapView
+module
+
+public import Iris.Algebra.Agree
+public import Iris.Algebra.CMRA
+public import Iris.Algebra.COFESolver
+public import Iris.Algebra.DFrac
+public import Iris.Algebra.Excl
+public import Iris.Algebra.Frac
+public import Iris.Algebra.GenMap
+public import Iris.Algebra.LocalUpdates
+public import Iris.Algebra.IProp
+public import Iris.Algebra.OFE
+public import Iris.Algebra.Updates
+public import Iris.Algebra.UPred
+public import Iris.Algebra.Heap
+public import Iris.Algebra.View
+public import Iris.Algebra.HeapView
diff --git a/src/Iris/Algebra/Agree.lean b/src/Iris/Algebra/Agree.lean
@@ -3,9 +3,12 @@ Copyright (c) 2025 Leo Stefanesco. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leo Stefanesco, Puming Liu
 -/
+module
 
-import Iris.Algebra.CMRA
-import Iris.Algebra.OFE
+public import Iris.Algebra.CMRA
+public import Iris.Algebra.OFE
+
+@[expose] public section
 
 namespace Iris
 

diff --git a/src/Iris/Algebra/Auth.lean b/src/Iris/Algebra/Auth.lean
@@ -3,8 +3,10 @@ Copyright (c) 2025 Alexander Bai. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alexander Bai
 -/
-import Iris.Algebra.View
-import Iris.Algebra.LocalUpdates
+module
+
+public import Iris.Algebra.View
+public import Iris.Algebra.LocalUpdates
 
 /-!
 # Authoritative Camera
@@ -14,6 +16,8 @@ The authoritative camera has 2 types of elements:
 -  and the fragment `◯ b`
 -/
 
+@[expose] public section
+
 open Iris
 
 open OFE CMRA UCMRA View

diff --git a/src/Iris/Algebra/CMRA.lean b/src/Iris/Algebra/CMRA.lean
@@ -3,7 +3,11 @@ Copyright (c) 2025 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Сухарик (@suhr), Markus de Medeiros, Puming Liu
 -/
-import Iris.Algebra.OFE
+module
+
+public import Iris.Algebra.OFE
+
+@[expose] public section
 
 namespace Iris
 open OFE

diff --git a/src/Iris/Algebra/COFESolver.lean b/src/Iris/Algebra/COFESolver.lean
@@ -3,7 +3,11 @@ Copyright (c) 2025 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Iris.Algebra.OFE
+module
+
+public import Iris.Algebra.OFE
+
+@[expose] public section
 
 namespace Iris.COFE.OFunctor
 open OFE

diff --git a/src/Iris/Algebra/DFrac.lean b/src/Iris/Algebra/DFrac.lean
@@ -3,12 +3,15 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros, Mario Carneiro
 -/
+module
 
-import Iris.Algebra.CMRA
-import Iris.Algebra.OFE
-import Iris.Algebra.Frac
-import Iris.Algebra.Updates
-import Iris.Algebra.LocalUpdates
+public import Iris.Algebra.CMRA
+public import Iris.Algebra.OFE
+public import Iris.Algebra.Frac
+public import Iris.Algebra.Updates
+public import Iris.Algebra.LocalUpdates
+
+@[expose] public section
 
 namespace Iris
 

diff --git a/src/Iris/Algebra/Excl.lean b/src/Iris/Algebra/Excl.lean
@@ -3,8 +3,11 @@ Copyright (c) 2025 Oliver Soeser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Soeser, Mario Carneiro
 -/
+module
 
-import Iris.Algebra.CMRA
+public import Iris.Algebra.CMRA
+
+@[expose] public section
 
 namespace Iris
 

diff --git a/src/Iris/Algebra/Frac.lean b/src/Iris/Algebra/Frac.lean
@@ -3,9 +3,10 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros, Shreyas Srinivas, Mario Carneiro
 -/
+module
 
-import Iris.Algebra.CMRA
-import Iris.Algebra.OFE
+public import Iris.Algebra.CMRA
+public import Iris.Algebra.OFE
 
 /-!
 # The Frac CMRA
@@ -14,6 +15,8 @@ This CMRA captures the notion of fractional ownership of another resource.
 Traditionally the underlying set is assumed to be the half open interval $$(0,1]$$.
 -/
 
+@[expose] public section
+
 namespace Iris
 
 class Fraction (α : Type _) extends Add α where

diff --git a/src/Iris/Algebra/GenMap.lean b/src/Iris/Algebra/GenMap.lean
@@ -3,9 +3,13 @@ Copyright (c) 2025 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros
 -/
-import Iris.Algebra.OFE
-import Iris.Algebra.CMRA
-import Iris.Algebra.Updates
+module
+
+public import Iris.Algebra.OFE
+public import Iris.Algebra.CMRA
+public import Iris.Algebra.Updates
+
+@[expose] public section
 
 namespace Iris
 open OFE

diff --git a/src/Iris/Algebra/Heap.lean b/src/Iris/Algebra/Heap.lean
@@ -3,11 +3,14 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros, Puming Liu
 -/
+module
 
-import Iris.Algebra.CMRA
-import Iris.Algebra.OFE
-import Iris.Std.Set
-import Iris.Std.PartialMap
+public import Iris.Algebra.CMRA
+public import Iris.Algebra.OFE
+public import Iris.Std.Set
+public import Iris.Std.PartialMap
+
+@[expose] public section
 
 open Iris Std
 

diff --git a/src/Iris/Algebra/HeapView.lean b/src/Iris/Algebra/HeapView.lean
@@ -3,10 +3,12 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros, Puming Liu
 -/
-import Iris.Algebra.Heap
-import Iris.Algebra.View
-import Iris.Algebra.DFrac
-import Iris.Algebra.Frac
+module
+
+public import Iris.Algebra.Heap
+public import Iris.Algebra.View
+public import Iris.Algebra.DFrac
+public import Iris.Algebra.Frac
 
 /-!
 # Heap Views
@@ -28,6 +30,8 @@ It provides authoritative and fragmental ownership over heap elements with fract
 * `HeapView.update_replace`: Replacement update lemma
 -/
 
+@[expose] public section
+
 open Iris
 
 section heapView

diff --git a/src/Iris/Algebra/IProp.lean b/src/Iris/Algebra/IProp.lean
@@ -3,13 +3,16 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros
 -/
+module
 
-import Iris.Algebra.CMRA
-import Iris.Algebra.OFE
-import Iris.Algebra.UPred
-import Iris.Algebra.GenMap
-import Iris.Algebra.COFESolver
-import Init.Data.Vector
+public import Iris.Algebra.CMRA
+public import Iris.Algebra.OFE
+public import Iris.Algebra.UPred
+public import Iris.Algebra.GenMap
+public import Iris.Algebra.COFESolver
+public import Init.Data.Vector
+
+@[expose] public section
 
 namespace Iris
 

diff --git a/src/Iris/Algebra/LocalUpdates.lean b/src/Iris/Algebra/LocalUpdates.lean
@@ -3,7 +3,11 @@ Copyright (c) 2025 Сухарик. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Сухарик (@suhr), Mario Carneiro
 -/
-import Iris.Algebra.CMRA
+module
+
+public import Iris.Algebra.CMRA
+
+@[expose] public section
 
 namespace Iris
 

diff --git a/src/Iris/Algebra/Numbers.lean b/src/Iris/Algebra/Numbers.lean
@@ -3,10 +3,11 @@ Copyright (c) 2025 Shreyas Srinivas. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Shreyas Srinivas, Markus de Medeiros
 -/
+module
 
-import Iris.Algebra.CMRA
-import Iris.Algebra.OFE
-import Iris.Algebra.LocalUpdates
+public import Iris.Algebra.CMRA
+public import Iris.Algebra.OFE
+public import Iris.Algebra.LocalUpdates
 
 /-! ## Numbers CMRA
 Simple CMRA's for commutative monoids.
@@ -17,6 +18,8 @@ There are three variants:
 - "No core": there is no core (eg. (PNat, +))
 -/
 
+@[expose] public section
+
 open Std
 
 class IdentityFree (α : Type _) [Add α] where

diff --git a/src/Iris/Algebra/OFE.lean b/src/Iris/Algebra/OFE.lean
@@ -3,6 +3,9 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+module
+
+@[expose] public section
 
 namespace Iris
 

diff --git a/src/Iris/Algebra/UPred.lean b/src/Iris/Algebra/UPred.lean
@@ -3,9 +3,12 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros
 -/
+module
 
-import Iris.Algebra.CMRA
-import Iris.Algebra.OFE
+public import Iris.Algebra.CMRA
+public import Iris.Algebra.OFE
+
+@[expose] public section
 
 namespace Iris
 open CMRA

diff --git a/src/Iris/Algebra/Updates.lean b/src/Iris/Algebra/Updates.lean
@@ -3,7 +3,11 @@ Copyright (c) 2025 Сухарик. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Сухарик (@suhr)
 -/
-import Iris.Algebra.CMRA
+module
+
+public import Iris.Algebra.CMRA
+
+@[expose] public section
 
 namespace Iris
 

diff --git a/src/Iris/Algebra/View.lean b/src/Iris/Algebra/View.lean
@@ -3,13 +3,17 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros, Puming Liu
 -/
-import Iris.Algebra.CMRA
-import Iris.Algebra.OFE
-import Iris.Algebra.Frac
-import Iris.Algebra.DFrac
-import Iris.Algebra.Agree
-import Iris.Algebra.Updates
-import Iris.Algebra.LocalUpdates
+module
+
+public import Iris.Algebra.CMRA
+public import Iris.Algebra.OFE
+public import Iris.Algebra.Frac
+public import Iris.Algebra.DFrac
+public import Iris.Algebra.Agree
+public import Iris.Algebra.Updates
+public import Iris.Algebra.LocalUpdates
+
+@[expose] public section
 
 open Iris
 

diff --git a/src/Iris/BI.lean b/src/Iris/BI.lean
@@ -1,8 +1,10 @@
-import Iris.BI.Classes
-import Iris.BI.DerivedLaws
-import Iris.BI.DerivedLawsLater
-import Iris.BI.Extensions
-import Iris.BI.Instances
-import Iris.BI.BI
-import Iris.BI.Notation
-import Iris.BI.Updates
+module
+
+public import Iris.BI.Classes
+public import Iris.BI.DerivedLaws
+public import Iris.BI.DerivedLawsLater
+public import Iris.BI.Extensions
+public import Iris.BI.Instances
+public import Iris.BI.BI
+public import Iris.BI.Notation
+public import Iris.BI.Updates
diff --git a/src/Iris/BI/BI.lean b/src/Iris/BI/BI.lean
@@ -3,8 +3,12 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro
 -/
-import Iris.Algebra.OFE
-import Iris.BI.BIBase
+module
+
+public import Iris.Algebra.OFE
+public import Iris.BI.BIBase
+
+@[expose] public section
 
 namespace Iris
 open Iris.Std OFE