This commit is contained in:
Nathan McCarty 2025-03-16 19:59:09 -04:00
parent 6f7be736e9
commit 99b7ca322e
4 changed files with 43 additions and 27 deletions

View file

@ -1,10 +1,10 @@
{
"edited-at": [
],
"hidden": true,
"hidden": false,
"idris": true,
"ipkg": "/home/nathan/Projects/Blog/projects/Idris/Idris.ipkg",
"posted-at": "2025-03-15T18:07:00.649227-04:00",
"posted-at": "2025-03-16T19:59:18.071274-04:00",
"slugs": [
],
"source": "/home/nathan/Projects/Blog/projects/Idris/src/DependentNuggets/FreshLists.md",
@ -13,4 +13,4 @@
"tags": [
"idris"
]
}
}

View file

@ -4,4 +4,4 @@
5
],
"title": "Less Macros, More Types"
}
}

View file

@ -1,5 +1,5 @@
{
"desc": "Introductions to the building blocks of dependently typed programs.",
"desc": "Introductions to the building blocks of dependently typed programs.</p><p>The posts in this series are 'living posts', they will be referenced as library modules by future posts, and will be updated as needs change.",
"post-ids": [
7
],