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) ❙ // "unparsed"❙
❚

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,… } ❙ // could probably replaced by cons in FiniteSet and subtyping ❙
	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 ) ❙
	
	test1 : A / R ❘ = [a]_ R ❙ // works, but breaks without the space after _ ! ❙
	test2 : A ❘ = rep(test1) ❙ // works ❙
❚