suzanne.soy/cur
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

A little more docs for tactics

Browse Source
This commit is contained in:
William J. Bowman 2015-11-10 13:42:04 -05:00
parent 1b4ea69548
commit 548b553e43
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
1 changed files with 2 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
scribblings/stdlib/tactics.scrbl
View File

@ -57,6 +57,8 @@ Returns an empty partial @tech{proof}, i.e., the identity function.
[current-goal natural-number/c] [current-goal natural-number/c]
[proof (or/c syntax? procedure?)] [proof (or/c syntax? procedure?)]
[theorem syntax?])]{ [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 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. 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. The list of goals @racket[goals] is a map from natural numbers to goals, types as syntax objects.