Loogle!

Result

Found 73799 declarations mentioning Nat. Of these, only the first 200 are shown.

• Nat 📋 Init.Prelude
  : Type
• Lean.defaultMaxRecDepth 📋 Init.Prelude
  : ℕ
• Lean.firstFrontendMacroScope 📋 Init.Prelude
  : ℕ
• Lean.reservedMacroScope 📋 Init.Prelude
  : ℕ
• Nat.zero 📋 Init.Prelude
  : ℕ
• UInt16.size 📋 Init.Prelude
  : ℕ
• UInt32.size 📋 Init.Prelude
  : ℕ
• UInt64.size 📋 Init.Prelude
  : ℕ
• UInt8.size 📋 Init.Prelude
  : ℕ
• USize.size 📋 Init.Prelude
  : ℕ
• System.Platform.numBits 📋 Init.Prelude
  : ℕ
• BitVec 📋 Init.Prelude
  (w : ℕ) : Type
• Fin 📋 Init.Prelude
  (n : ℕ) : Type
• instAddNat 📋 Init.Prelude
  : Add ℕ
• instDecidableEqNat 📋 Init.Prelude
  : DecidableEq ℕ
• instInhabitedNat 📋 Init.Prelude
  : Inhabited ℕ
• instLENat 📋 Init.Prelude
  : LE ℕ
• instLTNat 📋 Init.Prelude
  : LT ℕ
• instMinNat 📋 Init.Prelude
  : Min ℕ
• instMulNat 📋 Init.Prelude
  : Mul ℕ
• instNatPowNat 📋 Init.Prelude
  : NatPow ℕ
• instSubNat 📋 Init.Prelude
  : Sub ℕ
• Char.ofNat 📋 Init.Prelude
  (n : ℕ) : Char
• Char.utf8Size 📋 Init.Prelude
  (c : Char) : ℕ
• Nat.isValidChar 📋 Init.Prelude
  (n : ℕ) : Prop
• Nat.succ 📋 Init.Prelude
  (n : ℕ) : ℕ
• Substring.bsize 📋 Init.Prelude
  : Substring → ℕ
• UInt32.toNat 📋 Init.Prelude
  (n : UInt32) : ℕ
• Lean.Syntax.getNumArgs 📋 Init.Prelude
  (stx : Lean.Syntax) : ℕ
• String.Pos.byteIdx 📋 Init.Prelude
  (self : String.Pos) : ℕ
• String.Pos.mk 📋 Init.Prelude
  (byteIdx : ℕ) : String.Pos
• Lean.Macro.Context.currRecDepth 📋 Init.Prelude
  (self : Lean.Macro.Context) : ℕ
• Lean.Macro.Context.maxRecDepth 📋 Init.Prelude
  (self : Lean.Macro.Context) : ℕ
• Nat.pred 📋 Init.Prelude
  : ℕ → ℕ
• String.utf8ByteSize 📋 Init.Prelude
  : String → ℕ
• OfNat 📋 Init.Prelude
  (α : Type u) : ℕ → Type u
• Nat.le 📋 Init.Prelude
  (n : ℕ) : ℕ → Prop
• Nat.lt 📋 Init.Prelude
  (n m : ℕ) : Prop
• Lean.Name.mkNum 📋 Init.Prelude
  (p : Lean.Name) (v : ℕ) : Lean.Name
• Lean.Name.num 📋 Init.Prelude
  (pre : Lean.Name) (i : ℕ) : Lean.Name
• Lean.ParserDescr.cat 📋 Init.Prelude
  (catName : Lean.Name) (rbp : ℕ) : Lean.ParserDescr
• Lean.Syntax.getArg 📋 Init.Prelude
  (stx : Lean.Syntax) (i : ℕ) : Lean.Syntax
• Lean.Syntax.matchesNull 📋 Init.Prelude
  (stx : Lean.Syntax) (n : ℕ) : Bool
• String.utf8ByteSize.go 📋 Init.Prelude
  : List Char → ℕ
