diff --git a/content/http..www.gap-system.org/mitm/prim.omdoc.xz b/content/http..www.gap-system.org/mitm/prim.omdoc.xz new file mode 100644 index 0000000000000000000000000000000000000000..72d0bdafee404bd1bec725e28aea363e788cc94b Binary files /dev/null and b/content/http..www.gap-system.org/mitm/prim.omdoc.xz differ diff --git a/narration/primitives.omdoc b/narration/primitives.omdoc new file mode 100644 index 0000000000000000000000000000000000000000..af023ba7c91c02eeea8cb51bb079d9d26883f465 --- /dev/null +++ b/narration/primitives.omdoc @@ -0,0 +1,2 @@ +<?xml version="1.0" encoding="UTF-8"?> +<omdoc base="http://www.gap-system.org/primitives.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://www.gap-system.org/primitives.mmt#0.0.0:3045.89.0"/></metadata><mref name="[http://www.gap-system.org/mitm?prim]" target="http://www.gap-system.org/mitm?prim"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://www.gap-system.org/primitives.mmt#44.2.0:54.2.10"/></metadata></mref></omdoc> \ No newline at end of file diff --git a/relational/http..www.gap-system.org/mitm/prim.rel b/relational/http..www.gap-system.org/mitm/prim.rel new file mode 100644 index 0000000000000000000000000000000000000000..a2fe1f9f18f59ad3d47fafb4f27b97c25b8817e7 --- /dev/null +++ b/relational/http..www.gap-system.org/mitm/prim.rel @@ -0,0 +1,5 @@ +untypedconstant http://www.gap-system.org/mitm?prim?ListConstr +theory http://www.gap-system.org/mitm?prim +HasMeta http://www.gap-system.org/mitm?prim http://www.gap-system.org?Types +Declares http://www.gap-system.org/mitm?prim http://www.gap-system.org/mitm?prim?ListConstr +constant http://www.gap-system.org/mitm?prim?ListConstr diff --git a/relational/primitives.rel b/relational/primitives.rel new file mode 100644 index 0000000000000000000000000000000000000000..b680eac61bbf438c1288ea910ebfe377e20827a3 --- /dev/null +++ b/relational/primitives.rel @@ -0,0 +1,2 @@ +document http://www.gap-system.org/primitives.omdoc +Declares http://www.gap-system.org/primitives.omdoc http://www.gap-system.org/mitm?prim diff --git a/source/alignment.mmt b/source/alignment.mmt index b444533d2a7e955e9362dc4f3392f38bb8cf3faf..1c5d5ed628dea85a6f24d3f620a1d6506fb619ad 100644 --- a/source/alignment.mmt +++ b/source/alignment.mmt @@ -1 +1,5 @@ -namespace http://www.gap-system.org ⚠\ No newline at end of file +namespace http://www.gap-system.org ⚠+ +theory Alignments : mitm?lib = + DihedralGroup = [d] `lib?DihedralGroup `lib?IsPermGroup d ♠+⚠\ No newline at end of file diff --git a/source/primitives.mmt b/source/primitives.mmt new file mode 100644 index 0000000000000000000000000000000000000000..caff72895c7becd0faf195baebfea69619b9b5cb --- /dev/null +++ b/source/primitives.mmt @@ -0,0 +1,90 @@ +namespace http://www.gap-system.org/mitm ⚠+ +theory prim : ../?Types = + ListConstr ♠+⚠+ +// theory Types : ur:?PLF = + object : type ♠+ category : type ♠+ + booleans : type ♠+ integers : type ♠+ floats : type ♠+ + filter = object ⟶ type ♠+ + hastp : object ⟶ filter ⟶ type ☠// = [o][f] f o ☠# 1 $ 2 ♠+ + filter_and : filter ⟶ filter ⟶ filter ☠# 1 and 2 ♠+ filter_and_hasFilter1 : {x : object,f : filter,g : filter} x $ f ⟶ x $ g ⟶ x $ (f and g) ♠+ filter_and_hasFilter2 : {x : object,f : filter,g : filter} x $ (f and g) ⟶ x $ f ♠+ filter_and_hasFilter3 : {x : object,f : filter,g : filter} x $ (f and g) ⟶ x $ g ♠+ + ded : object ⟶ type ♠+ + rule rules?Booleans ♠+ rule rules?Integers ♠+ rule rules?Floats ♠+ + 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) ♠+ + 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 ♠+ + 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_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_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 ♠+ + 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 ♠+ + 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