no message

source/math.mmt

@@ -35,14 +35,13 @@ theory Logic : http://gl.mathhub.info/MMT/LFX/TypedHierarchy?LFHierarchy =
 	 ded : prop ⟶ type ❘ # ⊦ 1 prec -500 ❘ role Judgment ❘ = DED ❙
 	 ImplicitProof : {A} ⊦ A ❘ # ImplicitProof 1 ❙
 	 rule lf?TermIrrelevanceRule (ded) ([A : prop] ImplicitProof A) ❙
-	 rule lf?PiIrrelevanceRule ❙
 	 
 	 /T Equality on terms. The type A is left implicit and can be inferred by MMT ❙
 	 eq : {A:𝒰 100} A ⟶ A ⟶ bool ❘ # 2 ≐ 3 prec -5 ❘ role Eq ❘ // = EQUAL ❙
 	 
 	 
-	 // coersion : {A : type, P : A ⟶ prop,a} ⊦ P a ⟶ ⟨ A | ([x] ⊦ P x) ⟩ ❘ # coerce 3 %I4❙
-	 // coersion_theorem : {A : type,P : A ⟶ prop,a,p : ⊦ P a} ⊦ eq ⟨ A | ([x] ⊦ P x) ⟩ (coersion A P a p) a ❙
+	 // coercion : {A : type, P : A ⟶ prop,a} ⊦ P a ⟶ ⟨ A | ([x] ⊦ P x) ⟩ ❘ # coerce 3 %I4❙
+	 // coercion_theorem : {A : type,P : A ⟶ prop,a,p : ⊦ P a} ⊦ eq ⟨ A | ([x] ⊦ P x) ⟩ (coercion A P a p) a ❙
 	 
 	 rule rules?BooleanLiterals ❙
 	 
@@ -136,9 +135,9 @@ theory IntLiterals : ur:?PLF =
 	rule rules?IntMinus ❙
 	plus_int_lit : int_lit ⟶ int_lit ⟶ int_lit ❙
 	rule rules?IntPlus ❙
-   	times_int_lit : int_lit ⟶ int_lit ⟶ int_lit ❙
+  times_int_lit : int_lit ⟶ int_lit ⟶ int_lit ❙
 	rule rules?IntTimes ❙
-   	leq_int_lit : int_lit ⟶ int_lit ⟶ bool ❙
+  leq_int_lit : int_lit ⟶ int_lit ⟶ bool ❙
 	rule rules?IntLeq ❙
 ❚
 	
@@ -150,9 +149,9 @@ theory RealLiterals : ur:?LF =
 	
 	leq_real_lit : real_lit ⟶ real_lit ⟶ bool ❙
    	rule rules?RealLeq ❙
-   	minus_real_lit : real_lit ⟶ real_lit   # - 1 prec 25 ❙
+   	minus_real_lit : real_lit ⟶ real_lit  ❘ # - 1 prec 25 ❙
    	rule rules?RealMinus ❙   
-   	plus_real_lit : real_lit ⟶ real_lit ⟶ real_lit  # 1 + 2 prec 25 ❙
+   	plus_real_lit : real_lit ⟶ real_lit ⟶ real_lit ❘ # 1 + 2 prec 25 ❙
 	rule rules?RealPlus ❙
    	times_real_lit : real_lit ⟶ real_lit ⟶ real_lit ❘ # 1 × 2 prec 20 ❙
 	rule rules?RealTimes ❙
@@ -208,6 +207,7 @@ theory Strings : ur:?LF =
    include ?Logic❙
    string: type ❙
 	 rule rules?StringLiterals ❙
+	 concat: string ⟶ string ⟶ string❙
 ❚
 
 /T Now some more complex types. First lists.❚
@@ -289,8 +289,6 @@ theory DescriptionOperator : ur:?PLF =
 	if_false : {A : 𝒰 100, P : bool, a : A, b : A, p : ⊦ ¬ P } ⊦ (if P then a else b) ≐ b ❘ // = [A,P,a,b,p] _ ❘ ❙
 ❚
 
-/T Finally, a theory that puts everything together (not recommended, because modularity) ❚
-
 theory ProductTypes : http://gl.mathhub.info/MMT/LFX/Sigma?LFSigma =
 	// to have it in the meta-theory ❙                       
 ❚
@@ -300,8 +298,6 @@ theory InductiveTypes : http://gl.mathhub.info/MMT/LFX/WTypes?Inductive =
 ❚
 
 theory Sequences =
-	// Ditto ❙
-	/T Just an alternative notation: ❙
 	include ur:?Sequences ❙
 	include ur:?LFS ❙
 	include ?Logic ❙
@@ -310,6 +306,8 @@ theory Sequences =
 	exists_seq : {A: type}{n} (A^n ⟶ prop) ⟶ prop ❘ # ∃n 3 prec -101 ❘ = [A,n][P] ¬ forall_seq A n [s : A^n] ¬ (P s)❙
 ❚
 
+/T Finally, a theory that puts everything together (not recommended, because modularity) ❚
+
 theory Math : ur:?PLF =
 	include ?Subtyping ❙
 	include ?Logic ❙