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.Channel

Init.Data.Float

Init.Data.Hashable

Init.Data.OfScientific

Init.Data.Ord

Init.Data.Prod

Init.Data.Queue

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.Mutex

Init.System.Platform

Init.System.Promise

Init.System.ST

Init.System.Uri

Init.Classical

Init.Coe

Init.Conv

Init.Core

Init.Dynamic

Init.Hints

Init.Meta

Init.Notation

Init.NotationExtra

Init.Prelude

Init.ShareCommon

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.LCNF

Lean.Compiler.LCNF.Simp

Lean.Compiler.LCNF.Simp.Basic

Lean.Compiler.LCNF.Simp.Config

Lean.Compiler.LCNF.Simp.ConstantFold

Lean.Compiler.LCNF.Simp.DefaultAlt

Lean.Compiler.LCNF.Simp.FunDeclInfo

Lean.Compiler.LCNF.Simp.InlineCandidate

Lean.Compiler.LCNF.Simp.InlineProj

Lean.Compiler.LCNF.Simp.JpCases

Lean.Compiler.LCNF.Simp.Main

Lean.Compiler.LCNF.Simp.SimpM

Lean.Compiler.LCNF.Simp.SimpValue

Lean.Compiler.LCNF.Simp.Used

Lean.Compiler.LCNF.AlphaEqv

Lean.Compiler.LCNF.Basic

Lean.Compiler.LCNF.Bind

Lean.Compiler.LCNF.CSE

Lean.Compiler.LCNF.Check

Lean.Compiler.LCNF.CompilerM

Lean.Compiler.LCNF.ConfigOptions

Lean.Compiler.LCNF.DependsOn

Lean.Compiler.LCNF.ElimDead

Lean.Compiler.LCNF.FixedArgs

Lean.Compiler.LCNF.ForEachExpr

Lean.Compiler.LCNF.InferType

Lean.Compiler.LCNF.JoinPoints

Lean.Compiler.LCNF.LCtx

Lean.Compiler.LCNF.Level

Lean.Compiler.LCNF.Main

Lean.Compiler.LCNF.MonoTypes

Lean.Compiler.LCNF.OtherDecl

Lean.Compiler.LCNF.PassManager

Lean.Compiler.LCNF.Passes

Lean.Compiler.LCNF.PhaseExt

Lean.Compiler.LCNF.PrettyPrinter

Lean.Compiler.LCNF.PullFunDecls

Lean.Compiler.LCNF.PullLetDecls

Lean.Compiler.LCNF.ReduceJpArity

Lean.Compiler.LCNF.Renaming

Lean.Compiler.LCNF.SpecInfo

Lean.Compiler.LCNF.Specialize

Lean.Compiler.LCNF.Testing

Lean.Compiler.LCNF.ToDecl

Lean.Compiler.LCNF.ToExpr

Lean.Compiler.LCNF.ToLCNF

Lean.Compiler.LCNF.Types

Lean.Compiler.LCNF.Util

Lean.Compiler.AtMostOnce

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.Main

Lean.Compiler.NameMangling

Lean.Compiler.NeverExtractAttr

Lean.Compiler.NoncomputableAttr

Lean.Compiler.Old

Lean.Compiler.Options

Lean.Compiler.Specialize

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.CodeActions

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.AssocList

Lean.Data.Format

Lean.Data.FuzzyMatching

Lean.Data.HashMap

Lean.Data.HashSet

Lean.Data.JsonRpc

Lean.Data.KVMap

Lean.Data.LBool

Lean.Data.LOption

Lean.Data.Name

Lean.Data.NameMap

Lean.Data.NameTrie

Lean.Data.Occurrences

Lean.Data.OpenDecl

Lean.Data.Options

Lean.Data.Parsec

Lean.Data.PersistentArray

Lean.Data.PersistentHashMap

Lean.Data.PersistentHashSet

Lean.Data.Position

Lean.Data.PrefixTree

Lean.Data.RBMap

Lean.Data.RBTree

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.TypeName

Lean.Elab.Deriving.Util

Lean.Elab.InfoTree

Lean.Elab.InfoTree.Main

Lean.Elab.InfoTree.Types

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.Calc

Lean.Elab.Tactic.Config

Lean.Elab.Tactic.Congr

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.Calc

Lean.Elab.Command

Lean.Elab.ComputedFields

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.InheritDoc

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.Builtin

Lean.Linter.MissingDocs

Lean.Linter.UnusedVariables

Lean.Linter.Util

Lean.Meta

Lean.Meta.Match

Lean.Meta.Match.Basic

Lean.Meta.Match.CaseArraySizes

Lean.Meta.Match.CaseValues

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.Congr

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.ShareCommon

Lean.Util.Sorry

Lean.Util.Trace

Lean.Widget

Lean.Widget.Basic

Lean.Widget.Diff

Lean.Widget.InteractiveCode

Lean.Widget.InteractiveDiagnostic

Lean.Widget.InteractiveGoal

Lean.Widget.TaggedText

Lean.Widget.UserWidget

Lean.Attributes

Lean.AuxRecursor

Lean.Class

Lean.CoreM

Lean.Declaration

Lean.DeclarationRange

Lean.Deprecated

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

Mt

Mt.System

Mt.System.Basic

Mt.System.BasicAux

Mt.System.Traced

Mt.System.Validation

Mt.Task

Mt.Task.Basic

Mt.Task.Impl

Mt.Task.Validation

Mt.Thread

Mt.Thread.Basic

Mt.Thread.Traced

Mt.Utils

Mt.Utils.Fin

Mt.Utils.List

Mt.Utils.Nat

Mt.Reservation

Samples

Samples.sample

Samples.sample_mutex

Samples.sample_simple