init

source/test.mmt

+namespace http://mathhub.info/MitM/NewFoundation ❚
+
+// I left out all of the basic theories just to make sure that only
+the notations in this file are around ❚
+theory Basics =
+	brackets # ( 1 ) prec -100000 ❙
+	f ❙
+	a ❙
+	b ❙
+	c ❙
+	p ❙
+	A ❙
+	B ❙
+	C ❙
+	t ❙
+	ls ❙
+	
+	T ❙
+	P ❙
+	R ❙
+❚
+
+theory Pi : ?Basics =
+	pi # { V1T ,… } 2 prec -10000 ❙
+	arrow # 1⟶… prec -9999 ❙
+    apply1  # 1%w… prec -10 ❙
+	apply2 # 1(2,…) prec -100000 ❙
+	lambda # [ V1T ,… ] 2 prec -10000 ❙
+	
+	test1 : f a b ❙ // works ❙
+	test2 : f(a,b) ❙ // unbound token "," ❙
+❚
+
+theory Sigma : ?Basics =
+	sigma # Σ { V1T,… } prec -10000 ❙
+	tuple # ( 1,… ) prec -100000 ❙
+	tuple_entry # 1 . 2 prec -1000 ❙
+	
+	test1 : Σ { a : A, b : B a} ❙ // should work apart from ":" ❙
+	test2 : ( a,b ) ❙ // "unparsed" ❙
+	test3 : t.5 ❙ // works ❙
+❚
+
+theory Sequences : ?Basics =
+	seq # 1 ^* ❙
+	nil # nil %I1 ❙
+	cons # 1 :: 2 ❙
+	list_entry # 1 . 2 prec -1000 ❙	// ? ❙
+	match # 3 match case nil => 4 case V1 :: V2 => 5 prec -500 ❙ // variables apparently need to be the
+		first arguments? ❙
+	
+	test1 : A^* ❙ // works ❙
+	test2 : a :: ls ❙ // works ❙
+	test3 : a.5 ❙ // works ❙
+	test4 : ls match case nil => A case head::tail => (f head tail) ❙ // works ❙
+❚
+
+theory Options : ?Basics =
+	option # Option[ 1 ] ❙
+	some # Some( 1 ) ❙
+	none # None %I1 ❙
+	match # 2 match case None => 3 case Some( V1 ) => 4 prec -500 ❙
+	
+	test1 : Option[A] ❙ // works (except for possibly LFLambda?) ❙
+	test2 : Some(a) ❙ // works ❙
+	test3 : A ❘ = a match case None => b case Some(x) => c ❙ // this breaks somehow ❙
+❚
+
+// ℬ, ℕ, ℤ, ℚ, ℝ, ℂ ❚
+
+theory Mod : ?Basics =
+	mod # Mod 1 ❙
+	cons # ⟨ L1,… ⟩ ❙
+	elim # 1 . L2 ❙
+	
+	test1 : Mod T ❙ // works ❙
+	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
+❚
+
+theory FiniteSet : ?Basics =
+	finset # ℘n 1 ❙
+	in # 1 ‍∈ 2 ❙
+	cons # { 1,… } ❙
+	
+	test1 : ℘n A ❘ = { a, a, b, c, c, c } ❙ // works ❙
+	test2 : a ‍∈ test1 ❙ // works ❙
+❚
+
+theory MultiSet : ?Basics =
+	multiset # ℘m 1 ❙
+	cons # { 1,… } ❙
+	mul # mul( 1 , 2 ) ❙
+	
+	test1 : ℘m A ❘ = { a, a, b, c, c, c } ❙
+	test2 : ⊢ mul (test1,c) ≐ 3 ❙ // brackets! ❙
+❚
+
+// "A^n" - tuples? I dunno... ❚
+
+theory InfiniteSequences : ?Basics =
+	// pretty much identical to finite sequences, notationwise. Probably additional introduction
+	form via ℕ ⟶ A or induction? ❙
+	infseq # 1 ^≤ω ❙
+	nil # nil %I1 ❙
+	cons # 1 :: 2 ❙
+	seq_entry # 1 . 2 prec -1000 ❙	// ? ❙
+	match # 3 match case nil => 4 case V1 :: V2 => 5 prec -500 ❙
+	
+	test1 : A^≤ω ❙ // works ❙
+	test2 : a :: ls ❙ // works ❙
+	test3 : a.5 ❙ // works ❙
+	test4 : ls match case nil => A case head :: tail => (f head tail) ❙ // works ❙
+❚
+
+theory InfiniteSets : ?Basics =
+	set # ℘ 1 ❙
+	in # 1 ‍∈ 2 ❙
+	cons1 # { 1,… } ❙
+	cons2 # { V1 ‍: 2 | 3 } prec -500❙
+	
+	test1 : ℘ A ❘ = { a, a, b, c, c, c } ❙ // works ❙
+	test2 : ℘ A ❘ = { x ‍: A | P x } ❙ // works (SO FAR! colon in notation might be problematic) ❙
+	test3 : a ‍∈ test1 ❙ // works ❙
+❚
+
+theory PredSubtype : ?Basics =
+	predsub # ⟨ V1 : 2 | 3 ⟩ ❙
+	prf # prf 1 ❙ // idea: For x : ⟨ y : A | P y ⟩ we would have (prf x) : P x  ? ❙
+	coerce # 1 ↪ 2 ❙ // idea: For some p : P a we have (a ↪ p) : ⟨ x : A | P x ⟩  ? ❙
+	
+	test1 : ⟨ x : A | P x ⟩ ❙ // works ❙
+	test2 : prf test1 ❙ // works ❙
+	test3 : ⟨ x : A | P x ⟩ ❘ = (a ↪ p) ❙ // works ❙
+❚
+
+theory Quotients : ?Basics =
+	Quot # 1 / 2 ❙ // <type> / <relation> ❙
+	injection # [ 1 ]_ 2 ❙ // [a]_R ❙
+	representative # rep( 1 ) ❙ // requires axiom of choice ❙
+	
+	test1 : A / R ❘ = [a]_ R ❙ // works, but breaks without the space after _ ! ❙
+	test2 : A ❘ = rep(test1) ❙ // works ❙
+❚
\ No newline at end of file