Documented new elim form

cur-doc/cur/scribblings/curnel.scrbl

@@ -17,7 +17,7 @@ Edwin C. Brady.
 @(define curnel-eval (curnel-sandbox "(require cur/stdlib/nat cur/stdlib/bool cur/stdlib/prop)"))
 
 @defform*[((Type n)
-	   Type)]{
+           Type)]{
 Define the universe of types at level @racket[n], where @racket[n] is any natural number.
 @racket[Type] is a synonym for @racket[(Type 0)]. Cur is impredicative
 in @racket[(Type 0)], although this is likely to change to a more
@@ -91,13 +91,16 @@ For instance, Cur does not currently perform strict positivity checking.
           ((((conj Bool) Bool) true) false)]
 }
 
-@defform[(elim type motive-universe)]{
+@defform[(elim inductive-type motive (index ...) (method ...) disc)]{
-Returns the inductive eliminator for @racket[type] where the @racket[motive-universe] is the universe
+Fold over the term @racket[disc] of the inductively defined type @racket[inductive-type].
-of the motive.
+The @racket[motive] is a function that expects the indices of the inductive
-The eliminator expects the next argument to be the motive, the next @racket[N] arguments to be the methods for
+type and a term of the inductive type and produces the type that this
-each of the @racket[N] constructors of the inductive type @racket[type], the next @racket[P] arguments
+fold returns.
-to be the parameters @racket[p_0 ... p_P] of the inductive @racket[type], and the final argument to be the term to
+The type of @racket[disc] is @racket[(inductive-type index ...)].
-eliminate of type @racket[(type p_0 ... p_P)].
+@racket[elim] takes one method for each constructor of @racket[inductive-type].
+Each @racket[method] expects the arguments for its corresponding constructor,
+and the inductive hypotheses generated by recursively eliminating all recursive
+arguments of the constructor.
 
 The following example runs @racket[(sub1 (s z))].
 
@@ -105,11 +108,11 @@ The following example runs @racket[(sub1 (s z))].
           (data Nat : Type
             (z : Nat)
             (s : (Π (n : Nat) Nat)))
-          (((((elim Nat Type)
+          (elim Nat (λ (x : Nat) Nat)
-              (λ (x : Nat) Nat))
+                ()
-             z)
+                (z
-            (λ (n : Nat) (λ (IH : Nat) n)))
+                 (λ (n : Nat) (λ (IH : Nat) n)))
-           (s z))]
+                (s z))]
 }
 
 @defform[(define id expr)]{
@@ -120,9 +123,11 @@ Binds @racket[id] to the result of @racket[expr].
             (z : Nat)
             (s : (Π (n : Nat) Nat)))
           (define sub1 (λ (n : Nat)
-                         (((((elim Nat Type) (λ (x : Nat) Nat))
+                         (elim Nat (λ (x : Nat) Nat)
-                           z)
+                               ()
-                          (λ (n : Nat) (λ (IH : Nat) n))) n)))
+                               (z
+                                (λ (n : Nat) (λ (IH : Nat) n)))
+                               n)))
           (sub1 (s (s z)))
           (sub1 (s z))
           (sub1 z)]

cur-doc/cur/scribblings/reflection.scrbl

@@ -76,10 +76,10 @@ Runs the Cur term @racket[syn] for one step.
 (eval:alts (cur-step #'((λ (x : Type) x) Bool))
            (eval:result @racket[#'Bool] "" ""))
 (eval:alts (cur-step #'(sub1 (s (s z))))
-           (eval:result @racket[#'(((((elim Nat (Type 0))
+           (eval:result @racket[#'(elim Nat (λ (x2 : Nat) Nat)
-                                      (λ (x2 : Nat) Nat)) z)
+                                        ()
-                                    (λ (x2 : Nat) (λ (ih-n2 : Nat) x2)))
+                                        (z (λ (x2 : Nat) (λ (ih-n2 : Nat) x2)))
-                                   (s (s z)))] "" ""))
+                                        (s (s z)))] "" ""))
 ]
 }
 

cur-doc/cur/scribblings/stdlib/bool.scrbl

@@ -22,7 +22,7 @@ A syntactic form that expands to the inductive eliminator for @racket[Bool]. Thi
 
 @examples[#:eval curnel-eval
           (if true false true)
-	  (elim Bool Type (λ (x : Bool) Bool) false true true)]
+	  (elim Bool (λ (x : Bool) Bool) () (false true) true)]
 }
 
 @defproc[(not [x Bool])

cur-doc/cur/scribblings/stdlib/sugar.scrbl

@@ -82,17 +82,6 @@ a @racket[(: name type)] form appears earlier in the module.
 	  (define (id A a) a)]
 }
 
-@defform[(elim type motive-result-type e ...)]{
-Like the @racket[elim] provided by @racketmodname[cur], but supports
-automatically curries the remaining arguments @racket[e ...].
-
-@examples[#:eval curnel-eval
-          (elim Bool Type (lambda (x : Bool) Bool)
-            false
-            true
-            true)]
-}
-
 @defform*[((define-type name type)
            (define-type (name (a : t) ...) body))]{
 Like @racket[define], but uses @racket[forall] instead of @racket[lambda].

cur-doc/info.rkt

@@ -1,6 +1,6 @@
 #lang info
 (define collection 'multi)
 (define deps '("base" "racket-doc"))
-(define build-deps '("scribble-lib" ("cur-lib" #:version "0.2") "sandbox-lib"))
+(define build-deps '("scribble-lib" ("cur-lib" #:version "0.4") "sandbox-lib"))
 (define pkg-desc "Documentation for \"cur\".")
 (define pkg-authors '(wilbowma))