| /- | |
| Copyright (c) 2020 Microsoft Corporation. All rights reserved. | |
| Released under Apache 2.0 license as described in the file LICENSE. | |
| Authors: Leonardo de Moura | |
| -/ | |
| import Lean.Util.CollectFVars | |
| import Lean.Util.CollectLevelParams | |
| import Lean.Util.CollectMVars | |
| import Lean.Util.FindMVar | |
| import Lean.Util.FindLevelMVar | |
| import Lean.Util.MonadCache | |
| import Lean.Util.PPExt | |
| import Lean.Util.Path | |
| import Lean.Util.Profile | |
| import Lean.Util.RecDepth | |
| import Lean.Util.Sorry | |
| import Lean.Util.Trace | |
| import Lean.Util.FindExpr | |
| import Lean.Util.ReplaceExpr | |
| import Lean.Util.ForEachExpr | |
| import Lean.Util.ReplaceLevel | |
| import Lean.Util.FoldConsts | |
| import Lean.Util.SCC | |
| import Lean.Util.OccursCheck | |
| import Lean.Util.Paths | |
| import Lean.Util.HasConstCache |