Automatically replace old LF symbols and delimiters

source/draft-structure.mmt

-namespace http://mathhub.info/MitM/smglom/draft-0 
+namespace http://mathhub.info/MitM/smglom/draft-0 ❚
 
 
-import base http://mathhub.info/MitM/Foundation 
+import base http://mathhub.info/MitM/Foundation ❚
 
 // This is an outline of how to design the MitM for group theory 
 //
@@ -21,29 +21,29 @@ import base http://mathhub.info/MitM/Foundation
 // Subgroup
 // subset of group that is closed
 
-// AllSubgroups : {G : Group} → Set (of subgroups of G)
+// AllSubgroups : {G : Group} ⟶ Set (of subgroups of G)
 
 // Subgroups via embeddings:
-// subgroup : {G : Group} → (injection H → G)
+// subgroup : {G : Group} ⟶ (injection H ⟶ G)
 
-// Cosets {G : Group} → U : Subgroup G → Set 
+// Cosets {G : Group} ⟶ U : Subgroup G ⟶ Set 
 
 
 
 // Group Action (what about pairs?)
 // really these are permutation actions...
 // need both left- and right-actions 
-// left-action : {X : Set} → {G : Group} → X × G → X
-// right-action : {X : Set} → {G : Group} → G × X → X
+// left-action : {X : Set} ⟶ {G : Group} ⟶ X × G ⟶ X
+// right-action : {X : Set} ⟶ {G : Group} ⟶ G × X ⟶ X
 //
-// also: action : {X : Set} → {G : Group} → G → SymmetricGroup(X)
+// also: action : {X : Set} ⟶ {G : Group} ⟶ G ⟶ SymmetricGroup(X)
 // Formalise the "isomorphism" between the two?
 // What about Automorphism groups of stuff? If we have a graph Γ and a group G
 // then we act on Γ by graph automorphisms
 
 // for any group action `act` we define
-// stabiliser : {act : GroupAction} → groundset act → Subgroup of G
-// orbit : {act : GroupAction} → groundset act → Subset (groundset act)
+// stabiliser : {act : GroupAction} ⟶ groundset act ⟶ Subgroup of G
+// orbit : {act : GroupAction} ⟶ groundset act ⟶ Subset (groundset act)
 // 
 
 // Centraliser

source/types.mmt

-namespace http://www.gap-system.org/ 
-import rules scala://GAP.odk.mmt.kwarc.info
+namespace http://www.gap-system.org/ ❚
+import rules scala://GAP.odk.mmt.kwarc.info❚
 
 theory Types : ur:?PLF =
-	object : type 
-	category : type 
+	object : type ❙
+	category : type ❙
 	
-	filter = object → type 
+	filter = object ⟶ type ❙
 	
-	constant # : object → filter → type  //  = [o][f] f o  # 1 # 2 
+	constant # : object ⟶ filter ⟶ type ❘ //  = [o][f] f o ❘ # 1 # 2 ❙
 	
-	filter_and : filter → filter → filter  # 1 and 2 
-	filter_and_hasFilter1 : {x,f : filter,g : filter} x # f → x # g → x # (f and g) 
-	filter_and_hasFilter2 : {x,f : filter,g : filter} x # (f and g) → x # f 
-	filter_and_hasFilter3 : {x,f : filter,g : filter} x # (f and g) → x # g 
+	filter_and : filter ⟶ filter ⟶ filter ❘ # 1 and 2 ❙
+	filter_and_hasFilter1 : {x,f : filter,g : filter} x # f ⟶ x # g ⟶ x # (f and g) ❙
+	filter_and_hasFilter2 : {x,f : filter,g : filter} x # (f and g) ⟶ x # f ❙
+	filter_and_hasFilter3 : {x,f : filter,g : filter} x # (f and g) ⟶ x # g ❙
 	
-	ded : object → type 
+	ded : object ⟶ type ❙
 	
-	rule rules?Booleans 
-	rule rules?Integers 
-	rule rules?Floats 
+	rule rules?Booleans ❙
+	rule rules?Integers ❙
+	rule rules?Floats ❙
 	
-	booleans : type 
-	integers : type 
-	floats : type 
-	gapbool : booleans → object 
-	gapint : integers → object 
-	gapfloat : floats → object 
+	booleans : type ❙
+	integers : type ❙
+	floats : type ❙
+	gapbool : booleans ⟶ object ❙
+	gapint : integers ⟶ object ❙
+	gapfloat : floats ⟶ object ❙
 	
-	trueI : ded (gapbool true) 
-	catFilter : category → filter 
-	propertyFilter : (object → object) → filter  = [p] [o] ded (p o) 
+	trueI : ded (gapbool true) ❙
+	catFilter : category ⟶ filter ❙
+	propertyFilter : (object ⟶ object) ⟶ filter ❘ = [p] [o] ded (p o) ❙
 	
-	Has : (object → object) → filter 
-	CategoryCollection : filter → category 
-	Set : filter → (object → object) 
-	IsBool : category 
-	IsObject : category 
-	// HasIsProperty : {o,x} x # (propertyFilter o) → ((Has o) x) # catFilter IsBool 
+	Has : (object ⟶ object) ⟶ filter ❙
+	CategoryCollection : filter ⟶ category ❙
+	Set : filter ⟶ (object ⟶ object) ❙
+	IsBool : category ❙
+	IsObject : category ❙
+	// HasIsProperty : {o,x} x # (propertyFilter o) ⟶ ((Has o) x) # catFilter IsBool ❙
 	
-
+❚
 
 //   theory Types : odk:?Math =
-	Object : tp 
+	Object : tp ❙
 
