From c68d0ae97a4b5026abf8812422b446059a1b2207 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Wed, 23 Sep 2015 16:40:23 -0400 Subject: [PATCH] Added a few examples to tactic docs --- scribblings/stdlib/tactics.scrbl | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/scribblings/stdlib/tactics.scrbl b/scribblings/stdlib/tactics.scrbl index ef840d4..9d1bab9 100644 --- a/scribblings/stdlib/tactics.scrbl +++ b/scribblings/stdlib/tactics.scrbl @@ -16,6 +16,16 @@ Defines a new @tech{tactic}, at @gtech{phase} 1. A @deftech{tactic} is a Racket @tech{proof state} to @tech{proof state} that runs at @gtech{phase} 1. A @tech{tactic} takes any number of arguments, plus the @tech{proof state}. The @tech{proof state} must be the final argument of the tactic. + +Examples: +@racketblock[ +(define-tactic (do-nothing ps) + ps) + +(define-tactic (switch-goal i ps) + (struct-copy proof-state ps + [current-goal i])) +] } @defproc[(proof? [p any/c]) @@ -139,6 +149,18 @@ saved anywhere, only checked against the most recent theorem defined via @racket Note that the proof state is implicitly given to each call by @racket[proof] and should not appear as an explicit argument. + +Examples: +@racketblock[ +(define-theorem a-silly-theorem (forall (x : Nat) Nat)) +(proof + (intro x) + (by-assumption)) + +(define-theorem falseo (forall (x : Type) x)) +(proof + (interactive)) +] } @todo{Examples, better documentation (e.g. don't say "returns a proof state"; the signature says so)}