Skip to content

Commit

Permalink
Update textbook
Browse files Browse the repository at this point in the history
  • Loading branch information
clarksmr committed Jan 6, 2025
1 parent d58ce94 commit cec9347
Show file tree
Hide file tree
Showing 51 changed files with 1,307 additions and 1,307 deletions.
22 changes: 11 additions & 11 deletions _sources/chapters/adv/curry-howard.ipynb
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
"cells": [
{
"cell_type": "markdown",
"id": "bad1fbe2",
"id": "0cbf192e",
"metadata": {},
"source": [
"# The Curry-Howard Correspondence\n",
Expand Down Expand Up @@ -60,7 +60,7 @@
{
"cell_type": "code",
"execution_count": null,
"id": "90cb61be",
"id": "00d0d777",
"metadata": {},
"outputs": [],
"source": [
Expand All @@ -69,7 +69,7 @@
},
{
"cell_type": "markdown",
"id": "5b0b401e",
"id": "d5e470ba",
"metadata": {},
"source": [
"We could have called that type anything we wanted instead of `empty`; the\n",
Expand All @@ -88,7 +88,7 @@
{
"cell_type": "code",
"execution_count": null,
"id": "8e9a708e",
"id": "bfbc18da",
"metadata": {},
"outputs": [],
"source": [
Expand All @@ -99,7 +99,7 @@
},
{
"cell_type": "markdown",
"id": "59f3d994",
"id": "9bab6d1c",
"metadata": {},
"source": [
"We could think of `pair` as a function that takes in evidence for `'a` and\n",
Expand Down Expand Up @@ -248,7 +248,7 @@
{
"cell_type": "code",
"execution_count": null,
"id": "d014c190",
"id": "04b351c0",
"metadata": {},
"outputs": [],
"source": [
Expand All @@ -257,7 +257,7 @@
},
{
"cell_type": "markdown",
"id": "a6e8ce31",
"id": "8814f479",
"metadata": {},
"source": [
"A value `v` of that type is either `Left a`, where `a : 'a`; or `Right b`, where\n",
Expand Down Expand Up @@ -291,7 +291,7 @@
{
"cell_type": "code",
"execution_count": null,
"id": "3eb6075e",
"id": "1fb2f644",
"metadata": {},
"outputs": [],
"source": [
Expand All @@ -300,7 +300,7 @@
},
{
"cell_type": "markdown",
"id": "1644b8cf",
"id": "0afc1ffa",
"metadata": {},
"source": [
"Now if you enter this code in utop you will get no response:\n",
Expand All @@ -319,7 +319,7 @@
{
"cell_type": "code",
"execution_count": null,
"id": "7f7cabd1",
"id": "4b79835c",
"metadata": {
"tags": [
"raises-exception"
Expand All @@ -332,7 +332,7 @@
},
{
"cell_type": "markdown",
"id": "7db5558d",
"id": "fb7da075",
"metadata": {},
"source": [
"Again, the expression type checks, but it never produces an actual value of type\n",
Expand Down
2 changes: 1 addition & 1 deletion _sources/chapters/basics/debugging.ipynb
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
"cells": [
{
"cell_type": "markdown",
"id": "d566ce0d",
"id": "0422d924",
"metadata": {},
"source": [
"# Debugging\n",
Expand Down
Loading

0 comments on commit cec9347

Please sign in to comment.