This raise no error.
import LeanSearchClient.LoogleSyntax
/--
info: Loogle Search Results
• #check Option.get!
-/
#guard_msgs in
#loogle Option ?a → ?a, "get!"
But this fails.
import LeanSearchClient.LoogleSyntax
/--
info: Loogle Search Results
• #check Option.get!
-/
#guard_msgs in
#loogle Option ?a → ?a, "get!"
/- hello -/