search by signature

Stream: general

[Matthew Pocock]

I've written this simple function:

def compose_n (n : Nat) (g : α → α  ) (x : α) : α := match n with
  | Nat.zero => x
  | Nat.succ a => compose_n a g (g x)

Assuming I haven't mucked it up, it applies a function g to an argument x n times. I'm sure this or its equivalent must be in the standard library. Is it possible to search by type signature? Or structural equivalency?

[Ruben Van de Velde]

There's https://loogle.lean-fro.org

[Ruben Van de Velde]

You might be looking for docs#Nat.iterate

[Floris van Doorn]

@loogle Nat -> (?a -> ?a) -> ?a -> ?a

Do I do this right?

[loogle]

Failure! Bot is unavailable

[Matthew Pocock]

Ruben Van de Velde said:

You might be looking for docs#Nat.iterate

thanks

[Joachim Breitner]

You do it right, but that query seems to take too long because it's relatively generic - it only has Nat to index on, and too many lemmas mention Nat :-)
But not even

[Joachim Breitner]

@loogle Nat -> (?a -> ?a) -> ?a -> ?a, "iter"

[loogle]

:shrug: nothing found

[Joachim Breitner]

works, and I wonder why. The pattern matching with metavariables doesn't always seem to do what it should, I fear

[Matthew Pocock]

So as a sanity check, would this be a valid way to express the collatz conjecture using Nat.iterate?

def collatz_conjecture := n > 0 -> ∃ p, Nat.iterate collatz p n = 1

[Matthew Pocock]

Do I need to import anything to get #find syntax to work within a session?

[Joachim Breitner]

The syntax supported by https://loogle.lean-fro.org/ isn't in mathlib yet, so maybe just use the web version for now