From 735a4348c0af7020f1fd60c257e4f8174090ba26 Mon Sep 17 00:00:00 2001 From: Marius Kern <mariusskern@gmail.com> Date: Fri, 8 Mar 2024 13:05:30 +0100 Subject: [PATCH] new fact --- source/MetaTheories.mmt | 1 + 1 file changed, 1 insertion(+) diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt index 1e7a1d1..644d6a7 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 ♠-- GitLab