diff --git a/Lean4Lean.lean b/Lean4Lean.lean index a0874ef7..4adee1ab 100644 --- a/Lean4Lean.lean +++ b/Lean4Lean.lean @@ -1,3 +1,5 @@ +module +prelude import Lean4Lean.Environment /- diff --git a/Lean4Lean/Declaration.lean b/Lean4Lean/Declaration.lean index 94cbdf80..765199db 100644 --- a/Lean4Lean/Declaration.lean +++ b/Lean4Lean/Declaration.lean @@ -1,4 +1,8 @@ -import Lean.Declaration +module + +public import Lean.Declaration + +@[expose] public section namespace Lean diff --git a/Lean4Lean/Environment.lean b/Lean4Lean/Environment.lean index e7f49811..c9cd8567 100644 --- a/Lean4Lean/Environment.lean +++ b/Lean4Lean/Environment.lean @@ -1,7 +1,11 @@ -import Lean4Lean.TypeChecker -import Lean4Lean.Quot -import Lean4Lean.Inductive.Add -import Lean4Lean.Primitive +module + +public import Lean4Lean.TypeChecker +public import Lean4Lean.Quot +public import Lean4Lean.Inductive.Add +public import Lean4Lean.Primitive + +@[expose] public section namespace Lean4Lean open Lean hiding Environment Exception diff --git a/Lean4Lean/Environment/Basic.lean b/Lean4Lean/Environment/Basic.lean index 6cb49656..19f20f74 100644 --- a/Lean4Lean/Environment/Basic.lean +++ b/Lean4Lean/Environment/Basic.lean @@ -1,5 +1,9 @@ -import Lean.Environment -import Batteries.Tactic.OpenPrivate +module + +public import Lean.Environment +public import Batteries.Tactic.OpenPrivate + +@[expose] public section namespace Lean.Kernel.Environment diff --git a/Lean4Lean/EquivManager.lean b/Lean4Lean/EquivManager.lean index 51cb3f00..abc12669 100644 --- a/Lean4Lean/EquivManager.lean +++ b/Lean4Lean/EquivManager.lean @@ -1,5 +1,9 @@ -import Batteries.Data.UnionFind.Basic -import Lean4Lean.PtrEq +module + +public import Batteries.Data.UnionFind.Basic +public import Lean4Lean.PtrEq + +@[expose] public section namespace Lean4Lean open Lean diff --git a/Lean4Lean/Experimental/CoinductiveLogRel.lean b/Lean4Lean/Experimental/CoinductiveLogRel.lean index b33b9b8d..91e3e0da 100644 --- a/Lean4Lean/Experimental/CoinductiveLogRel.lean +++ b/Lean4Lean/Experimental/CoinductiveLogRel.lean @@ -1,4 +1,8 @@ -import Lean4Lean.Theory.Typing.HeadReduction +module + +public import Lean4Lean.Theory.Typing.HeadReduction + +@[expose] public section namespace Lean4Lean namespace VEnv diff --git a/Lean4Lean/Experimental/DomainTheory.lean b/Lean4Lean/Experimental/DomainTheory.lean index a20b2b95..12dcdda1 100644 --- a/Lean4Lean/Experimental/DomainTheory.lean +++ b/Lean4Lean/Experimental/DomainTheory.lean @@ -1,4 +1,8 @@ -import Lean4Lean.Experimental.SExpr +module + +public import Lean4Lean.Experimental.SExpr + +@[expose] public section namespace Lean4Lean diff --git a/Lean4Lean/Experimental/LogRel.lean b/Lean4Lean/Experimental/LogRel.lean index c519d919..3ef5d13c 100644 --- a/Lean4Lean/Experimental/LogRel.lean +++ b/Lean4Lean/Experimental/LogRel.lean @@ -1,4 +1,8 @@ -import Lean4Lean.Experimental.SExpr +module + +public import Lean4Lean.Experimental.SExpr + +@[expose] public section namespace Lean4Lean diff --git a/Lean4Lean/Experimental/MoreStepIndexed.lean b/Lean4Lean/Experimental/MoreStepIndexed.lean index b533aa77..1e1b7f85 100644 --- a/Lean4Lean/Experimental/MoreStepIndexed.lean +++ b/Lean4Lean/Experimental/MoreStepIndexed.lean @@ -1,4 +1,8 @@ -import Lean4Lean.Experimental.SExpr +module + +public import Lean4Lean.Experimental.SExpr + +@[expose] public section namespace Lean4Lean diff --git a/Lean4Lean/Experimental/NormalEq.lean b/Lean4Lean/Experimental/NormalEq.lean index a540cf19..b5e2b86e 100644 --- a/Lean4Lean/Experimental/NormalEq.lean +++ b/Lean4Lean/Experimental/NormalEq.lean @@ -1,5 +1,9 @@ -import Lean4Lean.Theory.Typing.Lemmas -import Lean4Lean.Theory.Typing.Pattern +module + +public import Lean4Lean.Theory.Typing.Lemmas +public import Lean4Lean.Theory.Typing.Pattern + +@[expose] public section -- TODO: remove, this is now part of ChurchRosser.lean diff --git a/Lean4Lean/Experimental/ParallelReduction.lean b/Lean4Lean/Experimental/ParallelReduction.lean index 187f4b27..0aa8d536 100644 --- a/Lean4Lean/Experimental/ParallelReduction.lean +++ b/Lean4Lean/Experimental/ParallelReduction.lean @@ -1,5 +1,9 @@ -import Lean4Lean.Theory.Typing.Strong -import Lean4Lean.Experimental.NormalEq +module + +public import Lean4Lean.Theory.Typing.Strong +public import Lean4Lean.Experimental.NormalEq + +@[expose] public section -- TODO: remove, this is now part of ChurchRosser.lean diff --git a/Lean4Lean/Experimental/SExpr.lean b/Lean4Lean/Experimental/SExpr.lean index 0d9aa48b..1260d184 100644 --- a/Lean4Lean/Experimental/SExpr.lean +++ b/Lean4Lean/Experimental/SExpr.lean @@ -1,5 +1,9 @@ -import Lean4Lean.Theory.Typing.Lemmas -import Lean4Lean.Theory.Typing.Pattern +module + +public import Lean4Lean.Theory.Typing.Lemmas +public import Lean4Lean.Theory.Typing.Pattern + +@[expose] public section namespace Lean4Lean diff --git a/Lean4Lean/Experimental/ShapeLogRel.lean b/Lean4Lean/Experimental/ShapeLogRel.lean index a17a961b..73678e67 100644 --- a/Lean4Lean/Experimental/ShapeLogRel.lean +++ b/Lean4Lean/Experimental/ShapeLogRel.lean @@ -1,4 +1,8 @@ -import Lean4Lean.Experimental.SExpr +module + +public import Lean4Lean.Experimental.SExpr + +@[expose] public section namespace Lean4Lean diff --git a/Lean4Lean/Experimental/ShapeLogRelAdequacy.lean b/Lean4Lean/Experimental/ShapeLogRelAdequacy.lean index c9b663e1..d41ad97f 100644 --- a/Lean4Lean/Experimental/ShapeLogRelAdequacy.lean +++ b/Lean4Lean/Experimental/ShapeLogRelAdequacy.lean @@ -1,4 +1,8 @@ -import Lean4Lean.Experimental.ShapeLogRel +module + +public import Lean4Lean.Experimental.ShapeLogRel + +@[expose] public section namespace Lean4Lean diff --git a/Lean4Lean/Experimental/StepIndexed.lean b/Lean4Lean/Experimental/StepIndexed.lean index 7b32fcac..a9e4dab1 100644 --- a/Lean4Lean/Experimental/StepIndexed.lean +++ b/Lean4Lean/Experimental/StepIndexed.lean @@ -1,4 +1,8 @@ -import Lean4Lean.Experimental.SExpr +module + +public import Lean4Lean.Experimental.SExpr + +@[expose] public section namespace Lean4Lean diff --git a/Lean4Lean/Experimental/Stratified.lean b/Lean4Lean/Experimental/Stratified.lean index 251abb12..5ceb35aa 100644 --- a/Lean4Lean/Experimental/Stratified.lean +++ b/Lean4Lean/Experimental/Stratified.lean @@ -1,5 +1,9 @@ -import Lean4Lean.Theory.Typing.Lemmas -import Lean4Lean.Theory.Typing.Strong +module + +public import Lean4Lean.Theory.Typing.Lemmas +public import Lean4Lean.Theory.Typing.Strong + +@[expose] public section namespace Lean4Lean namespace VEnv diff --git a/Lean4Lean/Experimental/StratifiedUntyped.lean b/Lean4Lean/Experimental/StratifiedUntyped.lean index d1ba4df8..68962e37 100644 --- a/Lean4Lean/Experimental/StratifiedUntyped.lean +++ b/Lean4Lean/Experimental/StratifiedUntyped.lean @@ -1,5 +1,9 @@ -import Lean4Lean.Theory.Typing.Lemmas -import Lean4Lean.Theory.Typing.Strong +module + +public import Lean4Lean.Theory.Typing.Lemmas +public import Lean4Lean.Theory.Typing.Strong + +@[expose] public section namespace Lean4Lean namespace VEnv diff --git a/Lean4Lean/Experimental/Stronger.lean b/Lean4Lean/Experimental/Stronger.lean index 20c308b6..b7b39fe2 100644 --- a/Lean4Lean/Experimental/Stronger.lean +++ b/Lean4Lean/Experimental/Stronger.lean @@ -1,4 +1,8 @@ -import Lean4Lean.Theory.Typing.Lemmas +module + +public import Lean4Lean.Theory.Typing.Lemmas + +@[expose] public section namespace Lean4Lean diff --git a/Lean4Lean/Experimental/Thierry.lean b/Lean4Lean/Experimental/Thierry.lean index e16d3109..fa36e281 100644 --- a/Lean4Lean/Experimental/Thierry.lean +++ b/Lean4Lean/Experimental/Thierry.lean @@ -1,3 +1,7 @@ +module + +@[expose] public section + /-! # Partial formalization of Coquand & Huber, "An Adequacy Theorem for Dependent Type Theory" https://doi.org/10.1007/s00224-018-9879-9 diff --git a/Lean4Lean/Experimental/Thierry2.lean b/Lean4Lean/Experimental/Thierry2.lean index 86eb589b..65e2390f 100644 --- a/Lean4Lean/Experimental/Thierry2.lean +++ b/Lean4Lean/Experimental/Thierry2.lean @@ -1,3 +1,5 @@ +module + /-! # Partial formalization of Coquand & Huber, "An Adequacy Theorem for Dependent Type Theory" https://doi.org/10.1007/s00224-018-9879-9 @@ -829,3 +831,5 @@ theorem DefEqLamF.mono_r : DefEqF (n := n) B B .U a .U → DefEqPiF DefEqF B F F termination_by 2 * n + 1 end + +@[expose] public section diff --git a/Lean4Lean/Experimental/UniqueTyping.lean b/Lean4Lean/Experimental/UniqueTyping.lean index 2d06d8cd..4731e33c 100644 --- a/Lean4Lean/Experimental/UniqueTyping.lean +++ b/Lean4Lean/Experimental/UniqueTyping.lean @@ -1,4 +1,8 @@ -import Lean4Lean.Experimental.ShapeLogRelAdequacy +module + +public import Lean4Lean.Experimental.ShapeLogRelAdequacy + +@[expose] public section /-! # Unique typing over the SExpr weak defeq. diff --git a/Lean4Lean/Expr.lean b/Lean4Lean/Expr.lean index e9bf4da3..de16749a 100644 --- a/Lean4Lean/Expr.lean +++ b/Lean4Lean/Expr.lean @@ -1,4 +1,8 @@ -import Lean.Environment +module + +public import Lean.Environment + +@[expose] public section namespace Lean namespace Expr diff --git a/Lean4Lean/ForEachExprV.lean b/Lean4Lean/ForEachExprV.lean index f76c67da..12c9dbe3 100644 --- a/Lean4Lean/ForEachExprV.lean +++ b/Lean4Lean/ForEachExprV.lean @@ -1,5 +1,9 @@ -import Lean.Expr -import Lean.Util.MonadCache +module + +public import Lean.Expr +public import Lean.Util.MonadCache + +@[expose] public section /-! This is the same as `Expr.forEach` but it uses `StateT` instead of `StateRefT` to avoid opaques. diff --git a/Lean4Lean/Inductive/Add.lean b/Lean4Lean/Inductive/Add.lean index 2085a04d..9a48544f 100644 --- a/Lean4Lean/Inductive/Add.lean +++ b/Lean4Lean/Inductive/Add.lean @@ -1,6 +1,10 @@ -import Batteries.Data.List.Basic -import Lean4Lean.Environment.Basic -import Lean4Lean.TypeChecker +module + +public import Batteries.Data.List.Basic +public import Lean4Lean.Environment.Basic +public import Lean4Lean.TypeChecker + +@[expose] public section namespace Lean4Lean open Lean hiding Environment Exception diff --git a/Lean4Lean/Inductive/Reduce.lean b/Lean4Lean/Inductive/Reduce.lean index 3779aca9..10cc2b41 100644 --- a/Lean4Lean/Inductive/Reduce.lean +++ b/Lean4Lean/Inductive/Reduce.lean @@ -1,6 +1,10 @@ -import Lean.Structure -import Lean4Lean.Expr -import Lean4Lean.Environment.Basic +module + +public import Lean.Structure +public import Lean4Lean.Expr +public import Lean4Lean.Environment.Basic + +@[expose] public section namespace Lean4Lean open Lean hiding Environment diff --git a/Lean4Lean/Instantiate.lean b/Lean4Lean/Instantiate.lean index b8cd6b9b..3e7584ca 100644 --- a/Lean4Lean/Instantiate.lean +++ b/Lean4Lean/Instantiate.lean @@ -1,6 +1,10 @@ -import Lean.Expr -import Lean.LocalContext -import Lean.Util.InstantiateLevelParams +module + +public import Lean.Expr +public import Lean.LocalContext +public import Lean.Util.InstantiateLevelParams + +@[expose] public section namespace Lean namespace Expr diff --git a/Lean4Lean/Level.lean b/Lean4Lean/Level.lean index ea798f7b..27366e0f 100644 --- a/Lean4Lean/Level.lean +++ b/Lean4Lean/Level.lean @@ -1,5 +1,9 @@ -import Lean -import Lean4Lean.List +module + +public import Lean +public import Lean4Lean.List + +@[expose] public section namespace Lean.Level diff --git a/Lean4Lean/List.lean b/Lean4Lean/List.lean index 875127c5..ad6cd0d8 100644 --- a/Lean4Lean/List.lean +++ b/Lean4Lean/List.lean @@ -1,3 +1,6 @@ +module + +@[expose] public section @[specialize] def List.all2 (R : α → α → Bool) : List α → List α → Bool | a1 :: as1, a2 :: as2 => R a1 a2 && all2 R as1 as2 diff --git a/Lean4Lean/LocalContext.lean b/Lean4Lean/LocalContext.lean index 2256893c..8055bc25 100644 --- a/Lean4Lean/LocalContext.lean +++ b/Lean4Lean/LocalContext.lean @@ -1,4 +1,8 @@ -import Lean.LocalContext +module + +public import Lean.LocalContext + +@[expose] public section namespace Lean4Lean open Lean diff --git a/Lean4Lean/Primitive.lean b/Lean4Lean/Primitive.lean index fae0c93a..fceff67d 100644 --- a/Lean4Lean/Primitive.lean +++ b/Lean4Lean/Primitive.lean @@ -1,5 +1,9 @@ -import Lean4Lean.TypeChecker -import Lean4Lean.Environment.Basic +module + +public import Lean4Lean.TypeChecker +public import Lean4Lean.Environment.Basic + +@[expose] public section namespace Lean4Lean namespace Environment diff --git a/Lean4Lean/PtrEq.lean b/Lean4Lean/PtrEq.lean index e5309f3c..9969d408 100644 --- a/Lean4Lean/PtrEq.lean +++ b/Lean4Lean/PtrEq.lean @@ -1,4 +1,8 @@ -import Lean.Declaration +module + +public import Lean.Declaration + +@[expose] public section namespace Lean4Lean open Lean diff --git a/Lean4Lean/Quot.lean b/Lean4Lean/Quot.lean index 194b3a47..0d3a76d8 100644 --- a/Lean4Lean/Quot.lean +++ b/Lean4Lean/Quot.lean @@ -1,8 +1,12 @@ -import Batteries.Tactic.OpenPrivate -import Lean4Lean.Environment.Basic -import Lean4Lean.Expr -import Lean4Lean.Instantiate -import Lean4Lean.LocalContext +module + +public import Batteries.Tactic.OpenPrivate +public import Lean4Lean.Environment.Basic +public import Lean4Lean.Expr +public import Lean4Lean.Instantiate +public import Lean4Lean.LocalContext + +@[expose] public section namespace Lean4Lean open Lean hiding Environment Exception diff --git a/Lean4Lean/Std/Basic.lean b/Lean4Lean/Std/Basic.lean index 9a353aa4..b567b41f 100644 --- a/Lean4Lean/Std/Basic.lean +++ b/Lean4Lean/Std/Basic.lean @@ -1,8 +1,12 @@ -import Batteries.CodeAction -import Batteries.Data.Array.Lemmas -import Batteries.Data.HashMap.Basic -import Batteries.Data.UnionFind.Basic -import Batteries.Tactic.SeqFocus +module + +public import Batteries.CodeAction +public import Batteries.Data.Array.Lemmas +public import Batteries.Data.HashMap.Basic +public import Batteries.Data.UnionFind.Basic +public import Batteries.Tactic.SeqFocus + +@[expose] public section open Std diff --git a/Lean4Lean/Std/Control.lean b/Lean4Lean/Std/Control.lean index d4c9e9d7..914d861f 100644 --- a/Lean4Lean/Std/Control.lean +++ b/Lean4Lean/Std/Control.lean @@ -1,2 +1,6 @@ +module + instance [Alternative m] : MonadLift Option m := ⟨fun | none => failure | some a => pure a⟩ + +@[expose] public section diff --git a/Lean4Lean/Std/HashMap.lean b/Lean4Lean/Std/HashMap.lean index 58c495eb..874a53ac 100644 --- a/Lean4Lean/Std/HashMap.lean +++ b/Lean4Lean/Std/HashMap.lean @@ -1,5 +1,9 @@ -import Std.Data.HashMap.Lemmas -import Lean +module + +public import Std.Data.HashMap.Lemmas +public import Lean + +@[expose] public section namespace Std.Internal.List diff --git a/Lean4Lean/Std/NodupKeys.lean b/Lean4Lean/Std/NodupKeys.lean index 97d42dfa..8bc299a7 100644 --- a/Lean4Lean/Std/NodupKeys.lean +++ b/Lean4Lean/Std/NodupKeys.lean @@ -1,5 +1,9 @@ -import Batteries.Data.List.Perm -import Batteries.Tactic.SeqFocus +module + +public import Batteries.Data.List.Perm +public import Batteries.Tactic.SeqFocus + +@[expose] public section namespace List def NodupKeys (l : List (α × β)) : Prop := Nodup (l.map (·.1)) diff --git a/Lean4Lean/Std/PersistentHashMap.lean b/Lean4Lean/Std/PersistentHashMap.lean index be9fab9b..43c803a6 100644 --- a/Lean4Lean/Std/PersistentHashMap.lean +++ b/Lean4Lean/Std/PersistentHashMap.lean @@ -1,6 +1,10 @@ -import Lean.Data.SMap -import Std.Data.HashMap.Lemmas -import Lean4Lean.Verify.Axioms +module + +public import Lean.Data.SMap +public import Std.Data.HashMap.Lemmas +public import Lean4Lean.Verify.Axioms + +@[expose] public section namespace Lean.PersistentHashMap diff --git a/Lean4Lean/Std/SMap.lean b/Lean4Lean/Std/SMap.lean index e1d72492..7362dccf 100644 --- a/Lean4Lean/Std/SMap.lean +++ b/Lean4Lean/Std/SMap.lean @@ -1,7 +1,11 @@ -import Lean.Data.SMap -import Std.Data.HashMap.Lemmas -import Lean4Lean.Std.HashMap -import Lean4Lean.Std.PersistentHashMap +module + +public import Lean.Data.SMap +public import Std.Data.HashMap.Lemmas +public import Lean4Lean.Std.HashMap +public import Lean4Lean.Std.PersistentHashMap + +@[expose] public section namespace Lean.SMap diff --git a/Lean4Lean/Std/ToExpr.lean b/Lean4Lean/Std/ToExpr.lean index 7a960731..9261ea81 100644 --- a/Lean4Lean/Std/ToExpr.lean +++ b/Lean4Lean/Std/ToExpr.lean @@ -1,9 +1,13 @@ +module + /- Copyright (c) 2023 Kyle Miller. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kyle Miller -/ -import Lean +public import Lean + +@[expose] public section /-! # `ToExpr` instances for Mathlib @@ -39,7 +43,7 @@ open DataValue in /-- Core of a hand-written `ToExpr` handler for `MData`. Uses the `KVMap.set*` functions rather than going into the internals of the `KVMap` data structure. -/ -private def toExprMData (md : MData) : Expr := Id.run do +def toExprMData (md : MData) : Expr := Id.run do let mut e := mkConst ``MData.empty for (k, v) in md do let k := toExpr k diff --git a/Lean4Lean/Std/Variable!.lean b/Lean4Lean/Std/Variable!.lean index b2280e8a..a3c6bce8 100644 --- a/Lean4Lean/Std/Variable!.lean +++ b/Lean4Lean/Std/Variable!.lean @@ -1,4 +1,8 @@ -import Lean +module + +public import Lean + +@[expose] public section macro "variable!" args:(ppSpace colGt bracketedBinder)+ " in" cmd:ppDedent(command) : command => do diff --git a/Lean4Lean/Theory.lean b/Lean4Lean/Theory.lean index 67c3c0f5..a08f47a8 100644 --- a/Lean4Lean/Theory.lean +++ b/Lean4Lean/Theory.lean @@ -1,3 +1,5 @@ +module +prelude import Lean4Lean.Theory.Typing.EnvLemmas import Lean4Lean.Theory.Typing.Strong import Lean4Lean.Theory.Typing.UniqueTyping diff --git a/Lean4Lean/Theory/Inductive.lean b/Lean4Lean/Theory/Inductive.lean index 624985fd..af5a60ac 100644 --- a/Lean4Lean/Theory/Inductive.lean +++ b/Lean4Lean/Theory/Inductive.lean @@ -1,4 +1,8 @@ -import Lean4Lean.Theory.VDecl +module + +public import Lean4Lean.Theory.VDecl + +@[expose] public section namespace Lean4Lean diff --git a/Lean4Lean/Theory/Meta.lean b/Lean4Lean/Theory/Meta.lean index 42ec4a3a..31a0bded 100644 --- a/Lean4Lean/Theory/Meta.lean +++ b/Lean4Lean/Theory/Meta.lean @@ -1,8 +1,12 @@ -import Batteries.Lean.Expr -import Lean4Lean.Std.Control -import Lean4Lean.Std.ToExpr -import Lean4Lean.Theory.VEnv -import Lean4Lean.Inductive.Reduce +module + +public import Batteries.Lean.Expr +public import Lean4Lean.Std.Control +public import Lean4Lean.Std.ToExpr +public import Lean4Lean.Theory.VEnv +public import Lean4Lean.Inductive.Reduce + +@[expose] public section namespace Lean4Lean diff --git a/Lean4Lean/Theory/Quot.lean b/Lean4Lean/Theory/Quot.lean index e52a5760..e27c0f4f 100644 --- a/Lean4Lean/Theory/Quot.lean +++ b/Lean4Lean/Theory/Quot.lean @@ -1,5 +1,9 @@ -import Lean4Lean.Theory.VEnv -import Lean4Lean.Theory.Meta +module + +public import Lean4Lean.Theory.VEnv +public import Lean4Lean.Theory.Meta + +@[expose] public section namespace Lean4Lean diff --git a/Lean4Lean/Theory/Typing/Basic.lean b/Lean4Lean/Theory/Typing/Basic.lean index 62ae8f86..5faa658c 100644 --- a/Lean4Lean/Theory/Typing/Basic.lean +++ b/Lean4Lean/Theory/Typing/Basic.lean @@ -1,4 +1,8 @@ -import Lean4Lean.Theory.VEnv +module + +public import Lean4Lean.Theory.VEnv + +@[expose] public section namespace Lean4Lean diff --git a/Lean4Lean/Theory/Typing/ChurchRosser.lean b/Lean4Lean/Theory/Typing/ChurchRosser.lean index 1f59b98b..9ed5e563 100644 --- a/Lean4Lean/Theory/Typing/ChurchRosser.lean +++ b/Lean4Lean/Theory/Typing/ChurchRosser.lean @@ -1,6 +1,10 @@ -import Lean4Lean.Theory.Typing.Pattern -import Lean4Lean.Theory.Typing.Strong -import Lean4Lean.Theory.Typing.UniqueTyping +module + +public import Lean4Lean.Theory.Typing.Pattern +public import Lean4Lean.Theory.Typing.Strong +public import Lean4Lean.Theory.Typing.UniqueTyping + +@[expose] public section namespace Lean4Lean namespace VEnv diff --git a/Lean4Lean/Theory/Typing/Env.lean b/Lean4Lean/Theory/Typing/Env.lean index 02306de7..e629bf26 100644 --- a/Lean4Lean/Theory/Typing/Env.lean +++ b/Lean4Lean/Theory/Typing/Env.lean @@ -1,7 +1,11 @@ -import Lean4Lean.Theory.Typing.Basic -import Lean4Lean.Theory.VDecl -import Lean4Lean.Theory.Quot -import Lean4Lean.Theory.Inductive +module + +public import Lean4Lean.Theory.Typing.Basic +public import Lean4Lean.Theory.VDecl +public import Lean4Lean.Theory.Quot +public import Lean4Lean.Theory.Inductive + +@[expose] public section namespace Lean4Lean diff --git a/Lean4Lean/Theory/Typing/EnvLemmas.lean b/Lean4Lean/Theory/Typing/EnvLemmas.lean index 3a7db5e1..23e1fdc6 100644 --- a/Lean4Lean/Theory/Typing/EnvLemmas.lean +++ b/Lean4Lean/Theory/Typing/EnvLemmas.lean @@ -1,7 +1,11 @@ -import Lean4Lean.Theory.Typing.Lemmas -import Lean4Lean.Theory.Typing.Env -import Lean4Lean.Theory.Typing.QuotLemmas -import Lean4Lean.Theory.Typing.InductiveLemmas +module + +public import Lean4Lean.Theory.Typing.Lemmas +public import Lean4Lean.Theory.Typing.Env +public import Lean4Lean.Theory.Typing.QuotLemmas +public import Lean4Lean.Theory.Typing.InductiveLemmas + +@[expose] public section namespace Lean4Lean diff --git a/Lean4Lean/Theory/Typing/HeadReduction.lean b/Lean4Lean/Theory/Typing/HeadReduction.lean index fbef3e73..c1a28652 100644 --- a/Lean4Lean/Theory/Typing/HeadReduction.lean +++ b/Lean4Lean/Theory/Typing/HeadReduction.lean @@ -1,4 +1,8 @@ -import Lean4Lean.Theory.Typing.ChurchRosser +module + +public import Lean4Lean.Theory.Typing.ChurchRosser + +@[expose] public section /-! diff --git a/Lean4Lean/Theory/Typing/InductiveLemmas.lean b/Lean4Lean/Theory/Typing/InductiveLemmas.lean index 8113f11d..8317aa18 100644 --- a/Lean4Lean/Theory/Typing/InductiveLemmas.lean +++ b/Lean4Lean/Theory/Typing/InductiveLemmas.lean @@ -1,6 +1,10 @@ -import Std -import Lean4Lean.Theory.Typing.Lemmas -import Lean4Lean.Theory.Typing.Env +module + +public import Std +public import Lean4Lean.Theory.Typing.Lemmas +public import Lean4Lean.Theory.Typing.Env + +@[expose] public section namespace Lean4Lean namespace VEnv diff --git a/Lean4Lean/Theory/Typing/Injectivity.lean b/Lean4Lean/Theory/Typing/Injectivity.lean index 462173f7..2737969c 100644 --- a/Lean4Lean/Theory/Typing/Injectivity.lean +++ b/Lean4Lean/Theory/Typing/Injectivity.lean @@ -1,5 +1,9 @@ -import Lean4Lean.Theory.Typing.EnvLemmas -import Lean4Lean.Theory.Typing.Strong +module + +public import Lean4Lean.Theory.Typing.EnvLemmas +public import Lean4Lean.Theory.Typing.Strong + +@[expose] public section /-! A bunch of important structural theorems which we can't prove :( diff --git a/Lean4Lean/Theory/Typing/Lemmas.lean b/Lean4Lean/Theory/Typing/Lemmas.lean index 96e94a0c..8486f342 100644 --- a/Lean4Lean/Theory/Typing/Lemmas.lean +++ b/Lean4Lean/Theory/Typing/Lemmas.lean @@ -1,5 +1,9 @@ -import Lean4Lean.Theory.Typing.Basic -import Lean4Lean.Std.Variable! +module + +public import Lean4Lean.Theory.Typing.Basic +public import Lean4Lean.Std.Variable! + +@[expose] public section namespace Lean4Lean diff --git a/Lean4Lean/Theory/Typing/Meta.lean b/Lean4Lean/Theory/Typing/Meta.lean index e02c7ecb..bd898b17 100644 --- a/Lean4Lean/Theory/Typing/Meta.lean +++ b/Lean4Lean/Theory/Typing/Meta.lean @@ -1,4 +1,8 @@ -import Lean4Lean.Theory.Typing.Lemmas +module + +public import Lean4Lean.Theory.Typing.Lemmas + +@[expose] public section namespace Lean4Lean namespace VEnv diff --git a/Lean4Lean/Theory/Typing/Pattern.lean b/Lean4Lean/Theory/Typing/Pattern.lean index 87e77492..25f43417 100644 --- a/Lean4Lean/Theory/Typing/Pattern.lean +++ b/Lean4Lean/Theory/Typing/Pattern.lean @@ -1,4 +1,8 @@ -import Lean4Lean.Theory.VExpr +module + +public import Lean4Lean.Theory.VExpr + +@[expose] public section namespace Lean4Lean diff --git a/Lean4Lean/Theory/Typing/QuotLemmas.lean b/Lean4Lean/Theory/Typing/QuotLemmas.lean index cc20adf1..901b7924 100644 --- a/Lean4Lean/Theory/Typing/QuotLemmas.lean +++ b/Lean4Lean/Theory/Typing/QuotLemmas.lean @@ -1,5 +1,9 @@ -import Lean4Lean.Theory.Typing.Env -import Lean4Lean.Theory.Typing.Meta +module + +public import Lean4Lean.Theory.Typing.Env +public import Lean4Lean.Theory.Typing.Meta + +@[expose] public section namespace Lean4Lean namespace VEnv diff --git a/Lean4Lean/Theory/Typing/Strong.lean b/Lean4Lean/Theory/Typing/Strong.lean index 3695e893..9546d099 100644 --- a/Lean4Lean/Theory/Typing/Strong.lean +++ b/Lean4Lean/Theory/Typing/Strong.lean @@ -1,4 +1,8 @@ -import Lean4Lean.Theory.Typing.Lemmas +module + +public import Lean4Lean.Theory.Typing.Lemmas + +@[expose] public section namespace Lean4Lean namespace VEnv diff --git a/Lean4Lean/Theory/Typing/UniqueTyping.lean b/Lean4Lean/Theory/Typing/UniqueTyping.lean index 90162770..f5fa385d 100644 --- a/Lean4Lean/Theory/Typing/UniqueTyping.lean +++ b/Lean4Lean/Theory/Typing/UniqueTyping.lean @@ -1,5 +1,9 @@ -import Lean4Lean.Theory.Typing.Injectivity -import Lean4Lean.Theory.Typing.Pattern +module + +public import Lean4Lean.Theory.Typing.Injectivity +public import Lean4Lean.Theory.Typing.Pattern + +@[expose] public section /-! # Unique typing and its consequences. -/ diff --git a/Lean4Lean/Theory/VDecl.lean b/Lean4Lean/Theory/VDecl.lean index 1dfdea0e..9a76bcdf 100644 --- a/Lean4Lean/Theory/VDecl.lean +++ b/Lean4Lean/Theory/VDecl.lean @@ -1,4 +1,8 @@ -import Lean4Lean.Theory.VEnv +module + +public import Lean4Lean.Theory.VEnv + +@[expose] public section namespace Lean4Lean diff --git a/Lean4Lean/Theory/VEnv.lean b/Lean4Lean/Theory/VEnv.lean index b0780ee9..08865ca0 100644 --- a/Lean4Lean/Theory/VEnv.lean +++ b/Lean4Lean/Theory/VEnv.lean @@ -1,4 +1,8 @@ -import Lean4Lean.Theory.VExpr +module + +public import Lean4Lean.Theory.VExpr + +@[expose] public section namespace Lean4Lean diff --git a/Lean4Lean/Theory/VExpr.lean b/Lean4Lean/Theory/VExpr.lean index ab1797c6..58519f35 100644 --- a/Lean4Lean/Theory/VExpr.lean +++ b/Lean4Lean/Theory/VExpr.lean @@ -1,5 +1,9 @@ -import Lean -import Lean4Lean.Theory.VLevel +module + +public import Lean +public import Lean4Lean.Theory.VLevel + +@[expose] public section namespace Lean4Lean diff --git a/Lean4Lean/Theory/VLevel.lean b/Lean4Lean/Theory/VLevel.lean index 51ec2732..1b09bd94 100644 --- a/Lean4Lean/Theory/VLevel.lean +++ b/Lean4Lean/Theory/VLevel.lean @@ -1,4 +1,8 @@ -import Lean4Lean.Std.Basic +module + +public import Lean4Lean.Std.Basic + +@[expose] public section namespace Lean4Lean diff --git a/Lean4Lean/TypeChecker.lean b/Lean4Lean/TypeChecker.lean index 9589739f..41ff23f1 100644 --- a/Lean4Lean/TypeChecker.lean +++ b/Lean4Lean/TypeChecker.lean @@ -1,10 +1,14 @@ -import Lean4Lean.Declaration -import Lean4Lean.Level -import Lean4Lean.Quot -import Lean4Lean.Inductive.Reduce -import Lean4Lean.Instantiate -import Lean4Lean.ForEachExprV -import Lean4Lean.EquivManager +module + +public import Lean4Lean.Declaration +public import Lean4Lean.Level +public import Lean4Lean.Quot +public import Lean4Lean.Inductive.Reduce +public import Lean4Lean.Instantiate +public import Lean4Lean.ForEachExprV +public import Lean4Lean.EquivManager + +@[expose] public section namespace Lean4Lean open Lean hiding Environment Exception diff --git a/Lean4Lean/Verify.lean b/Lean4Lean/Verify.lean index d9faa29f..6bdb4fee 100644 --- a/Lean4Lean/Verify.lean +++ b/Lean4Lean/Verify.lean @@ -1 +1,3 @@ +module +prelude import Lean4Lean.Verify.Typing.Lemmas diff --git a/Lean4Lean/Verify/Axioms.lean b/Lean4Lean/Verify/Axioms.lean index b18475d0..a9b0458b 100644 --- a/Lean4Lean/Verify/Axioms.lean +++ b/Lean4Lean/Verify/Axioms.lean @@ -1,6 +1,10 @@ -import Batteries.Tactic.OpenPrivate -import Lean4Lean.Std.Basic -import Lean4Lean.Std.NodupKeys +module + +public import Batteries.Tactic.OpenPrivate +public import Lean4Lean.Std.Basic +public import Lean4Lean.Std.NodupKeys + +@[expose] public section namespace Std.TreeMap diff --git a/Lean4Lean/Verify/Environment/Basic.lean b/Lean4Lean/Verify/Environment/Basic.lean index c78134a7..f1d6accb 100644 --- a/Lean4Lean/Verify/Environment/Basic.lean +++ b/Lean4Lean/Verify/Environment/Basic.lean @@ -1,5 +1,9 @@ -import Lean4Lean.Verify.LocalContext -import Lean4Lean.Theory.Typing.EnvLemmas +module + +public import Lean4Lean.Verify.LocalContext +public import Lean4Lean.Theory.Typing.EnvLemmas + +@[expose] public section namespace Lean4Lean open Lean hiding Environment Exception diff --git a/Lean4Lean/Verify/Environment/Lemmas.lean b/Lean4Lean/Verify/Environment/Lemmas.lean index 1bf8582d..d450a5a1 100644 --- a/Lean4Lean/Verify/Environment/Lemmas.lean +++ b/Lean4Lean/Verify/Environment/Lemmas.lean @@ -1,5 +1,9 @@ -import Lean4Lean.Std.SMap -import Lean4Lean.Verify.Environment.Basic +module + +public import Lean4Lean.Std.SMap +public import Lean4Lean.Verify.Environment.Basic + +@[expose] public section namespace Lean4Lean open Lean hiding Environment Exception diff --git a/Lean4Lean/Verify/EquivManager.lean b/Lean4Lean/Verify/EquivManager.lean index 31a07b2e..d40bc490 100644 --- a/Lean4Lean/Verify/EquivManager.lean +++ b/Lean4Lean/Verify/EquivManager.lean @@ -1,7 +1,11 @@ -import Batteries.Data.UnionFind.Lemmas -import Lean4Lean.Verify.Environment.Lemmas -import Lean4Lean.EquivManager -import Lean4Lean.Verify.TypeChecker.Basic +module + +public import Batteries.Data.UnionFind.Lemmas +public import Lean4Lean.Verify.Environment.Lemmas +public import Lean4Lean.EquivManager +public import Lean4Lean.Verify.TypeChecker.Basic + +@[expose] public section namespace Lean4Lean.EquivManager open Lean hiding Environment Exception diff --git a/Lean4Lean/Verify/Expr.lean b/Lean4Lean/Verify/Expr.lean index 4f62f2a8..41c6da56 100644 --- a/Lean4Lean/Verify/Expr.lean +++ b/Lean4Lean/Verify/Expr.lean @@ -1,10 +1,14 @@ -import Lean4Lean.Std.Basic -import Lean4Lean.Verify.Axioms -import Lean4Lean.Verify.Level -import Lean4Lean.Expr -import Lean4Lean.Instantiate -import Batteries.Data.String.Lemmas -import Std.Tactic.BVDecide +module + +public import Lean4Lean.Std.Basic +public import Lean4Lean.Verify.Axioms +public import Lean4Lean.Verify.Level +public import Lean4Lean.Expr +public import Lean4Lean.Instantiate +public import Batteries.Data.String.Lemmas +public import Std.Tactic.BVDecide + +@[expose] public section namespace Lean diff --git a/Lean4Lean/Verify/Level.lean b/Lean4Lean/Verify/Level.lean index df08aa3e..c9c3e95e 100644 --- a/Lean4Lean/Verify/Level.lean +++ b/Lean4Lean/Verify/Level.lean @@ -1,8 +1,12 @@ -import Lean4Lean.Theory.VLevel -import Lean4Lean.Level -import Lean4Lean.Verify.Axioms -import Std.Tactic.BVDecide -import Std.Data.TreeMap.Lemmas +module + +public import Lean4Lean.Theory.VLevel +public import Lean4Lean.Level +public import Lean4Lean.Verify.Axioms +public import Std.Tactic.BVDecide +public import Std.Data.TreeMap.Lemmas + +@[expose] public section namespace Lean diff --git a/Lean4Lean/Verify/LocalContext.lean b/Lean4Lean/Verify/LocalContext.lean index 7182d2d6..c671651d 100644 --- a/Lean4Lean/Verify/LocalContext.lean +++ b/Lean4Lean/Verify/LocalContext.lean @@ -1,7 +1,11 @@ -import Lean4Lean.Std.PersistentHashMap -import Lean4Lean.Verify.Expr -import Lean4Lean.Verify.Typing.Expr -import Lean4Lean.Verify.Typing.Lemmas +module + +public import Lean4Lean.Std.PersistentHashMap +public import Lean4Lean.Verify.Expr +public import Lean4Lean.Verify.Typing.Expr +public import Lean4Lean.Verify.Typing.Lemmas + +@[expose] public section namespace Lean.LocalContext diff --git a/Lean4Lean/Verify/NameGenerator.lean b/Lean4Lean/Verify/NameGenerator.lean index 02a6c991..b9d48b98 100644 --- a/Lean4Lean/Verify/NameGenerator.lean +++ b/Lean4Lean/Verify/NameGenerator.lean @@ -1,5 +1,9 @@ -import Lean4Lean.Expr -import Lean4Lean.Theory.VExpr +module + +public import Lean4Lean.Expr +public import Lean4Lean.Theory.VExpr + +@[expose] public section namespace Lean.NameGenerator diff --git a/Lean4Lean/Verify/TypeChecker.lean b/Lean4Lean/Verify/TypeChecker.lean index 166209c6..ea59d649 100644 --- a/Lean4Lean/Verify/TypeChecker.lean +++ b/Lean4Lean/Verify/TypeChecker.lean @@ -1,6 +1,10 @@ -import Lean4Lean.Verify.TypeChecker.InferType -import Lean4Lean.Verify.TypeChecker.WHNF -import Lean4Lean.Verify.TypeChecker.IsDefEq +module + +public import Lean4Lean.Verify.TypeChecker.InferType +public import Lean4Lean.Verify.TypeChecker.WHNF +public import Lean4Lean.Verify.TypeChecker.IsDefEq + +@[expose] public section namespace Lean4Lean diff --git a/Lean4Lean/Verify/TypeChecker/Basic.lean b/Lean4Lean/Verify/TypeChecker/Basic.lean index 011d403a..2db7eae5 100644 --- a/Lean4Lean/Verify/TypeChecker/Basic.lean +++ b/Lean4Lean/Verify/TypeChecker/Basic.lean @@ -1,6 +1,10 @@ -import Lean4Lean.Verify.Environment.Lemmas -import Lean4Lean.Verify.Typing.ConditionallyTyped -import Lean4Lean.TypeChecker +module + +public import Lean4Lean.Verify.Environment.Lemmas +public import Lean4Lean.Verify.Typing.ConditionallyTyped +public import Lean4Lean.TypeChecker + +@[expose] public section namespace Except diff --git a/Lean4Lean/Verify/TypeChecker/InferType.lean b/Lean4Lean/Verify/TypeChecker/InferType.lean index df7efd60..01b436da 100644 --- a/Lean4Lean/Verify/TypeChecker/InferType.lean +++ b/Lean4Lean/Verify/TypeChecker/InferType.lean @@ -1,5 +1,9 @@ -import Lean4Lean.Verify.TypeChecker.Reduce -import Lean4Lean.Verify.EquivManager +module + +public import Lean4Lean.Verify.TypeChecker.Reduce +public import Lean4Lean.Verify.EquivManager + +@[expose] public section namespace Lean4Lean.TypeChecker.Inner open Lean hiding Environment Exception diff --git a/Lean4Lean/Verify/TypeChecker/IsDefEq.lean b/Lean4Lean/Verify/TypeChecker/IsDefEq.lean index fa8a683f..d213a742 100644 --- a/Lean4Lean/Verify/TypeChecker/IsDefEq.lean +++ b/Lean4Lean/Verify/TypeChecker/IsDefEq.lean @@ -1,5 +1,9 @@ -import Lean4Lean.Verify.TypeChecker.Reduce -import Lean4Lean.Verify.EquivManager +module + +public import Lean4Lean.Verify.TypeChecker.Reduce +public import Lean4Lean.Verify.EquivManager + +@[expose] public section namespace Lean4Lean.TypeChecker.Inner open Lean hiding Environment Exception diff --git a/Lean4Lean/Verify/TypeChecker/Reduce.lean b/Lean4Lean/Verify/TypeChecker/Reduce.lean index 9ab93145..0bc5479b 100644 --- a/Lean4Lean/Verify/TypeChecker/Reduce.lean +++ b/Lean4Lean/Verify/TypeChecker/Reduce.lean @@ -1,4 +1,8 @@ -import Lean4Lean.Verify.TypeChecker.Basic +module + +public import Lean4Lean.Verify.TypeChecker.Basic + +@[expose] public section namespace Lean4Lean.TypeChecker.Inner open Lean hiding Environment Exception diff --git a/Lean4Lean/Verify/TypeChecker/WHNF.lean b/Lean4Lean/Verify/TypeChecker/WHNF.lean index 929570c6..bc3d3f6c 100644 --- a/Lean4Lean/Verify/TypeChecker/WHNF.lean +++ b/Lean4Lean/Verify/TypeChecker/WHNF.lean @@ -1,4 +1,8 @@ -import Lean4Lean.Verify.TypeChecker.Reduce +module + +public import Lean4Lean.Verify.TypeChecker.Reduce + +@[expose] public section namespace Lean4Lean.TypeChecker.Inner open Lean hiding Environment Exception diff --git a/Lean4Lean/Verify/Typing/ConditionallyTyped.lean b/Lean4Lean/Verify/Typing/ConditionallyTyped.lean index 4d339d60..011b251c 100644 --- a/Lean4Lean/Verify/Typing/ConditionallyTyped.lean +++ b/Lean4Lean/Verify/Typing/ConditionallyTyped.lean @@ -1,4 +1,8 @@ -import Lean4Lean.Verify.Typing.Lemmas +module + +public import Lean4Lean.Verify.Typing.Lemmas + +@[expose] public section namespace Lean4Lean open VEnv Lean diff --git a/Lean4Lean/Verify/Typing/Expr.lean b/Lean4Lean/Verify/Typing/Expr.lean index a572fabd..3cdd0a19 100644 --- a/Lean4Lean/Verify/Typing/Expr.lean +++ b/Lean4Lean/Verify/Typing/Expr.lean @@ -1,7 +1,11 @@ -import Lean4Lean.Theory.Typing.Basic -import Lean4Lean.Verify.NameGenerator -import Lean4Lean.Verify.VLCtx -import Lean4Lean.Verify.Axioms +module + +public import Lean4Lean.Theory.Typing.Basic +public import Lean4Lean.Verify.NameGenerator +public import Lean4Lean.Verify.VLCtx +public import Lean4Lean.Verify.Axioms + +@[expose] public section namespace Lean4Lean open Lean diff --git a/Lean4Lean/Verify/Typing/Lemmas.lean b/Lean4Lean/Verify/Typing/Lemmas.lean index 749130d1..1a3769a9 100644 --- a/Lean4Lean/Verify/Typing/Lemmas.lean +++ b/Lean4Lean/Verify/Typing/Lemmas.lean @@ -1,9 +1,13 @@ -import Batteries.Data.String.Lemmas -import Lean4Lean.Verify.Typing.Expr -import Lean4Lean.Verify.Expr -import Lean4Lean.Theory.Typing.Strong -import Lean4Lean.Theory.Typing.UniqueTyping -import Lean4Lean.Instantiate +module + +public import Batteries.Data.String.Lemmas +public import Lean4Lean.Verify.Typing.Expr +public import Lean4Lean.Verify.Expr +public import Lean4Lean.Theory.Typing.Strong +public import Lean4Lean.Theory.Typing.UniqueTyping +public import Lean4Lean.Instantiate + +@[expose] public section namespace Lean4Lean open VEnv Lean diff --git a/Lean4Lean/Verify/VLCtx.lean b/Lean4Lean/Verify/VLCtx.lean index f6c6d08c..973ef823 100644 --- a/Lean4Lean/Verify/VLCtx.lean +++ b/Lean4Lean/Verify/VLCtx.lean @@ -1,5 +1,9 @@ -import Lean4Lean.Verify.Expr -import Lean4Lean.Theory.VExpr +module + +public import Lean4Lean.Verify.Expr +public import Lean4Lean.Theory.VExpr + +@[expose] public section namespace Lean4Lean diff --git a/Main.lean b/Main.lean index 830d63a1..9e007494 100644 --- a/Main.lean +++ b/Main.lean @@ -1,12 +1,16 @@ +module + /- Copyright (c) 2023 Scott Morrison. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison -/ -import Lean.CoreM -import Lean.Util.FoldConsts -import Lean4Lean.Environment -import Lake.Load.Manifest +public import Lean.CoreM +public import Lean.Util.FoldConsts +public import Lean4Lean.Environment +public import Lake.Load.Manifest + +@[expose] public section namespace Lean