Recovered better elim syntax in sugar.rkt

scribblings/stdlib/sugar.scrbl

@@ -78,6 +78,18 @@ Like the @racket[define] provided by @racketmodname[cur/curnel/redex-lang], but
 defining curried functions via @racket[lambda*].
 }
 
+@defform[(elim type motive-result-type e ...)]{
+Like the @racket[elim] provided by @racketmodname[cur/curnel/redex-lang], but supports
+automatically curries the remaining arguments @racket[e ...].
+
+@examples[#:eval curnel-eval
+          (require cur/stdlib/bool)
+          (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*].

stdlib/nat.rkt

@@ -33,12 +33,12 @@
 
 ;; Credit to this function goes to Max
 (define nat-equal?
-  ((elim Nat Type) (lambda (x : Nat) (-> Nat Bool))
+  (elim Nat Type (lambda (x : Nat) (-> Nat Bool))
-    ((elim Nat Type) (lambda (x : Nat) Bool)
+    (elim Nat Type (lambda (x : Nat) Bool)
           true
           (lambda* (x : Nat) (ih-n2 : Bool) false))
     (lambda* (x : Nat) (ih : (-> Nat Bool))
-      ((elim Nat Type) (lambda (x : Nat) Bool)
+      (elim Nat Type (lambda (x : Nat) Bool)
             false
             (lambda* (x : Nat) (ih-bla : Bool)
                      (ih x))))))

stdlib/sugar.rkt

@@ -6,6 +6,7 @@
   lambda*
   #%app
   define
+  elim
   define-type
   case
   case*
@@ -18,6 +19,7 @@
 
 (require
   (only-in "../cur.rkt"
+    [elim real-elim]
     [#%app real-app]
     [define real-define]))
 
@@ -67,6 +69,9 @@
     [(define id body)
      #'(real-define id body)]))
 
+(define-syntax-rule (elim t1 t2 e ...)
+  ((real-elim t1 t2) e ...))
+
 (begin-for-syntax
   (define (rewrite-clause clause)
     (syntax-case clause (: IH:)
@@ -88,13 +93,13 @@
      (let* ([D (type-infer/syn #'e)]
             [M (type-infer/syn (clause-body #'(clause* ...)))]
             [U (type-infer/syn M)])
-       #`((elim #,D #,U) (lambda (x : #,D) #,M) #,@(map rewrite-clause (syntax->list #'(clause* ...)))
+       #`(elim #,D #,U (lambda (x : #,D) #,M) #,@(map rewrite-clause (syntax->list #'(clause* ...)))
                e))]))
 
 (define-syntax (case* syn)
   (syntax-case syn ()
     [(_ D U e (p ...) P clause* ...)
-     #`((elim D U) P #,@(map rewrite-clause (syntax->list #'(clause* ...))) p ... e)]))
+     #`(elim D U P #,@(map rewrite-clause (syntax->list #'(clause* ...))) p ... e)]))
 
 (define-syntax-rule (define-theorem name prop)
   (define name prop))