From b64d2837ad7e6cac851ad7958d35f373ea9de764 Mon Sep 17 00:00:00 2001
From: Marcel Dreier <marcelqq7@gmail.com>
Date: Thu, 16 Jun 2022 17:43:21 +0200
Subject: [PATCH] a bunch of new scrolls and facts
---
.../frameworld/$Frameworld$Meta.omdoc.xz | Bin 620 -> 620 bytes
narration/MetaTheories.omdoc | 2 +-
source/MetaTheories.mmt | 8 ++++----
3 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz
index f58dd1ac5451c19fd0e55f5fdb1830515be3f6b9..96aad98e857b18138e7a2af7caba74d23cf24813 100644
GIT binary patch
delta 250
zcmV<W00sZ-1ndN`djWp|`-<(hyawYc1dWP@gR1M6S=bBO-Y(+Xl1~~k=&<4)w+2|S
zMe_Yd_`Lh%P#?)w<X^W+xxDp-_QzpZ(yv(F*FH#ziE%a9P06@v&~Echd>bF(xmfM)
z)sI7t-G(ujataCzQNioS8z@A@qGve?wi#8WZ7Fc#1hSZvUvhGUI76B|I&eIA)13sT
zlQ}aQNrbx<hxeD27_=401c}yf9ZU9p;*@AE@J%NFD(;=0hWvZEiFfHyzm@KIT<T3`
z5OfI$xJ3RN5U>K;Ug^@f0LJ8nw!v<%CIA7*1eF#50FWSCS+T@t`vL#}000D8T9n0l
AQvd(}
delta 250
zcmV<W00sZ-1ndN`djWp{s`<#}y*SQmGye?fX>nM^638-Qx;87~x2Z~kUht`D{Kr7F
zCWxT6?$B(Jd~(Jjt<t$Uk>>(3-QQnKNT$-mV^|&0@!@7x>gyb@xg#ndpi)_=ejl&a
z>35(Yi&hvYTNhpY3n#ao8Hl`FIUI>kKIbRqtZdN-3`aB@lR<L)QEtBpZbWrZf1LXI
zBjg%C@WfY4l0clb)Gm9eZ|kRg#;3(0tE;Mvh8C*_9?ogKxBoqz%~-m{*5YpqUWPx6
zYS1$DC#zY`d!XtE5laY+0MeOY8Hp^sF#rL`1eF#50FWSCS+T@t`vL#}000D8TH{)G
ACIA2c
diff --git a/narration/MetaTheories.omdoc b/narration/MetaTheories.omdoc
index 34be72d..ff67f80 100644
--- a/narration/MetaTheories.omdoc
+++ b/narration/MetaTheories.omdoc
@@ -1,2 +1,2 @@
<?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>
\ No newline at end of file
+<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
diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt
index 39ae590..4d2c522 100644
--- a/source/MetaTheories.mmt
+++ b/source/MetaTheories.mmt
@@ -88,10 +88,10 @@ theory FrameITBasics =
// 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 â™
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 â™
- 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 â™
radToDegree : ℠⟶ ℠☠= [r] ( r / pi_num ) â‹… 180.0 ☠# radToDegree 1 prec 1 â™
@@ -100,7 +100,7 @@ theory FrameITBasics =
lineOnProofFrom: {l } ⊦ ( from l ) on l ☠# fromOnProofLine 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 =
angleCircleLine : circle ⟶ line ⟶ ℠☠= [c,l] radToDegree ( plcalc ( Pnormal ( planeCircle c ) ) ( directionL l ) ) ☠# ∠cl 1 2 prec 1 â™
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 â™
parallelCircles: circle ⟶ circle ⟶ bool ☠# paraCirc 1 2 â™
--
GitLab