Find a function by its signature

Stream: new members

[Sergey Cherkis]

I am new to lean(4). Can one search for a function by specifying its signature (as for Haskell with hoogle.com)?
For example, is there a function reading a character, with signature Char -> Nat or Char -> Option Nat ?

[Alex J. Best]

In mathlib4 there is an implementation of a #find command that does this, so you can use

import Mathlib.Tactic.Find

#find Char -> Nat

which returns

LeanProject.lean:4:0
  Char.toNat: Char → ℕ
LeanProject.lean:4:0
  String.count: String → Char → ℕ
LeanProject.lean:4:0
  Lean.Xml.Parser.hexDigitToNat: Lean.Xml.Parser.LeanChar → ℕ
LeanProject.lean:4:0
  String.csize: Char → ℕ

[Sergey Cherkis]

Alex J. Best said:

In mathlib4 there is an implementation of a #find command that does this, so you can use

import Mathlib.Tactic.Find

#find Char -> Nat

which returns

LeanProject.lean:4:0
  Char.toNat: Char → ℕ
LeanProject.lean:4:0
  String.count: String → Char → ℕ
LeanProject.lean:4:0
  Lean.Xml.Parser.hexDigitToNat: Lean.Xml.Parser.LeanChar → ℕ
LeanProject.lean:4:0
  String.csize: Char → ℕ

Thank you! And what is an idiomatic way of converting '4':Char into 4:Nat or into (some 4):Option Nat ?

[Alex J. Best]

Hmm there should be some string parsing functions that parse strings representing naturals into Nats. I don't know the names right now, but something in the parser namespace like parseNat or something would be a good place to start

[Adam Topaz]

docs#String.toNat! It seems

[Adam Topaz]

There’s also a String.toNat?

[Kyle Miller]

docs#Lean.Syntax.decodeNatLitVal? is the function that decodes natural number literals for the Lean 4 language, which includes things like 0xFF