How do I search function by type on loogle?

Stream: new members

[MrQubo]

I'm trying do find a theorem that would compose implications. On hoogle I can just search e.g. (p -> q) -> (q -> r) -> p -> r.
Is something like that possible on loogle? I've tried (?p ?q ?r : Prop) -> (?p -> ?q) -> (?q -> ?r) -> ?p -> ?r.

[MrQubo]

These don't work either:
(?p -> ?q) -> (?q -> ?r) -> ?p -> ?r
(p q r : Prop) -> (p -> q) -> (q -> r) -> p -> r

[Edward van de Meent]

is there a reason why usual function composition doesn't fit your use?

[suhr]

example {p q r: Prop}(pq: p → q)(qr: q → r): p → r :=
  qr ∘ pq

[MrQubo]

Edward van de Meent said:

is there a reason why usual function composition doesn't fit your use?

It does. But I don't know how to do function composition either.

[MrQubo]

And I've tried finding how to do function composition, without having to ask question on zulip. .-.

[MrQubo]

So, I've got the answer to that (thanks @suhr !), but I still would want to know how to use loogle.

[Eric Wieser]

I think you've just stumbled upon a corner case that Loogle can't handle

[MrQubo]

Hmm, I've tried using loogle like many times, and I think it never worked. What is the problem in this case?

[Eric Wieser]

"Cannot search: No constants or name fragments in search pattern." is what loogle says

[Eric Wieser]

Indeed, loogle works much better if you have some constants or name fragments

[MrQubo]

There's Prop constant. So I'm not even sure what the error means.

[Edward van de Meent]

technically, Prop is not a constant, i think...

[MrQubo]

Ah, yeah, you might be right.

[Edward van de Meent]

looking at the constructors of docs#Lean.Expr, indeed it is a separate expression. (.sort .zero rather than .const ``Prop or something)

[MrQubo]

Thanks! I hope this limitation will be fixed at some point. Until than, I guess I have to use zulip-powered search. :P
Or work through MoP, cause I would probably find function composition somewhere in there.

[Eric Wieser]

Searching loogle for "comp" and "function" would have found it