Documentation

LeanDoc

source

Imports

Init
Lean

Imported by

main

source

def main (xs : List String) :

IO Unit

Equations

main xs = pure ()

General documentation

index

Library

Init

Init.Control

Init.Control.Basic

Init.Control.EState

Init.Control.Except

Init.Control.ExceptCps

Init.Control.StateCps

Init.Control.StateRef

Init.Data

Init.Data.Array

Init.Data.Array.Basic

Init.Data.Array.BinSearch

Init.Data.Array.InsertionSort

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

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

Init.System

Init.WF

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

Lean.Compiler.ImplementedByAttr

Lean.Compiler.InitAttr

Lean.Compiler.InlineAttrs

Lean.Compiler.NameMangling

Lean.Compiler.NeverExtractAttr

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

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.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.PreDefinition.Structural

Lean.Elab.PreDefinition.WF

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

Lean.Elab.Tactic.Conv

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

Lean.Elab.MacroArgUtil

Lean.Elab.MacroRules

Lean.Elab.Match

Lean.Elab.MatchAltView

Lean.Elab.PreDefinition

Lean.Elab.Print

Lean.Elab.Quotation

Lean.Elab.RecAppSyntax

Lean.Elab.SyntheticMVars

Lean.Elab.Tactic

Lean.Elab.Term

Lean.Elab.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.MatchPatternAttr

Lean.Meta.Match.MatcherInfo

Lean.Meta.Match.Value

Lean.Meta.Tactic

Lean.Meta.Tactic.Simp

Lean.Meta.Tactic.Simp.CongrLemmas

Lean.Meta.Tactic.Simp.Main

Lean.Meta.Tactic.Simp.Rewrite

Lean.Meta.Tactic.Simp.SimpAll

Lean.Meta.Tactic.Simp.SimpLemmas

Lean.Meta.Tactic.Simp.Types

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

Lean.Meta.Tactic.Replace

Lean.Meta.Tactic.Revert

Lean.Meta.Tactic.Rewrite

Lean.Meta.Tactic.Simp

Lean.Meta.Tactic.Split

Lean.Meta.Tactic.SplitIf

Lean.Meta.Tactic.Subst

Lean.Meta.Tactic.Unfold

Lean.Meta.Tactic.Util

Lean.Meta.ACLt

Lean.Meta.AbstractMVars

Lean.Meta.AbstractNestedProofs

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

Lean.Meta.ForEachExpr

Lean.Meta.FunInfo

Lean.Meta.GeneralizeTelescope

Lean.Meta.GeneralizeVars

Lean.Meta.GetConst

Lean.Meta.GlobalInstances

Lean.Meta.IndPredBelow

Lean.Meta.RecursorInfo

Lean.Meta.Reduce

Lean.Meta.ReduceEval

Lean.Meta.SizeOf

Lean.Meta.SortLocalDecls

Lean.Meta.Structure

Lean.Meta.SynthInstance

Lean.Meta.Tactic

Lean.Meta.Transform

Lean.Meta.TransparencyMode

Lean.Meta.UnificationHint

Lean.Parser

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

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

Lean.Server.InfoUtils

Lean.Server.References

Lean.Server.Requests

Lean.Server.Rpc

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

Lean.Util.MonadCache

Lean.Util.OccursCheck

Lean.Util.Recognizers

Lean.Util.ReplaceExpr

Lean.Util.ReplaceLevel

Lean.Util.SCC

Lean.Util.Sorry

Lean.Util.Trace

Lean.Widget

Lean.Widget.InteractiveCode

Lean.Widget.InteractiveDiagnostic

Lean.Widget.InteractiveGoal

Lean.Widget.TaggedText

Lean.DeclarationRange

Lean.InternalExceptionId

Lean.KeyedDeclsAttribute

Lean.LazyInitExtension

Lean.ReducibilityAttrs

Lean.ResolveName

Lean.Runtime

Lean.ScopedEnvExtension

LeanDoc

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