up

Author: xieyuheng

docs/examples/factorial-wrap.scm

@@ -5,7 +5,7 @@
 
 ;; (claim factorial-wrap (-> (-> Nat Nat) (-> Nat Nat)))
 ;; (claim (Y factorial-wrap) (-> Nat Nat))
-;; (claim Y (forall (A) (-> (-> A A) A)))
+;; (claim Y (nu (A) (-> (-> A A) A)))
 
 (define factorial-wrap
   (lambda (factorial)

docs/examples/nat-church.scm

@@ -12,22 +12,22 @@
 ;; We know
 
 ;; (claim zero
-;;   (forall (X)
+;;   (nu (X)
 ;;     (-> X (-> X X) X)))
 
 ;; Thus
 
 ;; (define Nat
-;;   (forall (X)
+;;   (nu (X)
 ;;     (-> X (-> X X) X)))
 
 ;; (claim add1
 ;;   (-> Nat Nat)
-;;   (forall (X)
+;;   (nu (X)
 ;;     (-> Nat (-> X (-> X X) X))))
 
 ;; (claim iter-Nat
-;;   (forall (X)
+;;   (nu (X)
 ;;     (-> Nat (-> X (-> X X) X))))
 
 ;; # one to ten

docs/examples/nat-parigot.scm

@@ -9,16 +9,16 @@
 ;; ## Typing
 
 ;; (claim zero
-;;   (forall (X)
+;;   (nu (X)
 ;;     (-> X (-> Nat X X) X)))
 
 ;; (define Nat
-;;   (forall (X)
+;;   (nu (X)
 ;;     (-> X (-> Nat X X) X)))
 
 ;; (claim add1
 ;;   (-> Nat Nat)
-;;   (forall (X)
+;;   (nu (X)
 ;;     (-> Nat (-> X (-> Nat X X) X))))
 
 ;; # one to ten

docs/examples/nat-scott.scm

@@ -11,20 +11,20 @@
 ;; ## Typing
 
 ;; (claim zero
-;;   (forall (X)
+;;   (nu (X)
 ;;     (-> X (-> Nat X) X)))
 
 ;; (define Nat
-;;   (forall (X)
+;;   (nu (X)
 ;;     (-> X (-> Nat X) X)))
 
 ;; (claim add1
 ;;   (-> Nat Nat)
-;;   (forall (X)
+;;   (nu (X)
 ;;     (-> Nat (-> X (-> Nat X) X))))
 
 ;; (claim which-Nat
-;;   (forall (X)
+;;   (nu (X)
 ;;     (-> Nat (-> X (-> Nat X) X))))
 
 ;; # one to ten