diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt index 1e7a1d1f4a967b9caa8fbd2fdc9eaeb1c198dcd6..644d6a71f290c3665401148063f12eb3fa48f75b 100644 --- a/source/MetaTheories.mmt +++ b/source/MetaTheories.mmt @@ -120,6 +120,7 @@ theory FrameITRectangles = // TODO maybe delete â™ rectangle_type : type ☠# rect â™ + testPoint_type : type ☠# testPoint â™ mkRectangle : { A: point , B : point, C : point , D : point } ( ⊦ isRect A B C D ) ⟶ rect ☠# mkRect 1 2 3 4 5 â™ cornerA : rect ⟶ point ☠# rectA 1 â™