Manual.lean

/-
Copyright (c) 2024 Lean FRO LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: David Thrane Christiansen
-/
import VersoManual

import Manual.Intro
import Manual.Elaboration
import Manual.Types
import Manual.Language
import Manual.RecursiveDefs
import Manual.Classes
import Manual.Terms
import Manual.Tactics
import Manual.Simp
import Manual.BasicTypes
import Manual.BasicProps
import Manual.NotationsMacros
import Manual.IO
import Manual.Interaction
import Manual.Monads
import Manual.BuildTools

open Verso.Genre Manual

set_option pp.rawOnError true

#doc (Manual) "The Lean Language Reference" =>
%%%
tag := "lean-language-reference"
%%%


This is the _Lean Language Reference_, an in-progress reference work on Lean.
It is intended to be a comprehensive, precise description of Lean: a reference work in which Lean users can look up detailed information, rather than a tutorial intended for new users.
For other documentation, please refer to the [Lean documentation site](https://lean-lang.org/documentation/).

This reference manual is not yet complete, but there's enough information to provide value to users.
The top priority is to add the missing information as quickly as possible while staying up to date with Lean development.
As the rest of the text is written, regular snapshots will be released, tracking upstream changes.
This snapshot covers Lean version {versionString}[].

Our prioritization of content is based on our best understanding of our users' needs.
Please use the [issue tracker](https://github.com/leanprover/reference-manual/issues) to help us better understand what you need to know.
In particular, please create or upvote issues for topics that are important to you.
Your feedback is much appreciated!
Once sufficient content is available, we will begin saving snapshots for each release of Lean and making them conveniently available.

API reference documentation is included from the Lean standard library source code.
Due to technical limitations at the moment, the Lean terms and examples embedded in it do not render as nicely as we would like.
In the near future, we will be working on removing these limitations.
Additionally, we will be adding missing API reference documentation and revising and improving the existing API reference documentation.

**Release History**

: 2025-02-03

  This release updates the contents for Lean version 4.17.0-rc1.
  It adds descriptions of {ref "well-founded-recursion"}[well-founded recursion], the new {ref "partial-fixpoint"}[partial fixpoint] feature, {ref "quotients"}[quotient types], and {ref "lake"}[Lake], and {ref "structural-recursion"}[the description of structural recursion] has been greatly improved.
  Descriptions and API references for all fixed-width integer types, {name}`Int`, {name}`Fin`, {name}`Empty`, and {name}`Option` were also added.
  This release also includes a quick-jump box that can be used to quickly navigate to any documented topic.

: 2024-12-16

  This is the initial release of the reference manual.

{include 0 Manual.Intro}

{include 0 Manual.Elaboration}

{include 0 Manual.Types}

{include 0 Manual.Interaction}

{include 0 Manual.Language}

{include 0 Manual.RecursiveDefs}

{include 0 Manual.Terms}

{include 0 Manual.Classes}

{include 0 Manual.Monads}

{include 0 Manual.IO}

{include 0 Manual.Tactics}

{include 0 Manual.Simp}

{include 0 Manual.BasicProps}

{include 0 Manual.BasicTypes}

# Standard Library
%%%
tag := "standard-library"
%%%


:::planned 109
Overview of the standard library, including types from the prelude and those that require imports.
:::

{include 0 Manual.NotationsMacros}

# Output from Lean

:::planned 122
 * {deftech}[Unexpanders]
 * {deftech key:="delaborate"}[Delaboration]
 * {deftech}[Pretty printing]
 * Parenthesizers
:::

# Elan
%%%
tag := "elan"
%%%


::: planned 74

This section will describe Elan and how to use it:

 * `lean-toolchain` files
 * `+`-syntax for toolchain selection
 * Specific overrides
 * Using a local development build of Lean with Elan
:::

{include 0 Manual.BuildTools}

# Index
%%%
number := false
file := some "the-index"
%%%

{theIndex}



::::::draft

:::progress
```namespace
List
Int
IntCast
Empty
PEmpty
Function
Ord
Ordering
Functor
Applicative
Monad
Pure
Bind
Seq
SeqLeft
SeqRight
MonadState
MonadStateOf
StateT
StateM
MonadReader
MonadReaderOf
ReaderT
ReaderM
MonadExcept
MonadExceptOf
ExceptT
Except
MonadFunctor
MonadFunctorT
MonadControl
MonadControlT
MonadLift
MonadLiftT
OptionT
StateRefT'
StateCpsT
ExceptCpsT
LawfulFunctor
LawfulApplicative
LawfulMonad
Id
Thunk
ForM
ForIn
ForInStep
ForIn'
EStateM
EStateM.Result
EStateM.Backtrackable
String
Char
Nat
Lean.Elab.Tactic
Array
Subarray
IO
IO.FS
System
System.FilePath
IO.Process
IO.FS.Stream
ST
IO.Error
IO.FS.Stream.Buffer
IO.FS.Handle
IO.Process.SpawnArgs
IO.Process.Output
IO.Process.Child
IO.Process.StdioConfig
IO.Process.Stdio
IO.Ref
ST.Ref
IO.FS.Metadata
IO.FS.DirEntry
EIO
BaseIO
IO.FileRight
IO.FS.Stream
Task
Task.Priority
Unit
PUnit
Bool
Decidable
System.Platform
PLift
ULift
Subtype
Option
List
List.IsSuffix
List.IsPrefix
List.IsInfix
List.Perm
List.Pairwise
List.Nodup
List.Lex
USize
UInt8
UInt16
UInt32
UInt64
ISize
Int8
Int16
Int32
Int64
Fin
Option
List
Prod
PProd
MProd
Sum
PSum
Sigma
Subtype
Thunk
_root_
BitVec
Float
Float32
Empty
Quotient
Quot
Setoid
Squash
Subsingleton
WellFoundedRelation
Equivalence
HasEquiv
Lake
Lake.RecBuildM
Lake.FetchM
Lake.ScriptM
MonadEval
True
False
And
Or
Not
Iff
Exists
Eq
HEq
```

```exceptions
Bool.toLBool
Bool.«term_^^_»
```

```exceptions
Decidable.or_not_self
```

```exceptions
Sum.repr
```

```exceptions
String.revFindAux String.extract.go₂ String.substrEq.loop String.casesOn
String.offsetOfPosAux String.extract.go₁ String.mapAux String.firstDiffPos.loop String.utf8SetAux String.revPosOfAux String.replace.loop
String.rec String.recOn String.posOfAux String.splitAux String.foldrAux
String.splitOnAux String.intercalate.go String.anyAux String.findAux
String.utf8GetAux? String.foldlAux String.utf8GetAux
String.utf8PrevAux String.noConfusionType String.noConfusion
String.utf8ByteSize.go String.validateUTF8.loop
String.crlfToLf.go
String.fromUTF8.loop
String.one_le_csize
```

```exceptions
Quot.indep
Quot.lcInv
```

```exceptions
String.sluggify
```

```exceptions
Nat.anyM.loop
Nat.nextPowerOfTwo.go
Nat.foldRevM.loop
Nat.foldM.loop
Nat.foldTR.loop
Nat.recAux
Nat.allTR.loop
Nat.allM.loop
Nat.anyTR.loop
Nat.anyM.loop
Nat.toSuperDigitsAux
Nat.casesAuxOn
Nat.forM.loop
Nat.repeatTR.loop
Nat.forRevM.loop
Nat.toSubDigitsAux
```

```exceptions
Nat.one_pos
Nat.not_lt_of_lt
Nat.sub_lt_self
Nat.lt_or_gt
Nat.pow_le_pow_left
Nat.not_lt_of_gt
Nat.le_or_le
Nat.le_or_ge
Nat.pred_lt'
Nat.pow_le_pow_right
Nat.lt_iff_le_and_not_ge
Nat.mul_pred_right
Nat.mul_pred_left
Nat.prod_dvd_and_dvd_of_dvd_prod
Nat.lt_iff_le_and_not_ge
Nat.mul_pred_right
```

```exceptions
Nat.binductionOn
Nat.le.rec
Nat.le.recOn
Nat.le.casesOn
Nat.le.below
Nat.le.below.step
Nat.le.below.rec
Nat.le.below.recOn
Nat.le.below.refl
Nat.le.below.casesOn
```

```exceptions
EStateM.dummySave
EStateM.dummyRestore
```

```exceptions
Array.get?_size
Array.forIn'.loop
Array.mapM.map
Array.findIdx?.loop
Array.get_extract_loop_lt
Array.foldrM_eq_foldrM_data
Array.get?_push
Array.appendList_data
Array.insertAt.loop
Array.reverse.loop
Array.foldrM_eq_reverse_foldlM_data
Array.isPrefixOfAux
Array.takeWhile.go
Array.isPrefixOfAux
Array.size_eq_length_data
Array.qpartition.loop
Array.insertionSort.swapLoop
Array.foldl_data_eq_bind
Array.foldl_toList_eq_bind
Array.foldrMUnsafe
Array.get_swap_left
Array.get_extract_loop_ge_aux
Array.data_swap
Array.get_extract_loop_lt_aux
Array.get?_swap
Array.get_swap'
Array.mapM_eq_mapM_data
Array.anyM.loop
Array.getElem_eq_data_getElem
Array.get_swap_right
Array.get_extract_loop_ge
Array.foldrM.fold
Array.foldlM.loop
Array.take.loop
Array.mapMUnsafe
Array.binSearchAux
Array.eq_push_pop_back_of_size_ne_zero
Array.get?_push_eq
Array.append_data
Array.indexOfAux
Array.reverse_toList
Array.ofFn.go
Array.get?_eq_data_get?
Array.filterMap_data
Array.empty_data
Array.foldrMUnsafe.fold
Array.toListImpl
Array.filter_data
Array.get_swap_of_ne
Array.get_append_right
Array.getElem?_eq_toList_getElem?
Array.foldl_eq_foldl_data
Array.sequenceMap.loop
Array.toList_eq
Array.findSomeRevM?.find
Array.data_range
Array.forIn'Unsafe.loop
Array.foldlM_eq_foldlM_data
Array.getElem_eq_toList_getElem
Array.getElem_mem_data
Array.get_extract
Array.extract.loop
Array.foldlMUnsafe.fold
Array.data_set
Array.forIn'Unsafe
Array.mapMUnsafe.map
Array.mapM'.go
Array.pop_data
Array.appendCore.loop
Array.get?_len_le
Array.back_push
Array.all_def
Array.get_push_lt
Array.foldl_data_eq_map
Array.get?_eq_toList_get?
Array.isEqvAux
Array.getElem?_mem
Array.getElem_fin_eq_toList_get
Array.getElem?_eq_data_get?
Array.foldr_eq_foldr_data
Array.data_length
Array.get_push
Array.push_data
Array.toArray_data
Array.get_append_left
Array.insertionSort.traverse
Array.getElem_fin_eq_data_get
Array.toListLitAux
Array.map_data
Array.get?_push_lt
Array.get_extract_aux
Array.foldlMUnsafe
Array.qsort.sort
Array.any_def
Array.anyMUnsafe
Array.data_toArray
Array.mem_data
Array.get_swap
Array.mapFinIdxM.map
Array.data_pop
Array.anyMUnsafe.any
Array.mkArray0
Array.mkArray1
Array.mkArray2
Array.mkArray3
Array.mkArray4
Array.mkArray5
Array.mkArray6
Array.mkArray7
Array.mkArray8
Array.mkEmpty
Array.get_push_eq
Array.appendCore
Array.modifyMUnsafe
Array.mapSepElems
Array.mapSepElemsM
Array.toArrayLit
Array.getSepElems
Array.zipWithAux
Array.casesOn
Array.rec
Array.recOn
Array.noConfusion
Array.noConfusionType
Array.tacticArray_get_dec
Array.back_eq_back?
Array.mkArray_data
Array.getLit
```

```exceptions
Array.qpartition
```

```exceptions
Option.toLOption
```

```exceptions
Subarray.forInUnsafe.loop
Subarray.as
Subarray.casesOn
Subarray.recOn
Subarray.rec
Subarray.noConfusion
Subarray.noConfusionType
Subarray.forInUnsafe
Subarray.findSomeRevM?.find
```

```exceptions
Lean.Elab.Tactic.evalUnfold.go
Lean.Elab.Tactic.dsimpLocation.go
Lean.Elab.Tactic.withCollectingNewGoalsFrom.go
Lean.Elab.Tactic.evalRunTac.unsafe_impl_1
Lean.Elab.Tactic.evalRunTac.unsafe_1
Lean.Elab.Tactic.evalTactic.handleEx
Lean.Elab.Tactic.simpLocation.go
Lean.Elab.Tactic.instToSnapshotTreeTacticParsedSnapshot.go
Lean.Elab.Tactic.dsimpLocation'.go
Lean.Elab.Tactic.withRWRulesSeq.go
Lean.Elab.Tactic.runTermElab.go
Lean.Elab.Tactic.getMainGoal.loop
Lean.Elab.Tactic.elabSimpArgs.isSimproc?
Lean.Elab.Tactic.elabSimpArgs.resolveSimpIdTheorem?
Lean.Elab.Tactic.tactic.dbg_cache
Lean.Elab.Tactic.tactic.simp.trace
Lean.Elab.Tactic.liftMetaTacticAux
```

```exceptions

Lean.Elab.Tactic.elabSetOption
Lean.Elab.Tactic.evalSeq1
Lean.Elab.Tactic.evalSimp
Lean.Elab.Tactic.evalSpecialize
Lean.Elab.Tactic.evalTacticAt
Lean.Elab.Tactic.evalSimpAll
Lean.Elab.Tactic.evalIntro.introStep
Lean.Elab.Tactic.evalDone
Lean.Elab.Tactic.evalRevert
Lean.Elab.Tactic.evalRight
Lean.Elab.Tactic.evalUnfold
Lean.Elab.Tactic.evalConstructor
Lean.Elab.Tactic.evalTacticCDot
Lean.Elab.Tactic.evalTraceMessage
Lean.Elab.Tactic.evalClear
Lean.Elab.Tactic.evalIntroMatch
Lean.Elab.Tactic.evalInduction
Lean.Elab.Tactic.evalApply
Lean.Elab.Tactic.evalUnknown
Lean.Elab.Tactic.evalRefl
Lean.Elab.Tactic.evalTactic.throwExs
Lean.Elab.Tactic.evalDSimp
Lean.Elab.Tactic.evalSepTactics.goEven
Lean.Elab.Tactic.evalAllGoals
Lean.Elab.Tactic.evalSplit
Lean.Elab.Tactic.evalInjection
Lean.Elab.Tactic.evalParen
Lean.Elab.Tactic.evalFocus
Lean.Elab.Tactic.evalLeft
Lean.Elab.Tactic.evalRotateRight
Lean.Elab.Tactic.evalWithReducible
Lean.Elab.Tactic.evalTactic.expandEval
Lean.Elab.Tactic.evalTraceState
Lean.Elab.Tactic.evalCase'
Lean.Elab.Tactic.evalSepTactics.goOdd
Lean.Elab.Tactic.evalWithReducibleAndInstances
Lean.Elab.Tactic.evalTacticSeqBracketed
Lean.Elab.Tactic.evalTactic.eval
Lean.Elab.Tactic.evalAlt
Lean.Elab.Tactic.evalGeneralize
Lean.Elab.Tactic.evalRewriteSeq
Lean.Elab.Tactic.evalSleep
Lean.Elab.Tactic.evalDSimpTrace
Lean.Elab.Tactic.evalReplace
Lean.Elab.Tactic.evalOpen
Lean.Elab.Tactic.evalAssumption
Lean.Elab.Tactic.evalSepTactics
Lean.Elab.Tactic.evalWithUnfoldingAll
Lean.Elab.Tactic.evalMatch
Lean.Elab.Tactic.evalRepeat1'
Lean.Elab.Tactic.evalFailIfSuccess
Lean.Elab.Tactic.evalRename
Lean.Elab.Tactic.evalFirst.loop
Lean.Elab.Tactic.evalSimpTrace
Lean.Elab.Tactic.evalFirst
Lean.Elab.Tactic.evalSubstVars
Lean.Elab.Tactic.evalRunTac
Lean.Elab.Tactic.evalSymmSaturate
Lean.Elab.Tactic.evalWithAnnotateState
Lean.Elab.Tactic.evalTacticAtRaw
Lean.Elab.Tactic.evalDbgTrace
Lean.Elab.Tactic.evalSubst
Lean.Elab.Tactic.evalNativeDecide
Lean.Elab.Tactic.evalCalc
Lean.Elab.Tactic.evalCase
Lean.Elab.Tactic.evalRepeat'
Lean.Elab.Tactic.evalRefine
Lean.Elab.Tactic.evalContradiction
Lean.Elab.Tactic.evalSymm
Lean.Elab.Tactic.evalInjections
Lean.Elab.Tactic.evalExact
Lean.Elab.Tactic.evalRotateLeft
Lean.Elab.Tactic.evalFail
Lean.Elab.Tactic.evalTactic
Lean.Elab.Tactic.evalSimpAllTrace
Lean.Elab.Tactic.evalRefine'
Lean.Elab.Tactic.evalChoice
Lean.Elab.Tactic.evalInduction.checkTargets
Lean.Elab.Tactic.evalIntro
Lean.Elab.Tactic.evalAnyGoals
Lean.Elab.Tactic.evalCases
Lean.Elab.Tactic.evalDelta
Lean.Elab.Tactic.evalDecide
Lean.Elab.Tactic.evalChoiceAux
Lean.Elab.Tactic.evalTacticSeq
Lean.Elab.Tactic.evalCheckpoint
Lean.Elab.Tactic.evalRenameInaccessibles
Lean.Elab.Tactic.evalIntros
Lean.Elab.Tactic.evalApplyLikeTactic
Lean.Elab.Tactic.evalSkip
Lean.Elab.Tactic.evalCalc.throwFailed
Lean.Elab.Tactic.evalSubstEqs
Lean.Elab.Tactic.evalTacticSeq1Indented
```

```exceptions
IO.stdGenRef
IO.throwServerError
IO.initializing
```

```exceptions
IO.Process.StdioConfig.noConfusionType
IO.Process.StdioConfig.recOn
IO.Process.StdioConfig.rec
IO.Process.StdioConfig.noConfusion
IO.Process.StdioConfig.casesOn
```

```exceptions
IO.FS.lines.read
```


```exceptions
IO.FS.Handle.readBinToEndInto.loop
```

```exceptions
IO.FS.Stream.readLspNotificationAs
IO.FS.Stream.readNotificationAs
IO.FS.Stream.readResponseAs
IO.FS.Stream.writeLspNotification
IO.FS.Stream.readJson
IO.FS.Stream.readLspMessage
IO.FS.Stream.Buffer.casesOn
IO.FS.Stream.Buffer.noConfusion
IO.FS.Stream.Buffer.recOn
IO.FS.Stream.Buffer.noConfusionType
IO.FS.Stream.Buffer.rec
IO.FS.Stream.rec
IO.FS.Stream.writeLspRequest
IO.FS.Stream.writeResponseError
IO.FS.Stream.noConfusionType
IO.FS.Stream.writeLspResponseErrorWithData
IO.FS.Stream.readLspResponseAs
IO.FS.Stream.noConfusion
IO.FS.Stream.writeLspResponse
IO.FS.Stream.readLspRequestAs
IO.FS.Stream.casesOn
IO.FS.Stream.readMessage
IO.FS.Stream.writeLspMessage
IO.FS.Stream.writeResponseErrorWithData
IO.FS.Stream.recOn
IO.FS.Stream.writeRequest
IO.FS.Stream.writeJson
IO.FS.Stream.writeLspResponseError
IO.FS.Stream.chainLeft
IO.FS.Stream.readRequestAs
IO.FS.Stream.withPrefix
IO.FS.Stream.writeResponse
IO.FS.Stream.chainRight
IO.FS.Stream.writeNotification
IO.FS.Stream.writeMessage
```
```exceptions
System.FilePath.recOn
System.FilePath.noConfusion
System.FilePath.casesOn
System.FilePath.walkDir.go
System.FilePath.rec
System.FilePath.noConfusionType
```

```exceptions
List.tacticSizeOf_list_dec
Lean.Parser.Tactic.tacticRefine_lift_
Lean.Parser.Tactic.tacticRefine_lift'_
Array.tacticArray_mem_dec
Lean.Parser.Tactic.normCast0
tacticClean_wf
Lean.Parser.Tactic.nestedTactic
Lean.Parser.Tactic.unknown
Lean.Parser.Tactic.paren
tacticDecreasing_trivial_pre_omega
```


```exceptions
List.toAssocList'
List.toPArray'
List.countP.go
List.eraseDups.loop
List.eraseIdxTR.go
List.erasePTR.go
List.eraseReps.loop
List.eraseTR.go
List.filterAuxM
List.filterMapM.loop
List.filterMapTR.go
List.filterTR.loop
List.findFinIdx?.go
List.findIdx.go
List.findIdx?.go
List.flatMapM.loop
List.flatMapTR.go
List.forIn'.loop
List.insertIdxTR.go
List.intercalateTR.go
List.iotaTR.go
List.lengthTRAux
List.mapFinIdx.go
List.mapFinIdxM.go
List.mapIdx.go
List.mapIdxM.go
List.mapM.loop
List.mapTR.loop
List.modifyTR.go
List.partition.loop
List.partitionM.go
List.partitionMap.go
List.range'TR.go
List.range.loop
List.replaceTR.go
List.replicateTR.loop
List.reverseAux
List.setTR.go
List.span.loop
List.splitAt.go
List.splitBy.loop
List.takeTR.go
List.takeWhileTR.go
List.toArrayAux
List.toByteArray.loop
List.toFloatArray.loop
List.toPArray'.loop
List.toSMap
List.toSSet
List.zipWithTR.go
```

```exceptions
List.format
List.repr
List.repr'
List.«term_<+:_»
List.«term_<+_»
List.«term_<:+:_»
List.«term_<:+_»
List.«term_~_»
```

```exceptions
List.Perm.below
List.Lex.below
List.Pairwise.below
```

```exceptions
IO.Process.Stdio.toCtorIdx
```

```exceptions
BaseIO.mapTasks.go
```

```exceptions
Fin.foldrM.loop
Fin.induction.go
Fin.foldr.loop
Fin.foldlM.loop
Fin.foldl.loop
```
:::

::::::