|
409f8b7186
|
Switch tokenizing article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 18:20:04 -07:00 |
|
|
189422bf1e
|
Convert AoC Coq article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 18:16:20 -07:00 |
|
|
befcd3cf98
|
Add a sidenote about land and lor.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 15:41:50 -07:00 |
|
|
6179c86919
|
Show the basic Nat lattice.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-12 18:52:26 -07:00 |
|
|
a20fe07a56
|
Move original 'monotone function' text into new post and heavily rework it
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-12 18:28:44 -07:00 |
|
|
2b5dcf12d7
|
Rename the SPA intro to have a specific name
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-12 13:50:29 -07:00 |
|
|
5873c1ca96
|
Write a high-level introduction for the SPA series
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-12 13:49:21 -07:00 |
|
|
c6e2ecb996
|
Add first section of Agda program analysis article
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-14 22:25:17 -07:00 |
|
|
2130b00752
|
Narrow some of the tags
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-13 15:59:46 -07:00 |
|
|
474c3a8348
|
Switch bracket types in Agda expression pattern post
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-13 15:05:37 -07:00 |
|
|
29a18b8b37
|
Add description to expr_pattern
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-11 23:26:07 -07:00 |
|
|
7d2842fd64
|
Add article about the 'deeply embedded expression' pattern
|
2024-03-11 23:15:56 -07:00 |
|
|
266bf9b4cf
|
Add an exercise about conversions to types: basics
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-12-29 12:47:58 -08:00 |
|
|
a6f3bccf64
|
Use markdown for exercises, since it works fine out of the box.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-12-28 16:05:15 -08:00 |
|
|
d7d99205a1
|
Properly escape < in HTML content.
|
2023-12-28 00:36:58 -08:00 |
|
|
9f437d5b9f
|
Add a couple of exercises to types: basics.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-12-28 00:13:13 -08:00 |
|
|
72fb69d87b
|
Make minor changes to types: basics.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-12-27 23:31:45 -08:00 |
|
|
ed4fcf5e9d
|
Start explaining exercises in types intro.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-12-27 23:31:28 -08:00 |
|
|
8f2b2addc2
|
Rename the widget IDs to not include numbers.
|
2023-12-27 13:16:20 -08:00 |
|
|
e4743bbdef
|
Make some edits to 'types' part 1.
|
2023-12-26 14:02:48 -08:00 |
|
|
645f2c5c9c
|
Update inference rules to match new Bergamot's single-literal output
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-12-26 13:21:37 -08:00 |
|
|
16086e79b0
|
Proofread and publish bergamot post
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-12-22 22:15:17 -08:00 |
|
|
0c895a2662
|
Add an initial draft of the Bergamot post.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-12-22 22:00:06 -08:00 |
|
|
dc9dbe8a0f
|
Update for bergamot requiring an 'input program' too
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-12-22 16:04:33 -08:00 |
|
|
a83268a6e3
|
Update use of the bergamot widget
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-12-21 17:26:19 -08:00 |
|
|
c25f9ad9ae
|
Add the work-in-progress Bergamot widget to the basics page.
|
2023-11-29 23:21:15 -08:00 |
|
|
3bceab0606
|
Fix dates
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-10-14 15:58:20 -07:00 |
|
|
c189da3671
|
Finalize the X Macro article
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-10-14 15:38:54 -07:00 |
|
|
dd232cedb5
|
Fixup links and add description to X Macros article.
|
2023-10-09 20:33:21 -07:00 |
|
|
88c5daa561
|
Add the 'chapel' tag to the alloy article
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-10-09 20:24:19 -07:00 |
|
|
4f281ef108
|
Add a draft article about X Macros
|
2023-10-09 20:23:57 -07:00 |
|
|
12aca7ca58
|
Update the Alloy blogpost to point to the GitHub files.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-10-09 14:41:03 -07:00 |
|
|
6b24d67409
|
Minor wording updates to the Agda post.
|
2023-08-31 22:30:36 -07:00 |
|
|
48c3105f42
|
Finish and publish the IsSomething article
|
2023-08-31 22:16:26 -07:00 |
|
|
032453c4d0
|
Add a first draft of the IsSomething article
|
2023-08-28 23:04:39 -07:00 |
|
|
1f5e38190d
|
Fix DeMorgan's link
|
2023-06-04 22:03:38 -07:00 |
|
|
250884c7bc
|
Edit and publish Alloy article
|
2023-06-04 21:56:45 -07:00 |
|
|
5910ce7980
|
Say screw it and publish polynomial article
|
2023-05-22 21:42:32 -07:00 |
|
|
00bec06012
|
Make some edits to the polynomial draft
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-05-22 20:44:50 -07:00 |
|
|
54dccdbc7d
|
Fix accidentally lowercased shortcode
|
2023-05-14 21:23:22 -07:00 |
|
|
2bd776ec55
|
Add a description and disclaimer to the Alloy draft.
|
2023-05-14 21:18:23 -07:00 |
|
|
23cf7c9e8b
|
Finish initial draft of the Alloy article.
|
2023-05-14 21:13:23 -07:00 |
|
|
384f5de765
|
Make some more progress on the Alloy article.
|
2023-05-14 16:00:55 -07:00 |
|
|
9ae4798d80
|
Hide Alloy article even from draft side
|
2023-05-04 21:03:37 -07:00 |
|
|
d8ab3f2226
|
Continue working on the Alloy blog post
|
2023-05-04 21:01:31 -07:00 |
|
|
9ddd2dd3bc
|
Add initial draft of alloy article
|
2023-05-04 01:03:58 -07:00 |
|
|
f579641866
|
Add support for discussion rooms and add one to polynomial article
|
2023-04-15 15:09:06 -07:00 |
|
|
2964b6c6fa
|
Tweak some wording in the variables article
|
2023-03-11 12:15:21 -08:00 |
|
|
a833cd84f3
|
Add series tags to relevant articles
|
2023-01-31 18:53:30 -08:00 |
|
|
5bd8c11a86
|
Tag the more rough articles as expired to make sure they don't show up
|
2023-01-29 21:23:59 -08:00 |
|