• instDecidableEqBitVec 📋 Init.Prelude
  {w : ℕ} : DecidableEq (BitVec w)
• instDecidableEqFin 📋 Init.Prelude
  (n : ℕ) : DecidableEq (Fin n)
• instLEBitVec 📋 Init.Prelude
  {w : ℕ} : LE (BitVec w)
• instLEFin 📋 Init.Prelude
  {n : ℕ} : LE (Fin n)
• instLTBitVec 📋 Init.Prelude
  {w : ℕ} : LT (BitVec w)
• instLTFin 📋 Init.Prelude
  {n : ℕ} : LT (Fin n)
• instOfNatNat 📋 Init.Prelude
  (n : ℕ) : OfNat ℕ n
• BitVec.toNat 📋 Init.Prelude
  {w : ℕ} (x : BitVec w) : ℕ
• Fin.val 📋 Init.Prelude
  {n : ℕ} (self : Fin n) : ℕ
• List.length 📋 Init.Prelude
  {α : Type u_1} : List α → ℕ
• List.lengthTR 📋 Init.Prelude
  {α : Type u_1} (as : List α) : ℕ
• Nat.add 📋 Init.Prelude
  : ℕ → ℕ → ℕ
• Nat.beq 📋 Init.Prelude
  : ℕ → ℕ → Bool
• Nat.ble 📋 Init.Prelude
  : ℕ → ℕ → Bool
• Nat.mul 📋 Init.Prelude
  : ℕ → ℕ → ℕ
• Nat.pow 📋 Init.Prelude
  (m : ℕ) : ℕ → ℕ
• Nat.sub 📋 Init.Prelude
  : ℕ → ℕ → ℕ
• Lean.ParserDescr.node 📋 Init.Prelude
  (kind : Lean.SyntaxNodeKind) (prec : ℕ) (p : Lean.ParserDescr) : Lean.ParserDescr
• Lean.Syntax.isNodeOf 📋 Init.Prelude
  (stx : Lean.Syntax) (k : Lean.SyntaxNodeKind) (n : ℕ) : Bool
• Nat.le.refl 📋 Init.Prelude
  {n : ℕ} : n.le n
• Array.emptyWithCapacity 📋 Init.Prelude
  {α : Type u} (c : ℕ) : Array α
• Array.mkEmpty 📋 Init.Prelude
  {α : Type u} (c : ℕ) : Array α
• Array.size 📋 Init.Prelude
  {α : Type u} (a : Array α) : ℕ
• Char.ofNatAux 📋 Init.Prelude
  (n : ℕ) (h : n.isValidChar) : Char
• List.lengthTRAux 📋 Init.Prelude
  {α : Type u_1} : List α → ℕ → ℕ
• Lean.ParserDescr.trailingNode 📋 Init.Prelude
  (kind : Lean.SyntaxNodeKind) (prec lhsPrec : ℕ) (p : Lean.ParserDescr) : Lean.ParserDescr
• Lean.Syntax.getHeadInfo?.loop 📋 Init.Prelude
  (args : Array Lean.Syntax) (i : ℕ) : Option Lean.SourceInfo
• instPowNat 📋 Init.Prelude
  {α : Type u_1} [NatPow α] : Pow α ℕ
• Array.getD 📋 Init.Prelude
  {α : Type u_1} (a : Array α) (i : ℕ) (v₀ : α) : α
• Nat.le_refl 📋 Init.Prelude
  (n : ℕ) : n ≤ n
• NatPow.mk 📋 Init.Prelude
  {α : Type u} (pow : α → ℕ → α) : NatPow α
• NatPow.pow 📋 Init.Prelude
  {α : Type u} [self : NatPow α] : α → ℕ → α
• OfNat.mk 📋 Init.Prelude
  {α : Type u} {x✝ : ℕ} (ofNat : α) : OfNat α x✝
