Clean up examples

Beluga-lang · Jan 13, 2025 · d74b93d · d74b93d
1 parent c33ec07
commit d74b93d
Show file tree

Hide file tree

Showing 4 changed files with 55 additions and 34 deletions.
diff --git a/examples/let_nary.mctt b/examples/let_nary.mctt
@@ -17,28 +17,34 @@ let ((Nary : forall (n : Nat) -> Type@0) :=
        fun (n : Nat)
            (f : rec succ n return y . Type@0
                 | zero => Nat
-           	| succ m, r => forall (a : Nat) -> r
-           	end)
+            | succ m, r => forall (a : Nat) -> r
+            end)
            (arg : Nat)
          -> f arg
      ))
 
     ((n : Nat) := 3)
     ((f : Nary n) :=
      (
-       (fun (add : forall (a : Nat) (b : Nat) -> Nat) -> (fun (a : Nat) (b : Nat) (c : Nat) -> add a (add b c)))
-       (
-         fun (a : Nat)
-             (b : Nat)
-      	   -> rec a return y . Nat
-              | zero => b
-              | succ m, r => succ r
-              end
-       )
+       let ((add : forall (a : Nat) (b : Nat) -> Nat) :=
+            (fun (a : Nat)
+                 (b : Nat)
+               -> rec a return y . Nat
+                  | zero => b
+                  | succ m, r => succ r
+                  end))
+       in
+       fun (a : Nat) (b : Nat) (c : Nat) -> add a (add b c)
      ))
 
 in
   ((rec n return y . (forall (g : Nary y) -> Nat)
        | zero => toNat
        | succ m, r => fun (g : Nary (succ m)) -> r (appNary m g (succ m))
-       end) f) : Nat
+       end) f) : Nat
+(*
+  Basically:
+  f 3 2 1
+  where
+  f x y z = x + (y + z)
+*)
diff --git a/examples/let_two_vars.mctt b/examples/let_two_vars.mctt
@@ -1 +1 @@
-let ((x : Nat) := 0) ((f : forall (y : Nat) -> Nat) := (fun (n : Nat) -> n)) in f x : Nat
+let ((x : Nat) := 0) ((f : forall (y : Nat) -> Nat) := (fun (n : Nat) -> n)) in f x : Nat
diff --git a/examples/let_vector.mctt b/examples/let_vector.mctt
@@ -3,34 +3,49 @@ let ((Vec : forall (A : Type@0) (n : Nat) -> Type@2) :=
      (fun (A : Type@0) (n : Nat) -> forall (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> C n))
 
     ((nil : forall (A : Type@0) -> Vec A 0) :=
-     (fun (A : Type@0) (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> nil))
+     (fun (A : Type@0)
+          (C : forall (l : Nat) -> Type@1)
+          (nil : C 0)
+          (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) ->
+        nil
+     ))
 
     ((cons : forall (A : Type@0) (n : Nat) (head : A) (tail : Vec A n) -> Vec A (succ n)) :=
-     (fun (A : Type@0) (n : Nat) (head : A) (tail : forall (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> C n) (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> cons n head (tail C nil cons)))
+     (fun (A : Type@0)
+          (n : Nat)
+          (head : A)
+          (tail : forall (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> C n)
+          (C : forall (l : Nat) -> Type@1)
+          (nil : C 0)
+          (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) ->
+        cons n head (tail C nil cons)
+     ))
 
     ((vecRec : forall (A : Type@0) (n : Nat) (vec : Vec A n) (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> C n) :=
      (fun (A : Type@0) (n : Nat) (vec : forall (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> C n) (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> vec C nil cons))
 
-in (let ((totalHead : forall (A : Type@0) (n : Nat) (vec : Vec A (succ n)) -> A) :=
-   	 (
-       	  fun (A : Type@0) (n : Nat) (vec : Vec A (succ n)) ->
+in
+let ((totalHead : forall (A : Type@0) (n : Nat) (vec : Vec A (succ n)) -> A) :=
+     (fun (A : Type@0) (n : Nat) (vec : Vec A (succ n)) ->
            vecRec A (succ n) vec (fun (l : Nat) -> rec l return r . Type@0 | zero => Nat | succ l, r => A end) 0 (fun (l : Nat) (a : A) (r : rec l return r . Type@0 | zero => Nat | succ l, r => A end) -> a)
-      	 ))
+     ))
 
-	((vec : Vec (forall (n : Nat) -> Nat) 3) :=
-	 (
-           cons (forall (n : Nat) -> Nat) 2
-             (fun (n : Nat) -> succ (succ (succ n)))
-             (
-               cons (forall (n : Nat) -> Nat) 1
+    ((vec : Vec (forall (n : Nat) -> Nat) 3) :=
+     (cons (forall (n : Nat) -> Nat) 2
+           (fun (n : Nat) -> succ (succ (succ n)))
+           (cons (forall (n : Nat) -> Nat) 1
                  (fun (n : Nat) -> succ n)
-              	 (
-                   cons (forall (n : Nat) -> Nat) 0
-                     (fun (n : Nat) -> succ (succ n))
-                     (nil (forall (n : Nat) -> Nat))
+                 (cons (forall (n : Nat) -> Nat) 0
+                       (fun (n : Nat) -> succ (succ n))
+                       (nil (forall (n : Nat) -> Nat))
                  )
              )
-         ))
-
-   in totalHead ((forall (n : Nat) -> Nat)) 2 vec 4)
-) : Nat
+     ))
+in
+totalHead ((forall (n : Nat) -> Nat)) 2 vec 4
+) : Nat
+(*
+  When
+    vec = [fun x -> 3 + x; fun x -> 1 + x; fun x -> 2 + x]
+  we get its head (fun x -> 3 + x) and applies it to 4.
+*)
diff --git a/examples/simple_let.mctt b/examples/simple_let.mctt
@@ -1 +1 @@
-let ((x : Nat) := zero) in succ x : Nat
+let ((x : Nat) := zero) in succ x : Nat
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		let ((x : Nat) := 0) ((f : forall (y : Nat) -> Nat) := (fun (n : Nat) -> n)) in f x : Nat
		let ((x : Nat) := 0) ((f : forall (y : Nat) -> Nat) := (fun (n : Nat) -> n)) in f x : Nat
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		let ((x : Nat) := zero) in succ x : Nat
		let ((x : Nat) := zero) in succ x : Nat