Add type-inferring constructors

Convention: /i denotes a type-inferring version of something.

stdlib/maybe.rkt

@@ -1,13 +1,22 @@
 #lang s-exp "../cur.rkt"
 (require "sugar.rkt")
-(provide Maybe none some)
+(provide Maybe none some some/i)
 
 (data Maybe : (forall (A : Type) Type)
   (none : (forall (A : Type) (Maybe A)))
   (some : (forall* (A : Type) (a : A) (Maybe A))))
 
+(define-syntax (some/i syn)
+  (syntax-case syn ()
+   [(_ a)
+    (let ([a-ty (type-infer/syn #'a)])
+      #`(some #,a-ty a))]))
+
 (module+ test
   (require rackunit "bool.rkt")
+  (check-equal?
+   (some/i true)
+   (some Bool true))
   ;; Disabled until #22 fixed
   #;(check-equal?
     (case* Maybe Type (some Bool true) (Bool)

stdlib/prop.rkt

@@ -8,7 +8,7 @@
   False
   Not
   And
-  conj
+  conj conj/i
   thm:and-is-symmetric proof:and-is-symmetric
   thm:proj1 proof:proj1
   thm:proj2 proof:proj2
@@ -28,6 +28,13 @@
   (conj : (forall* (A : Type) (B : Type)
             (x : A) (y : B) (And A B))))
 
+(define-syntax (conj/i syn)
+  (syntax-case syn ()
+    [(_ a b)
+     (let ([a-type (type-infer/syn #'a)]
+           [b-type (type-infer/syn #'b)])
+       #`(conj #,a-type #,b-type a b))]))
+
 (define-theorem thm:and-is-symmetric
   (forall* (P : Type) (Q : Type) (ab : (And P Q)) (And Q P)))
 
@@ -36,7 +43,7 @@
     (case* And Type ab (P Q)
       (lambda* (P : Type) (Q : Type) (ab : (And P Q))
          (And Q P))
-      ((conj (P : Type) (Q : Type) (x : P) (y : Q)) IH: () (conj Q P y x)))))
+      ((conj (P : Type) (Q : Type) (x : P) (y : Q)) IH: () (conj/i y x)))))
 
 (qed thm:and-is-symmetric proof:and-is-symmetric)
 
@@ -94,4 +101,7 @@
          true
          true
          (refl Bool true))
-    z))
+    z)
+  (check-equal?
+   (conj/i (conj/i T T) T)
+   (conj (And True True) True (conj True True T T) T)))