Documentation
Init.Data.Nat.Log2
Google site search
Init.Data.Nat.Log2
source
Imports
Init.NotationExtra
Imported by
Init.Data.Nat
Nat.log2
source
@[extern lean_nat_log2]
def
Nat.log2
(n :
Nat
)
:
Nat
Equations
Nat.log2
n
=
if h :
n
≥
2
then
Nat.log2
(
n
/
2
)
+
1
else
0
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.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.Array
Init.Data.Basic
Init.Data.ByteArray
Init.Data.Char
Init.Data.Fin
Init.Data.Float
Init.Data.FloatArray
Init.Data.Format
Init.Data.Hashable
Init.Data.Int
Init.Data.List
Init.Data.Nat
Init.Data.OfScientific
Init.Data.Option
Init.Data.Ord
Init.Data.Random
Init.Data.Range
Init.Data.Repr
Init.Data.Stream
Init.Data.String
Init.Data.ToString
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.Control
Init.Conv
Init.Core
Init.Data
Init.Fix
Init.Hints
Init.Meta
Init.Notation
Init.NotationExtra
Init.Prelude
Init.SimpLemmas
Init.SizeOf
Init.System
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.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.Xml.Basic
Lean.Data.Xml.Parser
Lean.Data.Format
Lean.Data.Json
Lean.Data.JsonRpc
Lean.Data.KVMap
Lean.Data.LBool
Lean.Data.LOption
Lean.Data.Lsp
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.Data.Xml
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.App
Lean.Elab.Arg
Lean.Elab.Attributes
Lean.Elab.AutoBound
Lean.Elab.AuxDef
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.Deriving
Lean.Elab.Do
Lean.Elab.ElabRules
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.Log
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.PreDefinition
Lean.Elab.Print
Lean.Elab.Quotation
Lean.Elab.RecAppSyntax
Lean.Elab.SetOption
Lean.Elab.StructInst
Lean.Elab.Structure
Lean.Elab.Syntax
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.AppBuilder
Lean.Meta.Basic
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.ExprDefEq
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.LevelDefEq
Lean.Meta.Match
Lean.Meta.MatchUtil
Lean.Meta.Offset
Lean.Meta.PPGoal
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.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.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.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.InteractiveCode
Lean.Widget.InteractiveDiagnostic
Lean.Widget.InteractiveGoal
Lean.Widget.TaggedText
Lean.Attributes
Lean.AuxRecursor
Lean.Class
Lean.Compiler
Lean.CoreM
Lean.Data
Lean.Declaration
Lean.DeclarationRange
Lean.DocString
Lean.Elab
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.Message
Lean.Meta
Lean.MetavarContext
Lean.Modifiers
Lean.MonadEnv
Lean.Parser
Lean.ParserCompiler
Lean.PrettyPrinter
Lean.ProjFns
Lean.ReducibilityAttrs
Lean.ResolveName
Lean.Runtime
Lean.ScopedEnvExtension
Lean.Server
Lean.Structure
Lean.Syntax
Lean.ToExpr
Lean.Util
Lean.Widget
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