lean4-htt/src/Lean/Data.lean
Joachim Breitner 232a0495b0
chore: remove public section from end of files (#10684)
This PR removes `public section` lines from end of files; they look a
bit silly there.
2025-10-06 13:30:48 +00:00

32 lines
951 B
Text

/-
Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
-/
module
prelude
public import Lean.Data.AssocList
public import Lean.Data.Format
public import Lean.Data.Json
public import Lean.Data.JsonRpc
public import Lean.Data.KVMap
public import Lean.Data.LBool
public import Lean.Data.LOption
public import Lean.Data.Lsp
public import Lean.Data.Name
public import Lean.Data.NameMap
public import Lean.Data.OpenDecl
public import Lean.Data.Options
public import Lean.Data.PersistentArray
public import Lean.Data.PersistentHashMap
public import Lean.Data.PersistentHashSet
public import Lean.Data.Position
public import Lean.Data.PrefixTree
public import Lean.Data.SMap
public import Lean.Data.Trie
public import Lean.Data.Xml
public import Lean.Data.NameTrie
public import Lean.Data.RBTree
public import Lean.Data.RBMap
public import Lean.Data.RArray