Loogle implemented

[siddhartha-gadgil]

The syntax is different from the natural language queries. The following are examples.

#loogle sin go

#loogle nonsense go

#loogle "sin", Real → Real, |- Real go

example : 3 ≤ 5 := by
  #loogle Nat.succ_le_succ go
  decide

example := #loogle List ?a → ?b go

• In case of error, the Loogle instructions are given.
• In case of error with suggestions, there are also TryThis options for the suggestions.