update

source/test.mmt

@@ -24,11 +24,11 @@ theory Pi : ?Basics =
 	pi # { V1T ,… } 2 prec -10000 ❙
 	arrow # 1⟶… prec -9999 ❙
     apply1  # 1%w… prec -10 ❙
-	apply2 # 1(2,…) prec -100000 ❙
+	apply2 # 1 ( 2,… ) prec -100000 ❙
 	lambda # [ V1T ,… ] 2 prec -10000 ❙
 	
 	test1 : f a b ❙ // works ❙
-	test2 : f(a,b) ❙ // unbound token "," ❙
+	test2 : f(a,b) ❙ // "unparsed"❙
 ❚
 
 theory Sigma : ?Basics =
@@ -36,8 +36,8 @@ theory Sigma : ?Basics =
 	tuple # ( 1,… ) prec -100000 ❙
 	tuple_entry # 1 . 2 prec -1000 ❙
 	
-	test1 : Σ { a : A, b : B a} ❙ // should work apart from ":" ❙
-	test2 : ( a,b ) ❙ // "unparsed" ❙
+	test1 : Σ{a : A, b : B a} ❙ // should work apart from ":" ❙
+	test2 : (a,b) ❙ // "unparsed" ❙
 	test3 : t.5 ❙ // works ❙
 ❚
 
@@ -74,16 +74,16 @@ theory Mod : ?Basics =
 	elim # 1 . L2 ❙
 	
 	test1 : Mod T ❙ // works ❙
-	test2 : Mod T ❘ = ⟨ a1 := a, b1 := b ⟩ ❙ // works except for ":=" notations missing ❙
+	test2 : Mod T ❘ = ⟨a1 := a, b1 := b⟩ ❙ // works except for ":=" notations missing ❙
 	test3 : test2.a1 ❙ // works (so far) ❙
 ❚
 
 theory Term : ?Basics =
 	// copy paste ❙
-   formation # {| 1 |} 2 prec -10000
-   reflect   # ⌜ 1 : 2 ⌝ prec -10000
-   eval      # ⌞ 1 ⌟ 2   prec -10000
-   elim      # 1 ^ 2     prec -10000
+	formation # {| 1 |} 2 prec -10000
+	reflect   # ⌜ 1 : 2 ⌝ prec -10000
+	eval      # ⌞ 1 ⌟ 2   prec -10000
+	elim      # 1 ^ 2     prec -10000
 ❚
 
 theory FiniteSet : ?Basics =
@@ -91,7 +91,7 @@ theory FiniteSet : ?Basics =
 	in # 1 ‍∈ 2 ❙
 	cons # { 1,… } ❙
 	
-	test1 : ℘n A ❘ = { a, a, b, c, c, c } ❙ // works ❙
+	test1 : ℘n A ❘ = {a, a, b, c, c, c} ❙ // works ❙
 	test2 : a ‍∈ test1 ❙ // works ❙
 ❚
 
@@ -100,7 +100,7 @@ theory MultiSet : ?Basics =
 	cons # { 1,… } ❙
 	mul # mul( 1 , 2 ) ❙
 	
-	test1 : ℘m A ❘ = { a, a, b, c, c, c } ❙
+	test1 : ℘m A ❘ = {a, a, b, c, c, c} ❙
 	test2 : ⊢ mul (test1,c) ≐ 3 ❙ // brackets! ❙
 ❚
 
@@ -116,7 +116,7 @@ theory InfiniteSequences : ?Basics =
 	match # 3 match case nil => 4 case V1 :: V2 => 5 prec -500 ❙
 	
 	test1 : A^≤ω ❙ // works ❙
-	test2 : a :: ls ❙ // works ❙
+	test2 : a::ls ❙ // works ❙
 	test3 : a.5 ❙ // works ❙
 	test4 : ls match case nil => A case head :: tail => (f head tail) ❙ // works ❙
 ❚
@@ -124,7 +124,7 @@ theory InfiniteSequences : ?Basics =
 theory InfiniteSets : ?Basics =
 	set # ℘ 1 ❙
 	in # 1 ‍∈ 2 ❙
-	cons1 # { 1,… } ❙
+	cons1 # { 1,… } ❙ // could probably replaced by cons in FiniteSet and subtyping ❙
 	cons2 # { V1 ‍: 2 | 3 } prec -500❙
 	
 	test1 : ℘ A ❘ = { a, a, b, c, c, c } ❙ // works ❙
@@ -145,7 +145,7 @@ theory PredSubtype : ?Basics =
 theory Quotients : ?Basics =
 	Quot # 1 / 2 ❙ // <type> / <relation> ❙
 	injection # [ 1 ]_ 2 ❙ // [a]_R ❙
-	representative # rep( 1 ) ❙ // requires axiom of choice ❙
+	representative # rep( 1 ) ❙
 	
 	test1 : A / R ❘ = [a]_ R ❙ // works, but breaks without the space after _ ! ❙
 	test2 : A ❘ = rep(test1) ❙ // works ❙