• OfNat.ofNat 📋 Init.Prelude
  {α : Type u} (x✝ : ℕ) [self : OfNat α x✝] : α
• List.set 📋 Init.Prelude
  {α : Type u_1} (l : List α) (n : ℕ) (a : α) : List α
• Nat.ble_self_eq_true 📋 Init.Prelude
  (n : ℕ) : n.ble n = true
• Nat.le_succ 📋 Init.Prelude
  (n : ℕ) : n ≤ n.succ
• Nat.lt_irrefl 📋 Init.Prelude
  (n : ℕ) : ¬n < n
• UInt16.ofBitVec 📋 Init.Prelude
  (toBitVec : BitVec 16) : UInt16
• UInt16.toBitVec 📋 Init.Prelude
  (self : UInt16) : BitVec 16
• UInt32.ofBitVec 📋 Init.Prelude
  (toBitVec : BitVec 32) : UInt32
• UInt32.toBitVec 📋 Init.Prelude
  (self : UInt32) : BitVec 32
• UInt64.ofBitVec 📋 Init.Prelude
  (toBitVec : BitVec 64) : UInt64
• UInt64.toBitVec 📋 Init.Prelude
  (self : UInt64) : BitVec 64
• UInt8.ofBitVec 📋 Init.Prelude
  (toBitVec : BitVec 8) : UInt8
• UInt8.toBitVec 📋 Init.Prelude
  (self : UInt8) : BitVec 8
• Lean.Macro.Context.mk 📋 Init.Prelude
  (methods : Lean.Macro.MethodsRef✝) (mainModule : Lean.Name) (currMacroScope : Lean.MacroScope) (currRecDepth maxRecDepth : ℕ) (ref : Lean.Syntax) : Lean.Macro.Context
• Array.get!Internal 📋 Init.Prelude
  {α : Type u} [Inhabited α] (a : Array α) (i : ℕ) : α
• Nat.not_succ_le_self 📋 Init.Prelude
  (n : ℕ) : ¬n.succ ≤ n
• UInt16.ofNatLT 📋 Init.Prelude
  (n : ℕ) (h : n < UInt16.size) : UInt16
• UInt32.ofNatLT 📋 Init.Prelude
  (n : ℕ) (h : n < UInt32.size) : UInt32
• UInt64.ofNatLT 📋 Init.Prelude
  (n : ℕ) (h : n < UInt64.size) : UInt64
• UInt8.ofNatLT 📋 Init.Prelude
  (n : ℕ) (h : n < UInt8.size) : UInt8
• USize.ofNatLT 📋 Init.Prelude
  (n : ℕ) (h : n < USize.size) : USize
• Lean.Syntax.getTailPos?.loop 📋 Init.Prelude
  (canonicalOnly : Bool := false) (args : Array Lean.Syntax) (i : ℕ) : Option String.Pos
• Nat.decEq 📋 Init.Prelude
  (n m : ℕ) : Decidable (n = m)
• Fin.mk 📋 Init.Prelude
  {n : ℕ} (val : ℕ) (isLt : val < n) : Fin n
• USize.size_pos 📋 Init.Prelude
  : 0 < USize.size
• Array.appendCore.loop 📋 Init.Prelude
  {α : Type u} (bs : Array α) (i j : ℕ) (as : Array α) : Array α
• Array.extract.loop 📋 Init.Prelude
  {α : Type u_1} (as : Array α) (i j : ℕ) (bs : Array α) : Array α
• Nat.le.step 📋 Init.Prelude
  {n m : ℕ} : n.le m → n.le m.succ
• Nat.decLe 📋 Init.Prelude
  (n m : ℕ) : Decidable (n ≤ m)
• Nat.decLt 📋 Init.Prelude
  (n m : ℕ) : Decidable (n < m)
• Fin.isLt 📋 Init.Prelude
  {n : ℕ} (self : Fin n) : ↑self < n
• Nat.zero_le 📋 Init.Prelude
  (n : ℕ) : 0 ≤ n
