namespace http://mathhub.info/FrameIT/frameworld/integrationtests ❚

import frameworld http://mathhub.info/FrameIT/frameworld ❚

fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta ❚

theory SampleSituationSpace =
    theory Root =
        // planar triangle in R^2 ❙
        include ☞frameworld:?OppositeLen ❙
        include ☞frameworld:?AngleSum ❙

        A
            : point ❘
            = ⟨0.0, 0.0, 0.0⟩ ❘
            meta frameworld:?MetaAnnotations?label "𝔸"
        ❙

        B
            : point ❘
            = ⟨3.0, 3.0, 0.0⟩ ❘
            meta frameworld:?MetaAnnotations?label "𝔹"
        ❙

        C
            : point ❘
            = ⟨0.0, 3.0, 0.0⟩ ❘
            meta frameworld:?MetaAnnotations?label "ℂ"
        ❙

        distanceBC
            : Σ x:ℝ. ⊦ (d- B C ≐ x) ❘
            = ⟨3.0, sketch "calculated by ComFreek by hand"⟩ ❘
            meta frameworld:?MetaAnnotations?label "𝔹ℂ"
        ❙

        angleABC
            : Σ β:ℝ. ⊦ ( ∠ A,B,C ) ≐ β ❘
            = ⟨45.0, sketch "calculated by ComFreek by hand"⟩ ❘
            meta frameworld:?MetaAnnotations?label "∠𝔸𝔹ℂ"
        ❙

        angleBAC
            : Σ β:ℝ. ⊦ ( ∠ B,A,C ) ≐ β ❘
            = ⟨45.0, sketch "calculated by ComFreek by hand"⟩ ❘
            meta frameworld:?MetaAnnotations?label "∠ℬ𝔸ℂ"
        ❙

        rightAngledC
            : ⊦ ( ∠ B,C,A ) ≐ 90.0 ❘
            = sketch "calculated by ComFreek by hand, hopefully correct" ❘
            meta frameworld:?MetaAnnotations?label "∟ℂ"
        ❙
    ❚
❚

theory MyScroll =
  theory Problem = a: type ❙❚
  theory Solution =
    include ?MyScroll/Problem ❙
    c: type ❘ = a❙
  ❚
❚

theory SituationSpace =
  theory RootSituationTheory =
    include ?MyScroll ❙
    b: type ❙
    p : point ❘ = ⟨0.0, 0.0, 0.0⟩ ❙

    view v : ?MyScroll/Problem -> ?SituationSpace/RootSituationTheory =
      a = b ❙
    ❚
  ❚

  theory PushedOutSituationTheory =
    include ?SituationSpace/RootSituationTheory ❙
    c: type ❙
    q = p ❙

    view w : ?MyScroll/Problem -> ?SituationSpace/PushedOutSituationTheory =
      a = c ❙
    ❚
  ❚
❚