Loogle bug?

Stream: general

[Kenny Lau]

"ℕ" fails to find termℕ, which "termℕ" succeeds in for some reason

[Kenny Lau]

(cc @Joachim Breitner)

[Aaron Liu]

oh I remember this

[Aaron Liu]

looks like loogle doesn't find a declaration when you search for its last "letter" (whatever that means) and you only search by name fragments

[Kenny Lau]

interesting

[Aaron Liu]

oh I figured it out

[Aaron Liu]

this is really stupid

[Aaron Liu]

https://github.com/nomeata/loogle/blob/ad0d2bbd507ac28ef353c4421533192eda3c5555/Loogle/Find.lean#L196

[Aaron Liu]

it subtracts one, but List.range n only goes from 0 to n - 1 anyways, so it ends up going from 0 to s.length - 2

[Aaron Liu]

and when you drop s.length - 2 you end up with a string of length 2

[Aaron Liu]

so the length one suffix never gets added

[Kenny Lau]

import Lean

elab "test" : term => do
  have s := "testing"
  for i in List.range (s.length - 1) do -- -1 to not consider the empty suffix
    let suf := s.drop i
    Lean.logInfo suf
  return Lean.mkNatLit 1

#check test

[Kenny Lau]

yep your observation is correct

[Kenny Lau]

the last printed message is ng

[Kenny Lau]

@Aaron Liu you could probably just PR?

[Aaron Liu]

what

[Aaron Liu]

why me

[Kenny Lau]

you found the error code

[Aaron Liu]

fine I'll do it

[Kenny Lau]

thanks!

[Aaron Liu]

nomeata/loogle#45