|
|
13636a0d29
|
Write more about Agda+Hugo
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-30 00:13:48 -07:00 |
|
|
|
6a168f2fe1
|
Start on a draft about Agda and Hugo
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-25 23:28:18 -07:00 |
|
|
|
04f12b545d
|
Minor edits to 'lattices 2'
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-25 20:45:19 -07:00 |
|
|
|
711b01175d
|
Put the number back to what it was
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-24 23:12:27 -07:00 |
|
|
|
272c2666c5
|
Inconsequential tweak to test Agda caching in build system
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-24 13:44:34 -07:00 |
|
|
|
c0f4fe017f
|
Replace absolute links with relrefs
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-22 23:05:11 -07:00 |
|
|
|
11d726a6ad
|
Fix absolute link in favor of relref
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-22 23:01:26 -07:00 |
|
|
|
ee8b1f5dc0
|
Write a bit more, enable support for paragraph links
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-21 19:04:08 -07:00 |
|
|
|
4938cdaecd
|
Work some more on lattices 2
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-20 22:46:18 -07:00 |
|
|
|
84f28ae5ce
|
Add tags to Agda articles
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-20 21:46:14 -07:00 |
|
|
|
58e7a1f2dc
|
Start on a draft of 'combining lattices'
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-20 21:39:03 -07:00 |
|
|
|
78bba7a0e9
|
Update the blog for series navigation
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-20 00:37:16 -07:00 |
|
|
|
9d31764073
|
Tie up Lattices (1), and plan to write Lattices (2)
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-19 22:29:24 -07:00 |
|
|
|
60d3b3025a
|
Flesh out the Lattices post some more
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-14 21:43:12 -07:00 |
|
|
|
1df315612a
|
Update "typesafe interpreter" article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 19:08:17 -07:00 |
|
|
|
15beddf96b
|
Update btree article with new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 19:07:44 -07:00 |
|
|
|
20d8b18a9b
|
Update 'stack language recursion' article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 19:07:01 -07:00 |
|
|
|
53ff0c39e4
|
Update "search as polynomial" article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 19:06:33 -07:00 |
|
|
|
357a3bef09
|
Update the modulo patterns article to use new delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 19:04:08 -07:00 |
|
|
|
81eef51e88
|
Update 'math rendering is wrong' to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 19:02:14 -07:00 |
|
|
|
10dfb2fe49
|
Update "church encoding" article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 19:01:42 -07:00 |
|
|
|
ef76149112
|
Update 'newtype' article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 19:01:08 -07:00 |
|
|
|
a6a330a78e
|
Update Haskell LSP article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 19:00:23 -07:00 |
|
|
|
7f4d0df366
|
Update "catemorphisms" article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 18:59:54 -07:00 |
|
|
|
3eddac0a89
|
Update "proving my compiler incorrect" to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 18:58:50 -07:00 |
|
|
|
6e7ac1c1ca
|
Update "I don't like Coq's docs" article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 18:58:15 -07:00 |
|
|
|
68d9cf1274
|
Update 'evaluator for Dawn in Coq' article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 18:57:15 -07:00 |
|
|
|
5eb0d1548c
|
Update dawn-in-coq to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 18:55:59 -07:00 |
|
|
|
e543904995
|
Update boolean values article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 18:54:11 -07:00 |
|
|
|
ffda1d3235
|
Moved the bergamot article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 18:52:21 -07:00 |
|
|
|
b705aa217c
|
Update "expr pattern in agda" to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 18:50:56 -07:00 |
|
|
|
6f20b17948
|
Update "compiler: polymorphic data types" to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 18:50:05 -07:00 |
|
|
|
2fde7e5cf8
|
Update "compiler: polymorphism" to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 18:48:34 -07:00 |
|
|
|
bee06b6731
|
Update "compiler: compilation" to use new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 18:43:14 -07:00 |
|
|
|
d3fa7336a2
|
Update "compiler: execution" to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 18:38:05 -07:00 |
|
|
|
96545a899f
|
Update "compiler: typechecking" to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 18:33:30 -07:00 |
|
|
|
6ef5ae2394
|
Update "types: variables" to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 18:31:52 -07:00 |
|
|
|
05a31dd4d4
|
Update 'compiler: parsing' article to new string literals
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 18:30:27 -07:00 |
|
|
|
d9d5c8bf14
|
Switch 'types: basics' to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 18:28:36 -07:00 |
|
|
|
291a1f0178
|
Update SPA article on Lattices with new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 18:22:21 -07:00 |
|
|
|
2547b53aa2
|
Switch "Homework for an assignment" post 2 to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-13 18:20:54 -07:00 |
|
|
|
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 |
|
|
|
b492c2d0fb
|
Add more drafts
|
2023-01-29 21:08:31 -08:00 |
|
|
|
1a6f5e061b
|
Add a very rough draft of the idris catemorphisms article I found lying around
|
2023-01-29 21:00:22 -08:00 |
|
|
|
e7cb818f05
|
Merge branch 'master' of https://dev.danilafe.com/Web-Projects/blog-static
|
2022-12-30 13:35:00 -08:00 |
|
|
|
8d980b0287
|
Fix typo in equation for search-as-polynomial article
|
2022-12-30 13:27:47 -08:00 |
|
Danila Fedorin
|
baa199c50f
|
Prevent overlap in polynomial search article
|
2022-12-09 15:42:48 -08:00 |
|
Danila Fedorin
|
29a0d2e357
|
Remove linear multistep article (transferred to Chapel blog)
|
2022-12-09 15:42:29 -08:00 |
|
|
|
ca3345cb33
|
Edit and improve the polynomial search post
|
2022-10-26 21:26:27 -07:00 |
|
|
|
0ade4b2efb
|
Add a tiny section about the tropical semiring to polynomial post
|
2022-10-25 22:46:05 -07:00 |
|
|
|
2439a02dbb
|
Add draft of first part of polynomials article
|
2022-10-23 17:27:30 -07:00 |
|