• BitVec.decEq 📋 Init.Prelude
  {w : ℕ} (x y : BitVec w) : Decidable (x = y)
• Nat.not_lt_zero 📋 Init.Prelude
  (n : ℕ) : ¬n < 0
• Nat.succ_pos 📋 Init.Prelude
  (n : ℕ) : 0 < n.succ
• Nat.zero_lt_succ 📋 Init.Prelude
  (n : ℕ) : 0 < n.succ
• Nat.le.below 📋 Init.Prelude
  {n : ℕ} : {motive : (a : ℕ) → n.le a → Prop} → {a : ℕ} → n.le a → Prop
• Nat.eq_of_beq_eq_true 📋 Init.Prelude
  {n m : ℕ} : n.beq m = true → n = m
• Nat.not_succ_le_zero 📋 Init.Prelude
  (n : ℕ) : n.succ ≤ 0 → False
• Nat.le.below.refl 📋 Init.Prelude
  {n : ℕ} {motive✝ : (a : ℕ) → n.le a → Prop} : ⋯.below
• instDecidableLeBitVec 📋 Init.Prelude
  {w : ℕ} (x y : BitVec w) : Decidable (x ≤ y)
• instDecidableLtBitVec 📋 Init.Prelude
  {w : ℕ} (x y : BitVec w) : Decidable (x < y)
• Fin.decLe 📋 Init.Prelude
  {n : ℕ} (a b : Fin n) : Decidable (a ≤ b)
• Fin.decLt 📋 Init.Prelude
  {n : ℕ} (a b : Fin n) : Decidable (a < b)
• Nat.le_of_lt_succ 📋 Init.Prelude
  {m n : ℕ} : m < n.succ → m ≤ n
• Nat.le_step 📋 Init.Prelude
  {n m : ℕ} (h : n ≤ m) : n ≤ m.succ
• Nat.le_succ_of_le 📋 Init.Prelude
  {n m : ℕ} (h : n ≤ m) : n ≤ m.succ
• Nat.lt_or_ge 📋 Init.Prelude
  (n m : ℕ) : n < m ∨ n ≥ m
• Nat.ne_of_beq_eq_false 📋 Init.Prelude
  {n m : ℕ} : n.beq m = false → ¬n = m
• Array.getInternal 📋 Init.Prelude
  {α : Type u} (a : Array α) (i : ℕ) (h : i < a.size) : α
• Nat.le_of_succ_le_succ 📋 Init.Prelude
  {n m : ℕ} : n.succ ≤ m.succ → n ≤ m
• Nat.pred_le_pred 📋 Init.Prelude
  {n m : ℕ} : n ≤ m → n.pred ≤ m.pred
• Nat.succ_le_succ 📋 Init.Prelude
  {n m : ℕ} : n ≤ m → n.succ ≤ m.succ
• Nat.ble_eq_true_of_le 📋 Init.Prelude
  {n m : ℕ} (h : n ≤ m) : n.ble m = true
• Nat.le_of_ble_eq_true 📋 Init.Prelude
  {n m : ℕ} (h : n.ble m = true) : n ≤ m
• Nat.ble_succ_eq_true 📋 Init.Prelude
  {n m : ℕ} : n.ble m = true → n.ble m.succ = true
• Nat.le_antisymm 📋 Init.Prelude
  {n m : ℕ} (h₁ : n ≤ m) (h₂ : m ≤ n) : n = m
• Nat.not_le_of_not_ble_eq_true 📋 Init.Prelude
  {n m : ℕ} (h : ¬n.ble m = true) : ¬n ≤ m
• Array.extract 📋 Init.Prelude
  {α : Type u_1} (as : Array α) (start : ℕ := 0) (stop : ℕ := as.size) : Array α
• Nat.eq_or_lt_of_le 📋 Init.Prelude
  {n m : ℕ} : n ≤ m → n = m ∨ n < m
• Nat.lt_of_le_of_ne 📋 Init.Prelude
  {n m : ℕ} (h₁ : n ≤ m) (h₂ : ¬n = m) : n < m
