Documentation
Lean.Meta.Structure
Google site search
Lean.Meta.Structure
source
Imports
Init
Lean.Structure
Lean.Meta.AppBuilder
Imported by
Lean.Meta
Lean.Elab.StructInst
Lean.Elab.Structure
Lean.Meta.getStructureName
source
def
Lean.Meta.getStructureName
(struct :
Lean.Expr
)
:
Lean.MetaM
Lean.Name
Equations
One or more equations did not get rendered due to their size.
General documentation
index
Library
Init
Init.Control
Init.Control.Basic
Init.Control.EState
Init.Control.Except
Init.Control.ExceptCps
Init.Control.Id
Init.Control.Lawful
Init.Control.Option
Init.Control.Reader
Init.Control.State
Init.Control.StateCps
Init.Control.StateRef
Init.Data
Init.Data.Array
Init.Data.Array.Basic
Init.Data.Array.BasicAux
Init.Data.Array.BinSearch
Init.Data.Array.DecidableEq
Init.Data.Array.InsertionSort
Init.Data.Array.Mem
Init.Data.Array.QSort
Init.Data.Array.Subarray
Init.Data.ByteArray
Init.Data.ByteArray.Basic
Init.Data.Char
Init.Data.Char.Basic
Init.Data.Fin
Init.Data.Fin.Basic
Init.Data.FloatArray
Init.Data.FloatArray.Basic
Init.Data.Format
Init.Data.Format.Basic
Init.Data.Format.Instances
Init.Data.Format.Macro
Init.Data.Format.Syntax
Init.Data.Int
Init.Data.Int.Basic
Init.Data.List
Init.Data.List.Basic
Init.Data.List.BasicAux
Init.Data.List.Control
Init.Data.Nat
Init.Data.Nat.Basic
Init.Data.Nat.Bitwise
Init.Data.Nat.Control
Init.Data.Nat.Div
Init.Data.Nat.Gcd
Init.Data.Nat.Linear
Init.Data.Nat.Log2
Init.Data.Nat.SOM
Init.Data.Option
Init.Data.Option.Basic
Init.Data.Option.BasicAux
Init.Data.Option.Instances
Init.Data.String
Init.Data.String.Basic
Init.Data.String.Extra
Init.Data.ToString
Init.Data.ToString.Basic
Init.Data.ToString.Macro
Init.Data.AC
Init.Data.Basic
Init.Data.Float
Init.Data.Hashable
Init.Data.OfScientific
Init.Data.Ord
Init.Data.Prod
Init.Data.Random
Init.Data.Range
Init.Data.Repr
Init.Data.Stream
Init.Data.UInt
Init.System
Init.System.FilePath
Init.System.IO
Init.System.IOError
Init.System.Platform
Init.System.ST
Init.Classical
Init.Coe
Init.Conv
Init.Core
Init.Hints
Init.Meta
Init.Notation
Init.NotationExtra
Init.Prelude
Init.SimpLemmas
Init.SizeOf
Init.SizeOfLemmas
Init.Tactics
Init.Util
Init.WF
Init.WFTactics
Lean
Lean.Compiler
Lean.Compiler.IR
Lean.Compiler.IR.Basic
Lean.Compiler.IR.Borrow
Lean.Compiler.IR.Boxing
Lean.Compiler.IR.Checker
Lean.Compiler.IR.CompilerM
Lean.Compiler.IR.CtorLayout
Lean.Compiler.IR.ElimDeadBranches
Lean.Compiler.IR.ElimDeadVars
Lean.Compiler.IR.EmitC
Lean.Compiler.IR.EmitUtil
Lean.Compiler.IR.ExpandResetReuse
Lean.Compiler.IR.Format
Lean.Compiler.IR.FreeVars
Lean.Compiler.IR.LiveVars
Lean.Compiler.IR.NormIds
Lean.Compiler.IR.PushProj
Lean.Compiler.IR.RC
Lean.Compiler.IR.ResetReuse
Lean.Compiler.IR.SimpCase
Lean.Compiler.IR.Sorry
Lean.Compiler.IR.UnboxResult
Lean.Compiler.BorrowedAnnotation
Lean.Compiler.CSimpAttr
Lean.Compiler.ClosedTermCache
Lean.Compiler.ConstFolding
Lean.Compiler.ExportAttr
Lean.Compiler.ExternAttr
Lean.Compiler.FFI
Lean.Compiler.ImplementedByAttr
Lean.Compiler.InitAttr
Lean.Compiler.InlineAttrs
Lean.Compiler.NameMangling
Lean.Compiler.NeverExtractAttr
Lean.Compiler.NoncomputableAttr
Lean.Compiler.Specialize
Lean.Compiler.Util
Lean.Data
Lean.Data.Json
Lean.Data.Json.Basic
Lean.Data.Json.FromToJson
Lean.Data.Json.Parser
Lean.Data.Json.Printer
Lean.Data.Json.Stream
Lean.Data.Lsp
Lean.Data.Lsp.Basic
Lean.Data.Lsp.Capabilities
Lean.Data.Lsp.Client
Lean.Data.Lsp.Communication
Lean.Data.Lsp.Diagnostics
Lean.Data.Lsp.Extra
Lean.Data.Lsp.InitShutdown
Lean.Data.Lsp.Internal
Lean.Data.Lsp.Ipc
Lean.Data.Lsp.LanguageFeatures
Lean.Data.Lsp.TextSync
Lean.Data.Lsp.Utf16
Lean.Data.Lsp.Workspace
Lean.Data.Xml
Lean.Data.Xml.Basic
Lean.Data.Xml.Parser
Lean.Data.Format
Lean.Data.FuzzyMatching
Lean.Data.JsonRpc
Lean.Data.KVMap
Lean.Data.LBool
Lean.Data.LOption
Lean.Data.Name
Lean.Data.NameTrie
Lean.Data.Occurrences
Lean.Data.OpenDecl
Lean.Data.Options
Lean.Data.Parsec
Lean.Data.Position
Lean.Data.PrefixTree
Lean.Data.Rat
Lean.Data.SMap
Lean.Data.SSet
Lean.Data.Trie
Lean.Elab
Lean.Elab.Deriving
Lean.Elab.Deriving.BEq
Lean.Elab.Deriving.Basic
Lean.Elab.Deriving.DecEq
Lean.Elab.Deriving.FromToJson
Lean.Elab.Deriving.Hashable
Lean.Elab.Deriving.Inhabited
Lean.Elab.Deriving.Ord
Lean.Elab.Deriving.Repr
Lean.Elab.Deriving.SizeOf
Lean.Elab.Deriving.Util
Lean.Elab.PreDefinition
Lean.Elab.PreDefinition.Structural
Lean.Elab.PreDefinition.Structural.BRecOn
Lean.Elab.PreDefinition.Structural.Basic
Lean.Elab.PreDefinition.Structural.Eqns
Lean.Elab.PreDefinition.Structural.FindRecArg
Lean.Elab.PreDefinition.Structural.IndPred
Lean.Elab.PreDefinition.Structural.Main
Lean.Elab.PreDefinition.Structural.Preprocess
Lean.Elab.PreDefinition.Structural.SmartUnfolding
Lean.Elab.PreDefinition.WF
Lean.Elab.PreDefinition.WF.Eqns
Lean.Elab.PreDefinition.WF.Fix
Lean.Elab.PreDefinition.WF.Ite
Lean.Elab.PreDefinition.WF.Main
Lean.Elab.PreDefinition.WF.PackDomain
Lean.Elab.PreDefinition.WF.PackMutual
Lean.Elab.PreDefinition.WF.Rel
Lean.Elab.PreDefinition.WF.TerminationHint
Lean.Elab.PreDefinition.Basic
Lean.Elab.PreDefinition.Eqns
Lean.Elab.PreDefinition.Main
Lean.Elab.PreDefinition.MkInhabitant
Lean.Elab.Quotation
Lean.Elab.Quotation.Precheck
Lean.Elab.Quotation.Util
Lean.Elab.Tactic
Lean.Elab.Tactic.Conv
Lean.Elab.Tactic.Conv.Basic
Lean.Elab.Tactic.Conv.Change
Lean.Elab.Tactic.Conv.Congr
Lean.Elab.Tactic.Conv.Delta
Lean.Elab.Tactic.Conv.Pattern
Lean.Elab.Tactic.Conv.Rewrite
Lean.Elab.Tactic.Conv.Simp
Lean.Elab.Tactic.Conv.Unfold
Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.Cache
Lean.Elab.Tactic.Config
Lean.Elab.Tactic.Delta
Lean.Elab.Tactic.ElabTerm
Lean.Elab.Tactic.Generalize
Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.Injection
Lean.Elab.Tactic.Location
Lean.Elab.Tactic.Match
Lean.Elab.Tactic.Meta
Lean.Elab.Tactic.Rewrite
Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.Split
Lean.Elab.Tactic.Unfold
Lean.Elab.App
Lean.Elab.Arg
Lean.Elab.Attributes
Lean.Elab.AutoBound
Lean.Elab.AuxDef
Lean.Elab.AuxDiscr
Lean.Elab.Binders
Lean.Elab.BindersUtil
Lean.Elab.BuiltinCommand
Lean.Elab.BuiltinNotation
Lean.Elab.BuiltinTerm
Lean.Elab.Command
Lean.Elab.Config
Lean.Elab.DeclModifiers
Lean.Elab.DeclUtil
Lean.Elab.Declaration
Lean.Elab.DeclarationRange
Lean.Elab.DefView
Lean.Elab.Do
Lean.Elab.ElabRules
Lean.Elab.Eval
Lean.Elab.Exception
Lean.Elab.Extra
Lean.Elab.Frontend
Lean.Elab.GenInjective
Lean.Elab.Import
Lean.Elab.Inductive
Lean.Elab.InfoTree
Lean.Elab.LetRec
Lean.Elab.Level
Lean.Elab.Macro
Lean.Elab.MacroArgUtil
Lean.Elab.MacroRules
Lean.Elab.Match
Lean.Elab.MatchAltView
Lean.Elab.Mixfix
Lean.Elab.MutualDef
Lean.Elab.Notation
Lean.Elab.Open
Lean.Elab.PatternVar
Lean.Elab.Print
Lean.Elab.RecAppSyntax
Lean.Elab.SetOption
Lean.Elab.StructInst
Lean.Elab.Structure
Lean.Elab.Syntax
Lean.Elab.SyntheticMVars
Lean.Elab.Term
Lean.Elab.Util
Lean.Linter
Lean.Linter.Basic
Lean.Linter.Util
Lean.Meta
Lean.Meta.Match
Lean.Meta.Match.Basic
Lean.Meta.Match.CaseArraySizes
Lean.Meta.Match.CaseValues
Lean.Meta.Match.MVarRenaming
Lean.Meta.Match.Match
Lean.Meta.Match.MatchEqs
Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.MatchPatternAttr
Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Value
Lean.Meta.Tactic
Lean.Meta.Tactic.AC
Lean.Meta.Tactic.AC.Main
Lean.Meta.Tactic.LinearArith
Lean.Meta.Tactic.LinearArith.Nat
Lean.Meta.Tactic.LinearArith.Nat.Basic
Lean.Meta.Tactic.LinearArith.Nat.Simp
Lean.Meta.Tactic.LinearArith.Nat.Solver
Lean.Meta.Tactic.LinearArith.Basic
Lean.Meta.Tactic.LinearArith.Main
Lean.Meta.Tactic.LinearArith.Simp
Lean.Meta.Tactic.LinearArith.Solver
Lean.Meta.Tactic.Simp
Lean.Meta.Tactic.Simp.Main
Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.Tactic.Simp.Types
Lean.Meta.Tactic.Acyclic
Lean.Meta.Tactic.Apply
Lean.Meta.Tactic.Assert
Lean.Meta.Tactic.Assumption
Lean.Meta.Tactic.AuxLemma
Lean.Meta.Tactic.Cases
Lean.Meta.Tactic.Cleanup
Lean.Meta.Tactic.Clear
Lean.Meta.Tactic.Constructor
Lean.Meta.Tactic.Contradiction
Lean.Meta.Tactic.Delta
Lean.Meta.Tactic.ElimInfo
Lean.Meta.Tactic.FVarSubst
Lean.Meta.Tactic.Generalize
Lean.Meta.Tactic.Induction
Lean.Meta.Tactic.Injection
Lean.Meta.Tactic.Intro
Lean.Meta.Tactic.Refl
Lean.Meta.Tactic.Rename
Lean.Meta.Tactic.Replace
Lean.Meta.Tactic.Revert
Lean.Meta.Tactic.Rewrite
Lean.Meta.Tactic.Split
Lean.Meta.Tactic.SplitIf
Lean.Meta.Tactic.Subst
Lean.Meta.Tactic.Unfold
Lean.Meta.Tactic.UnifyEq
Lean.Meta.Tactic.Util
Lean.Meta.ACLt
Lean.Meta.AbstractMVars
Lean.Meta.AbstractNestedProofs
Lean.Meta.AppBuilder
Lean.Meta.Basic
Lean.Meta.CasesOn
Lean.Meta.Check
Lean.Meta.Closure
Lean.Meta.Coe
Lean.Meta.CollectFVars
Lean.Meta.CollectMVars
Lean.Meta.CongrTheorems
Lean.Meta.Constructions
Lean.Meta.DecLevel
Lean.Meta.DiscrTree
Lean.Meta.DiscrTreeTypes
Lean.Meta.Eqns
Lean.Meta.Eval
Lean.Meta.ExprDefEq
Lean.Meta.ExprLens
Lean.Meta.ExprTraverse
Lean.Meta.ForEachExpr
Lean.Meta.FunInfo
Lean.Meta.GeneralizeTelescope
Lean.Meta.GeneralizeVars
Lean.Meta.GetConst
Lean.Meta.GlobalInstances
Lean.Meta.IndPredBelow
Lean.Meta.Inductive
Lean.Meta.InferType
Lean.Meta.Injective
Lean.Meta.Instances
Lean.Meta.KAbstract
Lean.Meta.KExprMap
Lean.Meta.LevelDefEq
Lean.Meta.MatchUtil
Lean.Meta.Offset
Lean.Meta.PPGoal
Lean.Meta.RecursorInfo
Lean.Meta.Reduce
Lean.Meta.ReduceEval
Lean.Meta.SizeOf
Lean.Meta.Structure
Lean.Meta.SynthInstance
Lean.Meta.Transform
Lean.Meta.TransparencyMode
Lean.Meta.UnificationHint
Lean.Meta.WHNF
Lean.Parser
Lean.Parser.Attr
Lean.Parser.Basic
Lean.Parser.Command
Lean.Parser.Do
Lean.Parser.Extension
Lean.Parser.Extra
Lean.Parser.Level
Lean.Parser.Module
Lean.Parser.StrInterpolation
Lean.Parser.Syntax
Lean.Parser.Tactic
Lean.Parser.Term
Lean.ParserCompiler
Lean.ParserCompiler.Attribute
Lean.PrettyPrinter
Lean.PrettyPrinter.Delaborator
Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.Options
Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Basic
Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Parenthesizer
Lean.Server
Lean.Server.FileWorker
Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.WidgetRequests
Lean.Server.Rpc
Lean.Server.Rpc.Basic
Lean.Server.Rpc.Deriving
Lean.Server.Rpc.RequestHandling
Lean.Server.AsyncList
Lean.Server.Completion
Lean.Server.FileSource
Lean.Server.GoTo
Lean.Server.InfoUtils
Lean.Server.References
Lean.Server.Requests
Lean.Server.Snapshots
Lean.Server.Utils
Lean.Server.Watchdog
Lean.Util
Lean.Util.CollectFVars
Lean.Util.CollectLevelParams
Lean.Util.CollectMVars
Lean.Util.FindExpr
Lean.Util.FindLevelMVar
Lean.Util.FindMVar
Lean.Util.FoldConsts
Lean.Util.ForEachExpr
Lean.Util.HasConstCache
Lean.Util.MonadBacktrack
Lean.Util.MonadCache
Lean.Util.OccursCheck
Lean.Util.PPExt
Lean.Util.Path
Lean.Util.Paths
Lean.Util.Profile
Lean.Util.RecDepth
Lean.Util.Recognizers
Lean.Util.ReplaceExpr
Lean.Util.ReplaceLevel
Lean.Util.SCC
Lean.Util.Sorry
Lean.Util.Trace
Lean.Widget
Lean.Widget.Basic
Lean.Widget.InteractiveCode
Lean.Widget.InteractiveDiagnostic
Lean.Widget.InteractiveGoal
Lean.Widget.TaggedText
Lean.Attributes
Lean.AuxRecursor
Lean.Class
Lean.CoreM
Lean.Declaration
Lean.DeclarationRange
Lean.DocString
Lean.Environment
Lean.Eval
Lean.Exception
Lean.Expr
Lean.HeadIndex
Lean.Hygiene
Lean.ImportingFlag
Lean.InternalExceptionId
Lean.KeyedDeclsAttribute
Lean.LazyInitExtension
Lean.Level
Lean.LoadDynlib
Lean.LocalContext
Lean.Log
Lean.Message
Lean.MetavarContext
Lean.Modifiers
Lean.MonadEnv
Lean.ProjFns
Lean.ReducibilityAttrs
Lean.ResolveName
Lean.Runtime
Lean.ScopedEnvExtension
Lean.Structure
Lean.SubExpr
Lean.Syntax
Lean.ToExpr
Mathlib
Mathlib.Util
Mathlib.Util.IncludeStr
Std
Std.Data
Std.Data.AssocList
Std.Data.HashMap
Std.Data.HashSet
Std.Data.PersistentArray
Std.Data.PersistentHashMap
Std.Data.PersistentHashSet
Std.Data.RBMap
Std.Data.RBTree
Std.ShareCommon
Unicode
Unicode.General
Unicode.General.GeneralCategory
Unicode.General.Name
Unicode.Includes