-	Family : tp 
-	Family_Of_Families : tm Family 
-	Families_are_Objects : Family < Object 
-	Family_Of_Object : tm Object → tm Family  # FamilyOfObj 1 
-	Family_Of_Family_is_Family_of_Families : {F:tm Family} ⊦ eq Family (FamilyOfObj (tpCast Families_are_Objects F)) Family_Of_Families 
+	Family : tp ❙
+	Family_Of_Families : tm Family ❙
+	Families_are_Objects : Family < Object ❙
+	Family_Of_Object : tm Object ⟶ tm Family ❘ # FamilyOfObj 1 ❙
+	Family_Of_Family_is_Family_of_Families : {F:tm Family} ⊦ eq Family (FamilyOfObj (tpCast Families_are_Objects F)) Family_Of_Families ❙
 
-	Filter : tp 
-	Elementary_Filter : tp 
-	Elementary_Filter_Is_Filter : Elementary_Filter < Filter 
+	Filter : tp ❙
+	Elementary_Filter : tp ❙
+	Elementary_Filter_Is_Filter : Elementary_Filter < Filter ❙
 
-	Filter_applies : tm Filter → tm Object → prop  # 1 _ 2 
+	Filter_applies : tm Filter ⟶ tm Object ⟶ prop ❘ # 1 _ 2 ❙
 	
-	filter_conj : tm Filter → tm Filter → tm Filter  # 1 + 2 prec 5
-	filter_conj_is_Conjunction : {F1,F2,O} ⊦ ((F1 + F2) _ O) ≐ ((F1 _ O) ∧ (F2 _ O))  role Simplify 
-	filter_conj_is_associative : {F1,F2,F3} ⊦ F1 + (F2 + F3) ≐ (F1 + F2) + F3 
-	filter_conj_is_commutative : {F1,F2} ⊦ F1 + F2 ≐ F2 + F1 
+	filter_conj : tm Filter ⟶ tm Filter ⟶ tm Filter ❘ # 1 + 2 prec 5❙
+	filter_conj_is_Conjunction : {F1,F2,O} ⊦ ((F1 + F2) _ O) ≐ ((F1 _ O) ∧ (F2 _ O)) ❘ role Simplify ❙
+	filter_conj_is_associative : {F1,F2,F3} ⊦ F1 + (F2 + F3) ≐ (F1 + F2) + F3 ❙
+	filter_conj_is_commutative : {F1,F2} ⊦ F1 + F2 ≐ F2 + F1 ❙
 
-	filter_def : (tm Object → prop) → tm Filter  # MakeFilter 1 
-	filter_def_application : {F,O} ⊦ ((MakeFilter F) _ O) ≐ F O 
+	filter_def : (tm Object ⟶ prop) ⟶ tm Filter ❘ # MakeFilter 1 ❙
+	filter_def_application : {F,O} ⊦ ((MakeFilter F) _ O) ≐ F O ❙
 
-	GAPtype : tp 
-	Family_of_GAPtype : tm GAPtype → tm Family  # FamilyOfTp 1 
-	Filter_of_GAPtype : tm GAPtype → tm list Elementary_Filter   # FilterOf 1 
-	GAPtype_Constructor : tm Family → tm list Elementary_Filter → tm GAPtype  # GAPtp 1 2 
-	// Filter_applies_to_type_object : {O} ⊦ (FilterOf O) _ O 
+	GAPtype : tp ❙
+	Family_of_GAPtype : tm GAPtype ⟶ tm Family ❘ # FamilyOfTp 1 ❙
+	Filter_of_GAPtype : tm GAPtype ⟶ tm list Elementary_Filter  ❘ # FilterOf 1 ❙
+	GAPtype_Constructor : tm Family ⟶ tm list Elementary_Filter ⟶ tm GAPtype ❘ # GAPtp 1 2 ❙
+	// Filter_applies_to_type_object : {O} ⊦ (FilterOf O) _ O ❙
 	
-	Operation : tp 
-	Name_of_Operation : tm Operation → tm string 
-	Arglength_of_Operation : tm Operation → tm ℕ 
-	Filter_of_Operation : {op: tm Operation} tm vector Filter (Arglength_of_Operation op) 
-	Operation_Constructor : {name: tm string, args: tm ℕ} tm vector Filter args → tm Operation 
+	Operation : tp ❙
+	Name_of_Operation : tm Operation ⟶ tm string ❙
+	Arglength_of_Operation : tm Operation ⟶ tm ℕ ❙
+	Filter_of_Operation : {op: tm Operation} tm vector Filter (Arglength_of_Operation op) ❙
+	Operation_Constructor : {name: tm string, args: tm ℕ} tm vector Filter args ⟶ tm Operation ❙
 	
-	Category : tp 
-	Category_is_elementary_Filter : Category < Elementary_Filter 
+	Category : tp ❙
+	Category_is_elementary_Filter : Category < Elementary_Filter ❙
 	
-	Property : tp 
-	Property_is_elementary_Filter : Property < Elementary_Filter 
-	Has : tm Property → tm Elementary_Filter 
-	OperationFromProperty : tm Property → tm Operation 
-	OperationSet : tm Property → tm Operation  # Set 1 
-
\ No newline at end of file
+	Property : tp ❙
+	Property_is_elementary_Filter : Property < Elementary_Filter ❙
+	Has : tm Property ⟶ tm Elementary_Filter ❙
+	OperationFromProperty : tm Property ⟶ tm Operation ❙
+	OperationSet : tm Property ⟶ tm Operation ❘ # Set 1 ❙
+❚
\ No newline at end of file