• USize.size_eq 📋 Init.Prelude
  : USize.size = 4294967296 ∨ USize.size = 18446744073709551616
• System.Platform.numBits_eq 📋 Init.Prelude
  : System.Platform.numBits = 32 ∨ System.Platform.numBits = 64
• Fin.eq_of_val_eq 📋 Init.Prelude
  {n : ℕ} {i j : Fin n} : ↑i = ↑j → i = j
• Fin.val_eq_of_eq 📋 Init.Prelude
  {n : ℕ} {i j : Fin n} (h : i = j) : ↑i = ↑j
• Nat.le_trans 📋 Init.Prelude
  {n m k : ℕ} : n ≤ m → m ≤ k → n ≤ k
• Nat.lt_of_le_of_lt 📋 Init.Prelude
  {n m k : ℕ} (h₁ : n ≤ m) (h₂ : m < k) : n < k
• Nat.lt_trans 📋 Init.Prelude
  {n m k : ℕ} (h₁ : n < m) : m < k → n < k
• BitVec.ofFin 📋 Init.Prelude
  {w : ℕ} (toFin : Fin (2 ^ w)) : BitVec w
• BitVec.toFin 📋 Init.Prelude
  {w : ℕ} (self : BitVec w) : Fin (2 ^ w)
• System.Platform.getNumBits 📋 Init.Prelude
  : Unit → { n // n = 32 ∨ n = 64 }
• BitVec.ofNatLT 📋 Init.Prelude
  {w : ℕ} (i : ℕ) (p : i < 2 ^ w) : BitVec w
• Nat.le.brecOn 📋 Init.Prelude
  {n : ℕ} {motive✝ : (a : ℕ) → n.le a → Prop} {a✝ : ℕ} (x✝ : n.le a✝) : (∀ (a : ℕ) (x : n.le a), x.below → motive✝ a x) → motive✝ a✝ x✝
• Nat.le.below.step 📋 Init.Prelude
  {n : ℕ} {motive✝ : (a : ℕ) → n.le a → Prop} {m : ℕ} {a✝ : n.le m} : a✝.below → motive✝ m a✝ → ⋯.below
• instSizeOfNat 📋 Init.SizeOf
  : SizeOf ℕ
• Lean.Name.sizeOf 📋 Init.SizeOf
  : Lean.Name → ℕ
• default.sizeOf 📋 Init.SizeOf
  (α : Sort u) : α → ℕ
• SizeOf.mk 📋 Init.SizeOf
  {α : Sort u} (sizeOf : α → ℕ) : SizeOf α
• SizeOf.sizeOf 📋 Init.SizeOf
  {α : Sort u} [self : SizeOf α] : α → ℕ
• sizeOf_nat 📋 Init.SizeOf
  (n : ℕ) : sizeOf n = n
• Bool.false.sizeOf_spec 📋 Init.SizeOf
  : sizeOf false = 1
• Bool.true.sizeOf_spec 📋 Init.SizeOf
  : sizeOf true = 1
• PUnit.unit.sizeOf_spec 📋 Init.SizeOf
  : sizeOf PUnit.unit = 1
• Lean.Name.anonymous.sizeOf_spec 📋 Init.SizeOf
  : sizeOf Lean.Name.anonymous = 1
• Lean.SourceInfo.none.sizeOf_spec 📋 Init.SizeOf
  : sizeOf Lean.SourceInfo.none = 1
• Lean.Syntax.missing.sizeOf_spec 📋 Init.SizeOf
  : sizeOf Lean.Syntax.missing = 1
• Lean.Macro.Exception.unsupportedSyntax.sizeOf_spec 📋 Init.SizeOf
  : sizeOf Lean.Macro.Exception.unsupportedSyntax = 1
• Bool.sizeOf_eq_one 📋 Init.SizeOf
  (b : Bool) : sizeOf b = 1
• Unit.sizeOf 📋 Init.SizeOf
  (u : Unit) : sizeOf u = 1
• sizeOf_default 📋 Init.SizeOf
  {α : Sort u_1} (n : α) : sizeOf n = 0
• List.nil.sizeOf_spec 📋 Init.SizeOf
  {α : Type u} [SizeOf α] : sizeOf [] = 1
• Option.none.sizeOf_spec 📋 Init.SizeOf
  {α : Type u} [SizeOf α] : sizeOf none = 1
• sizeOf_thunk 📋 Init.SizeOf
  {α : Sort u_1} [SizeOf α] (f : Unit → α) : sizeOf f = sizeOf (f ())
• Decidable.isFalse.sizeOf_spec 📋 Init.SizeOf
  {p : Prop} [SizeOf p] (h : ¬p) : sizeOf (isFalse h) = 1
• Lean.ParserDescr.const.sizeOf_spec 📋 Init.SizeOf
  (name : Lean.Name) : sizeOf (Lean.ParserDescr.const name) = 1 + sizeOf name
• Lean.ParserDescr.parser.sizeOf_spec 📋 Init.SizeOf
  (declName : Lean.Name) : sizeOf (Lean.ParserDescr.parser declName) = 1 + sizeOf declName
• Lean.ParserDescr.symbol.sizeOf_spec 📋 Init.SizeOf
  (val : String) : sizeOf (Lean.ParserDescr.symbol val) = 1 + sizeOf val
• String.Pos.mk.sizeOf_spec 📋 Init.SizeOf
  (byteIdx : ℕ) : sizeOf { byteIdx := byteIdx } = 1 + sizeOf byteIdx
• USize.ofBitVec.sizeOf_spec 📋 Init.SizeOf
  (toBitVec : BitVec System.Platform.numBits) : sizeOf { toBitVec := toBitVec } = 1 + sizeOf toBitVec
• String.mk.sizeOf_spec 📋 Init.SizeOf
  (data : List Char) : sizeOf { data := data } = 1 + sizeOf data
• Lean.TSyntax.mk.sizeOf_spec 📋 Init.SizeOf
  {ks : Lean.SyntaxNodeKinds} (raw : Lean.Syntax) : sizeOf { raw := raw } = 1 + sizeOf raw
• Decidable.isTrue.sizeOf_spec 📋 Init.SizeOf
  {p : Prop} [SizeOf p] (h : p) : sizeOf (isTrue h) = 1 + sizeOf h
• Option.some.sizeOf_spec 📋 Init.SizeOf
  {α : Type u} [SizeOf α] (val : α) : sizeOf (some val) = 1 + sizeOf val
• PLift.up.sizeOf_spec 📋 Init.SizeOf
  {α : Sort u} [SizeOf α] (down : α) : sizeOf { down := down } = 1 + sizeOf down
• ULift.up.sizeOf_spec 📋 Init.SizeOf
  {α : Type s} [SizeOf α] (down : α) : sizeOf { down := down } = 1 + sizeOf down
• Lean.Syntax.SepArray.mk.sizeOf_spec 📋 Init.SizeOf
  {sep : String} (elemsAndSeps : Array Lean.Syntax) : sizeOf { elemsAndSeps := elemsAndSeps } = 1 + sizeOf elemsAndSeps
• Array.mk.sizeOf_spec 📋 Init.SizeOf
  {α : Type u} [SizeOf α] (toList : List α) : sizeOf { toList := toList } = 1 + sizeOf toList
• Lean.Macro.Methods.mk.sizeOf_spec 📋 Init.SizeOf
  (expandMacro? : Lean.Syntax → Lean.MacroM (Option Lean.Syntax)) (getCurrNamespace : Lean.MacroM Lean.Name) (hasDecl : Lean.Name → Lean.MacroM Bool) (resolveNamespace : Lean.Name → Lean.MacroM (List Lean.Name)) (resolveGlobalName : Lean.Name → Lean.MacroM (List (Lean.Name × List String))) : sizeOf { expandMacro? := expandMacro?, getCurrNamespace := getCurrNamespace, hasDecl := hasDecl, resolveNamespace := resolveNamespace, resolveGlobalName := resolveGlobalName } = 1
• Lean.Syntax.TSepArray.mk.sizeOf_spec 📋 Init.SizeOf
  {ks : Lean.SyntaxNodeKinds} {sep : String} (elemsAndSeps : Array Lean.Syntax) : sizeOf { elemsAndSeps := elemsAndSeps } = 1 + sizeOf elemsAndSeps
• Lean.Name.num.sizeOf_spec 📋 Init.SizeOf
  (p : Lean.Name) (n : ℕ) : sizeOf (p.num n) = 1 + sizeOf p + sizeOf n
• Lean.Name.str.sizeOf_spec 📋 Init.SizeOf
  (p : Lean.Name) (s : String) : sizeOf (p.str s) = 1 + sizeOf p + sizeOf s
• Lean.ParserDescr.cat.sizeOf_spec 📋 Init.SizeOf
  (catName : Lean.Name) (rbp : ℕ) : sizeOf (Lean.ParserDescr.cat catName rbp) = 1 + sizeOf catName + sizeOf rbp
• Lean.ParserDescr.nonReservedSymbol.sizeOf_spec 📋 Init.SizeOf
  (val : String) (includeIdent : Bool) : sizeOf (Lean.ParserDescr.nonReservedSymbol val includeIdent) = 1 + sizeOf val + sizeOf includeIdent
• Lean.ParserDescr.unary.sizeOf_spec 📋 Init.SizeOf
  (name : Lean.Name) (p : Lean.ParserDescr) : sizeOf (Lean.ParserDescr.unary name p) = 1 + sizeOf name + sizeOf p
• Lean.Syntax.atom.sizeOf_spec 📋 Init.SizeOf
  (info : Lean.SourceInfo) (val : String) : sizeOf (Lean.Syntax.atom info val) = 1 + sizeOf info + sizeOf val
• Lean.Macro.Exception.error.sizeOf_spec 📋 Init.SizeOf
  (a✝ : Lean.Syntax) (a✝¹ : String) : sizeOf (Lean.Macro.Exception.error a✝ a✝¹) = 1 + sizeOf a✝ + sizeOf a✝¹
• Except.error.sizeOf_spec 📋 Init.SizeOf
  {ε : Type u} {α : Type v} [SizeOf ε] [SizeOf α] (a✝ : ε) : sizeOf (Except.error a✝) = 1 + sizeOf a✝
• Except.ok.sizeOf_spec 📋 Init.SizeOf
  {ε : Type u} {α : Type v} [SizeOf ε] [SizeOf α] (a✝ : α) : sizeOf (Except.ok a✝) = 1 + sizeOf a✝
• UInt16.ofBitVec.sizeOf_spec 📋 Init.SizeOf
  (toBitVec : BitVec 16) : sizeOf { toBitVec := toBitVec } = 1 + sizeOf toBitVec
• UInt32.ofBitVec.sizeOf_spec 📋 Init.SizeOf
  (toBitVec : BitVec 32) : sizeOf { toBitVec := toBitVec } = 1 + sizeOf toBitVec
• UInt64.ofBitVec.sizeOf_spec 📋 Init.SizeOf
  (toBitVec : BitVec 64) : sizeOf { toBitVec := toBitVec } = 1 + sizeOf toBitVec
• UInt8.ofBitVec.sizeOf_spec 📋 Init.SizeOf
  (toBitVec : BitVec 8) : sizeOf { toBitVec := toBitVec } = 1 + sizeOf toBitVec
• Char.mk.sizeOf_spec 📋 Init.SizeOf
  (val : UInt32) (valid : val.isValidChar) : sizeOf { val := val, valid := valid } = 1 + sizeOf val + sizeOf valid

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 19971e9 serving mathlib revision 151dd12