https://starling-lang.org/editor/index.html

1<!doctype html>
2<html lang="en">
3    <head>
4        <meta charset="UTF-8" />
5        <meta name="viewport" content="width=device-width, initial-scale=1.0" />
6        <title>⭐ Starling IDE</title>
7        <style>
8            html {
9                background-color: rgba(255, 240, 245, 0.125);
10            }
11            #top-nav {
12                display: flex;
13                flex-direction: row;
14                gap: 35px;
15                margin-bottom: 20px;
16            }
17
18            button {
19                all: unset;
20                cursor: pointer;
21            }
22
23            a:link,
24            button {
25                background-color: lavenderblush;
26                color: maroon;
27                border-radius: 5px;
28                font-size: 21px;
29                font-family: sans-serif;
30                border: darkslategray 1px solid;
31                padding: 7.5px;
32            }
33
34            a:link:hover,
35            button:hover {
36                background-color: maroon;
37                color: white;
38            }
39
40            pre {
41                background-color: rgba(255, 240, 245, 0.125);
42                color: darkslategray;
43                border-radius: 5px;
44                border: darkslategray 1px solid;
45                font-size: 18px;
46                padding: 20px;
47            }
48        </style>
49    </head>
50    <body>
51        <nav id="top-nav">
52            <div class="nav-links">
53                <a href="../docs/index.html" class="nav-link">Documentation</a>
54                <a href="index.html" class="nav-link">New</a>
55                <button id="verify" class="nav-link" type="button">
56                    Verify
57                </button>
58            </div>
59        </nav>
60        <pre contenteditable>
61import "set.mm";
62replace { equals : = , provable : |- };
63
642plus2 = ( 2 + 2 ) equals 4: provable;
65
66proof of 2plus2 {
67    c2;
68    c2;
69    caddc;
70    co;
71    c2;
72    c1;
73    c1;
74    caddc;
75    co;
76    caddc;
77    co;
78    c4;
79    c2;
80    c1;
81    c1;
82    caddc;
83    co;
84    c2;
85    caddc;
86    df-2;
87    oveq2i;
88    c4;
89    c3;
90    c1;
91    caddc;
92    co;
93    c2;
94    c1;
95    caddc;
96    co;
97    c1;
98    caddc;
99    co;
100    c2;
101    c1;
102    c1;
103    caddc;
104    co;
105    caddc;
106    co;
107    df-4;
108    c3;
109    c2;
110    c1;
111    caddc;
112    co;
113    c1;
114    caddc;
115    df-3;
116    oveq1i;
117    c2;
118    c1;
119    c1;
120    2cn;
121    ax-1cn;
122    ax-1cn;
123    addassi;
124    3eqtri;
125    eqtr4i;
126}
127</pre
128        >
129        

129<script src="src/work.js"></script>

129
130    </body>
131</html>