mathlib3 documentation

tactic.observe

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 (optional (lean.parser.tk "?"))) (h : interactive.parse (optional 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.

source
def tactic_doc.tactic.observe  :
tactic_doc_entry

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.