observe #

The observe tactic is mainly intended for demo/educational purposes. Calling observe hp : p is equivalent to have hp : p, { library_search }.

source

meta def tactic.interactive.observe (trc : interactive.parse (lean.parser.tk "?")?) (h : interactive.parse lean.parser.ident ?) (t : interactive.parse (lean.parser.tk ":" *> interactive.types.texpr)) :

tactic unit

observe hp : p asserts the proposition p, and tries to prove it using library_search. If no proof is found, the tactic fails. In other words, this tactic is equivalent to have hp : p, { library_search }.

If hp is omitted, then the placeholder this is used.

The variant observe? hp : p will emit a trace message of the form have hp : p := proof_term. This may be particularly useful to speed up proofs.