From 548b553e434afa7583c8126edb53b80e56f676cb Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Tue, 10 Nov 2015 13:42:04 -0500 Subject: [PATCH] A little more docs for tactics --- scribblings/stdlib/tactics.scrbl | 2 ++ 1 file changed, 2 insertions(+) diff --git a/scribblings/stdlib/tactics.scrbl b/scribblings/stdlib/tactics.scrbl index ac94477..b6d92f1 100644 --- a/scribblings/stdlib/tactics.scrbl +++ b/scribblings/stdlib/tactics.scrbl @@ -57,6 +57,8 @@ Returns an empty partial @tech{proof}, i.e., the identity function. [current-goal natural-number/c] [proof (or/c syntax? procedure?)] [theorem syntax?])]{ +A structure representing the @deftech{proof state} for the proof of the current theorem. + The environment @racket[env] is a map of assumptions local to the theorem from symbols (names) to the type of the assumption as a syntax object. The list of goals @racket[goals] is a map from natural numbers to goals, types as syntax objects.