From 11f07080bd5db0380d1c688c53cb3a1a71eecdfd Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Tue, 10 Nov 2015 16:30:46 -0500 Subject: [PATCH] More documentation --- scribblings/stdlib.scrbl | 2 ++ scribblings/stdlib/nat.scrbl | 69 ++++++++++++++++++++++++++++++++++++ stdlib/nat.rkt | 2 +- 3 files changed, 72 insertions(+), 1 deletion(-) create mode 100644 scribblings/stdlib/nat.scrbl diff --git a/scribblings/stdlib.scrbl b/scribblings/stdlib.scrbl index fe4a1ea..4682c30 100644 --- a/scribblings/stdlib.scrbl +++ b/scribblings/stdlib.scrbl @@ -9,3 +9,5 @@ Cur has a small standard library, primary for demonstration purposes. @include-section{stdlib/tactics.scrbl} @include-section{stdlib/sugar.scrbl} +@include-section{stdlib/bool.scrbl} +@include-section{stdlib/nat.scrbl} diff --git a/scribblings/stdlib/nat.scrbl b/scribblings/stdlib/nat.scrbl new file mode 100644 index 0000000..cfbd3e3 --- /dev/null +++ b/scribblings/stdlib/nat.scrbl @@ -0,0 +1,69 @@ +#lang scribble/manual + +@(require + "../defs.rkt" + scribble/eval) + +@(define curnel-eval (curnel-sandbox "(require cur/stdlib/bool cur/stdlib/nat cur/stdlib/sugar)")) + +@title{Nat} +@defmodule[cur/stdlib/nat] +This library defines the datatype @racket[Nat] and several functions on them. + +@deftogether[(@defthing[Nat Type] + @defthing[z Nat] + @defthing[s (-> Nat Nat)])]{ +The natural number datatype. +} + +@defproc[(add1 [n Nat]) Nat]{ +A more lispy name for @racket[s]. + +@examples[#:eval curnel-eval + (s z) + (add1 z)] +} + +@defproc[(sub1 [n Nat]) Nat]{ +Return the predecessor of @racket[n], or @racket[z] is @racket[n] is @racket[z]. + +@examples[#:eval curnel-eval + (sub1 (s z))] + +} + +@defproc[(plus [n Nat] [m Nat]) Nat]{ +Add @racket[n] and @racket[m]. + +@examples[#:eval curnel-eval + (plus (s z) (s z)) + (plus z (s z)) + (plus (s (s z)) (s z))] +} + +@defproc[(nat-equal? [n Nat] [m Nat]) Bool]{ +Return @racket[true] if and only if @racket[n] is equal to @racket[m]. + +@examples[#:eval curnel-eval + (nat-equal? (s z) (s z)) + (nat-equal? z (s z))] +} + +@defproc[(even? [n Nat]) Bool]{ +Return @racket[true] if and only if @racket[n] is even. + +@examples[#:eval curnel-eval + (even? (s z)) + (even? z) + (even? (s (s z)))] + +} + +@defproc[(odd? [n Nat]) Bool]{ +Return @racket[true] if and only if @racket[n] is not even. + +@examples[#:eval curnel-eval + (odd? (s z)) + (odd? z) + (odd? (s (s z)))] +} diff --git a/stdlib/nat.rkt b/stdlib/nat.rkt index f7bf650..85eced7 100644 --- a/stdlib/nat.rkt +++ b/stdlib/nat.rkt @@ -2,7 +2,7 @@ (require "sugar.rkt" "bool.rkt") ;; TODO: override (all-defined-out) to enable exporting all these ;; properly. -(provide Nat z s add1 sub1 plus ) +(provide Nat z s add1 sub1 plus nat-equal? even? odd?) (module+ test (require rackunit))