Skip to content
Snippets Groups Projects
Commit b64d2837 authored by Dreier Marcel's avatar Dreier Marcel
Browse files

a bunch of new scrolls and facts

parent 0619da5f
No related branches found
No related tags found
1 merge request!1Added new Scrolls and new Theories
Hide whitespace changes
Inline Side-by-side
content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz
+ 0
− 0
View file @ b64d2837
No preview for this file type
narration/MetaTheories.omdoc
+ 1
− 1
View file @ b64d2837
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#0.0.0:20521.388.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://cds.omdoc.org/urtheories?LF"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#125.5.0:253.5.128"/></metadata>MMT meta keys and value constructors for meta annotations of facts in situation theories and (input/output) facts in scrolls</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?MetaAnnotations]" target="http://mathhub.info/FrameIT/frameworld?MetaAnnotations"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#255.6.0:276.6.21"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?2DPoints]" target="http://mathhub.info/FrameIT/frameworld?2DPoints"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#685.24.1:699.24.15"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITBasics]" target="http://mathhub.info/FrameIT/frameworld?FrameITBasics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#1094.48.0:1113.48.19"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITRectangles]" target="http://mathhub.info/FrameIT/frameworld?FrameITRectangles"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#4340.108.0:4363.108.23"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITTriangles]" target="http://mathhub.info/FrameIT/frameworld?FrameITTriangles"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#7437.158.0:7459.158.22"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITCircle]" target="http://mathhub.info/FrameIT/frameworld?FrameITCircle"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#10771.202.0:10790.202.19"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITCone]" target="http://mathhub.info/FrameIT/frameworld?FrameITCone"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#12754.240.0:12771.240.17"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITCylinder]" target="http://mathhub.info/FrameIT/frameworld?FrameITCylinder"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#16111.295.0:16132.295.21"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITTheories]" target="http://mathhub.info/FrameIT/frameworld?FrameITTheories"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#17019.318.0:17040.318.21"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#19961.370.0:20056.370.95"/></metadata>The meta theory to use for situation theories, scroll problem, and scroll solution theories</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?FrameworldMeta]" target="http://mathhub.info/FrameIT/frameworld?FrameworldMeta"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#20058.371.0:20078.371.20"/></metadata></mref></omdoc> <omdoc base="http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#0.0.0:20627.388.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://cds.omdoc.org/urtheories?LF"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#125.5.0:253.5.128"/></metadata>MMT meta keys and value constructors for meta annotations of facts in situation theories and (input/output) facts in scrolls</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?MetaAnnotations]" target="http://mathhub.info/FrameIT/frameworld?MetaAnnotations"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#255.6.0:276.6.21"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?2DPoints]" target="http://mathhub.info/FrameIT/frameworld?2DPoints"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#685.24.1:699.24.15"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITBasics]" target="http://mathhub.info/FrameIT/frameworld?FrameITBasics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#1094.48.0:1113.48.19"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITRectangles]" target="http://mathhub.info/FrameIT/frameworld?FrameITRectangles"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#4442.108.0:4465.108.23"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITTriangles]" target="http://mathhub.info/FrameIT/frameworld?FrameITTriangles"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#7539.158.0:7561.158.22"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITCircle]" target="http://mathhub.info/FrameIT/frameworld?FrameITCircle"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#10873.202.0:10892.202.19"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITCone]" target="http://mathhub.info/FrameIT/frameworld?FrameITCone"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#12860.240.0:12877.240.17"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITCylinder]" target="http://mathhub.info/FrameIT/frameworld?FrameITCylinder"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#16217.295.0:16238.295.21"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITTheories]" target="http://mathhub.info/FrameIT/frameworld?FrameITTheories"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#17125.318.0:17146.318.21"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#20067.370.0:20162.370.95"/></metadata>The meta theory to use for situation theories, scroll problem, and scroll solution theories</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?FrameworldMeta]" target="http://mathhub.info/FrameIT/frameworld?FrameworldMeta"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#20164.371.0:20184.371.20"/></metadata></mref></omdoc>
\ No newline at end of file \ No newline at end of file
source/MetaTheories.mmt
+ 4
− 4
View file @ b64d2837
...@@ -88,10 +88,10 @@ theory FrameITBasics = ...@@ -88,10 +88,10 @@ theory FrameITBasics =
// projection and distance function for planes ❙ // projection and distance function for planes ❙
helperFunctionForProjection : plane ⟶ point ⟶ ℝ ❘ = [e, p] ( < ( Pnormal e ) , ( planeBase e ) > - < ( Pnormal e ) , p > ) / ( < ( Pnormal e ) , ( Pnormal e ) > ) ❘ # helperT 1 2 prec 1 ❙ helperFunctionForProjection : plane ⟶ point ⟶ ℝ ❘ = [e, p] ( < ( Pnormal e ) , ( planeBase e ) > - < ( Pnormal e ) , p > ) / ( < ( Pnormal e ) , ( Pnormal e ) > ) ❘ # helperT 1 2 prec 1 ❙
orthogonalProjectionPointToPlane : plane ⟶ point ⟶ point ❘ = [e,p] p p+p ( ( helperT e p ) rdotp( Pnormal e ) ) ❘ # orthogProjPointToPlane 1 2 prec 1 ❙ orthogonalProjectionPointToPlane : plane ⟶ point ⟶ point ❘ = [e,p] p p+p ( ( helperT e p ) rdotp( Pnormal e ) ) ❘ # orthogProjPointToPlane 1 2 prec 1 ❙
distancePlanePoint : plane ⟶ point ⟶ ℝ ❘ = [e,p] ( doAbs ( < Pnormal e , p > - < Pnormal e , Pbase e > ) ) / ( | Pnormal e | ) ❘ # distPlP 1 2 prec 1 ❙ distancePlanePoint : plane ⟶ point ⟶ ℝ ❘ = [e,p] ( doAbs ( < Pnormal e , p > - < Pnormal e , Pbase e > ) ) / ( | Pnormal e | + epsi ) ❘ # distPlP 1 2 prec 1 ❙
// functions to calculate the angle between a plane and a line ❙ // functions to calculate the angle between a plane and a line ❙
anglePlaneLineCalc : point ⟶ point ⟶ ℝ ❘ = [v,w] asin ( < v,w > / (|v| ⋅ |w|)) ❘ # plcalc 1 2 prec 1 ❙ anglePlaneLineCalc : point ⟶ point ⟶ ℝ ❘ = [v,w] asin ( < v,w > / ( (|v| ⋅ |w|) + epsi )) ❘ # plcalc 1 2 prec 1 ❙
anglePlaneLine : plane ⟶ line ⟶ ℝ ❘ = [e,l] plcalc ( Pnormal e ) ( directionL l ) ❘ # ∠pl 1 2 prec 1 ❙ anglePlaneLine : plane ⟶ line ⟶ ℝ ❘ = [e,l] plcalc ( Pnormal e ) ( directionL l ) ❘ # ∠pl 1 2 prec 1 ❙
radToDegree : ℝ ⟶ ℝ ❘ = [r] ( r / pi_num ) ⋅ 180.0 ❘ # radToDegree 1 prec 1 ❙ radToDegree : ℝ ⟶ ℝ ❘ = [r] ( r / pi_num ) ⋅ 180.0 ❘ # radToDegree 1 prec 1 ❙
...@@ -100,7 +100,7 @@ theory FrameITBasics = ...@@ -100,7 +100,7 @@ theory FrameITBasics =
lineOnProofFrom: {l } ⊦ ( from l ) on l ❘ # fromOnProofLine 1 ❙ lineOnProofFrom: {l } ⊦ ( from l ) on l ❘ # fromOnProofLine 1 ❙
lineOnProofTo: {l } ⊦ ( to l ) on l ❘ # toOnProofLine 1 ❙ lineOnProofTo: {l } ⊦ ( to l ) on l ❘ # toOnProofLine 1 ❙
normalizeSafe: point ⟶ point ❘ = [v] (1.0 / ( | v | + epsi )) ⋅⋅ v ❘ # normS 1 ❙
❚ ❚
...@@ -228,7 +228,7 @@ theory FrameITCircle = ...@@ -228,7 +228,7 @@ theory FrameITCircle =
angleCircleLine : circle ⟶ line ⟶ ℝ ❘ = [c,l] radToDegree ( plcalc ( Pnormal ( planeCircle c ) ) ( directionL l ) ) ❘ # ∠cl 1 2 prec 1 ❙ angleCircleLine : circle ⟶ line ⟶ ℝ ❘ = [c,l] radToDegree ( plcalc ( Pnormal ( planeCircle c ) ) ( directionL l ) ) ❘ # ∠cl 1 2 prec 1 ❙
orthogonalCircleLine : circle ⟶ line ⟶ bool ❘ # orthogCL 1 2 ❙ orthogonalCircleLine : circle ⟶ line ⟶ bool ❘ # orthogCL 1 2 ❙
pointsToPlaneNormal : point ⟶ point ⟶ point ⟶ plane ❘ = [p1,p2,p3] Ppn p1 ( normalize ( (p2 p-p p1 ) Vcross ( p3 p-p p1) ) ) ❘ # pToPlane 1 2 3 ❙ pointsToPlaneNormal : point ⟶ point ⟶ point ⟶ plane ❘ = [p1,p2,p3] Ppn p1 ( normalizeSafe ( (p2 p-p p1 ) Vcross ( p3 p-p p1) ) ) ❘ # pToPlane 1 2 3 ❙
wrap3EdgePointsToPlaneParametric : point ⟶ point ⟶ point ⟶ plane ❘ = [p1,p2,p3 ] Ppara p1 (p2 p-p p1 ) ( p3 p-p p1) ❘ # pointsToPlanePara 1 2 3 ❙ wrap3EdgePointsToPlaneParametric : point ⟶ point ⟶ point ⟶ plane ❘ = [p1,p2,p3 ] Ppara p1 (p2 p-p p1 ) ( p3 p-p p1) ❘ # pointsToPlanePara 1 2 3 ❙
parallelCircles: circle ⟶ circle ⟶ bool ❘ # paraCirc 1 2 ❙ parallelCircles: circle ⟶ circle ⟶ bool ❘ # paraCirc 1 2 ❙
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment