Added axioms; added test, but it's *slow*

cur-lib/cur/curnel/redex-lang.rkt

@@ -47,6 +47,7 @@
     [dep-void void])
   begin
   Type
+  assume
   ;; DYI syntax extension
   define-syntax
   begin-for-syntax
@@ -483,3 +484,15 @@
        (extend-Γ/term! gamma id (type-infer/term e))
        (add-binding/term! id e)
        #'(void))]))
+
+(define-syntax (assume syn)
+  (syntax-parse syn
+    [(_ id:id t)
+     (let ()
+       (printf "WARNING: Assuming ~a of type ~a.~n"
+               (syntax->datum #'id)
+               (syntax->datum #'t))
+       ;; NB: Have to roll our own namespace rather than use built-in define so id is resolved at
+       ;; compile time in redex, and at runtime in racket.
+       (extend-Γ/syn! gamma #'id #'t)
+       #'(void))]))

cur-test/cur/tests/stdlib/nat-theorem.rkt

@@ -0,0 +1,38 @@
+#lang cur
+
+(require
+ cur/stdlib/sugar
+ cur/stdlib/nat
+ cur/stdlib/prop)
+
+
+(assume f_equal
+        (-> (A : Type) (a1 : A) (a2 : A) (B : Type) (f : (-> A B))
+            (== A a1 a2)
+            (== B (f a1) (f a2))))
+(define plus_0_n
+  (elim Nat Type
+        (lambda (n : Nat) (== Nat n (plus z n)))
+        (refl Nat z)
+        (lambda (n : Nat) (ih : (== Nat n (plus z n)))
+                (f_equal Nat n (plus z n) Nat s ih))))
+
+;; TODO: implicits
+;; No way to define axioms in Cur, yet, although it is a simple change.
+;; No implicits in Cur, yet
+#;(define (plus_0_n  (n : Nat))
+  (match n
+    ;; TODO: This should work
+    #:return (== Nat n (plus z n))
+    [z (refl Nat z)]
+    [(s (n : Nat))
+     (f_equal Nat n (plus z n) Nat s (recur n))]))
+(:: plus_0_n (forall (n : Nat) (== Nat n (plus z n))))
+
+#;(define (plus_n_Sm (n : Nat) (m : Nat))
+  (elim Nat Type
+        (lambda (n : Nat) (== Nat (plus n m) (plus m n)))
+        (plus_n_0 m)
+        (lambda (y : Nat) (ih : ))
+        (elim == Type)))
+#;(:: plus_n_Sm (forall (n : Nat) (m : Nat) (== (s (plus n m)) (plus n (s m)))))