0db89d65b2
This PR changes the terminology used from "premise selection" to "library suggestions". This will be more understandable to users (we don't assume anyone is familiar with the premise selection literature), and avoids a conflict with the existing use of "premise" in Lean terminology (e.g. "major premise" in induction, as well as generally the synonym for "hypothesis"/"argument").
50 lines
1.4 KiB
Text
50 lines
1.4 KiB
Text
/-
|
|
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Leonardo de Moura
|
|
-/
|
|
module
|
|
|
|
public import Lean.Data
|
|
public import Lean.Compiler
|
|
public import Lean.Environment
|
|
public import Lean.Modifiers
|
|
public import Lean.ProjFns
|
|
public import Lean.Runtime
|
|
public import Lean.ResolveName
|
|
public import Lean.Attributes
|
|
public import Lean.Parser
|
|
public import Lean.ReducibilityAttrs
|
|
public import Lean.Elab
|
|
public import Lean.Class
|
|
public import Lean.LocalContext
|
|
public import Lean.MetavarContext
|
|
public import Lean.AuxRecursor
|
|
public import Lean.Meta
|
|
public import Lean.Util
|
|
public import Lean.Structure
|
|
public import Lean.PrettyPrinter
|
|
public import Lean.CoreM
|
|
public import Lean.ReservedNameAction
|
|
public import Lean.InternalExceptionId
|
|
public import Lean.Server
|
|
public import Lean.ScopedEnvExtension
|
|
public import Lean.DocString
|
|
public import Lean.DeclarationRange
|
|
public import Lean.LoadDynlib
|
|
public import Lean.Widget
|
|
public import Lean.Log
|
|
public import Lean.Linter
|
|
public import Lean.SubExpr
|
|
public import Lean.LabelAttribute
|
|
public import Lean.AddDecl
|
|
public import Lean.Replay
|
|
public import Lean.PrivateName
|
|
public import Lean.LibrarySuggestions
|
|
public import Lean.Namespace
|
|
public import Lean.EnvExtension
|
|
public import Lean.ErrorExplanation
|
|
public import Lean.ErrorExplanations
|
|
public import Lean.DefEqAttrib
|
|
public import Lean.Shell
|
|
public import Lean.ExtraModUses
|