markdown config
This commit is contained in:
parent
9d8395b7b4
commit
95a30f831a
20
package-lock.json
generated
20
package-lock.json
generated
|
@ -11,11 +11,11 @@
|
|||
"vue": "^3.4.29"
|
||||
},
|
||||
"devDependencies": {
|
||||
"@traptitech/markdown-it-katex": "^3.6.0",
|
||||
"@tsconfig/node20": "^20.1.4",
|
||||
"@types/node": "^20.14.5",
|
||||
"@unhead/vue": "^1.9.16",
|
||||
"@vitejs/plugin-vue": "^5.0.5",
|
||||
"@vscode/markdown-it-katex": "^1.1.0",
|
||||
"@vue/language-server": "^2.0.26",
|
||||
"@vue/tsconfig": "^0.5.1",
|
||||
"@vue/typescript-plugin": "^2.0.26",
|
||||
|
@ -821,15 +821,6 @@
|
|||
"win32"
|
||||
]
|
||||
},
|
||||
"node_modules/@traptitech/markdown-it-katex": {
|
||||
"version": "3.6.0",
|
||||
"resolved": "https://registry.npmjs.org/@traptitech/markdown-it-katex/-/markdown-it-katex-3.6.0.tgz",
|
||||
"integrity": "sha512-CnJzTWxsgLGXFdSrWRaGz7GZ1kUUi8g3E9HzJmeveX1YwVJavrKYqysktfHZQsujdnRqV5O7g8FPKEA/aeTkOQ==",
|
||||
"dev": true,
|
||||
"dependencies": {
|
||||
"katex": "^0.16.0"
|
||||
}
|
||||
},
|
||||
"node_modules/@tsconfig/node20": {
|
||||
"version": "20.1.4",
|
||||
"resolved": "https://registry.npmjs.org/@tsconfig/node20/-/node20-20.1.4.tgz",
|
||||
|
@ -1048,6 +1039,15 @@
|
|||
"integrity": "sha512-KYSIHVmslkaCDyw013pphY+d7x1qV8IZupYfeIfzNA+nsaWHbn5uPuQRvdRFsa9zFzGeudPuoGoZ1Op4jrJXIQ==",
|
||||
"dev": true
|
||||
},
|
||||
"node_modules/@vscode/markdown-it-katex": {
|
||||
"version": "1.1.0",
|
||||
"resolved": "https://registry.npmjs.org/@vscode/markdown-it-katex/-/markdown-it-katex-1.1.0.tgz",
|
||||
"integrity": "sha512-9cF2eJpsJOEs2V1cCAoJW/boKz9GQQLvZhNvI030K90z6ZE9lRGc9hDVvKut8zdFO2ObjwylPXXXVYvTdP2O2Q==",
|
||||
"dev": true,
|
||||
"dependencies": {
|
||||
"katex": "^0.16.4"
|
||||
}
|
||||
},
|
||||
"node_modules/@vue/compiler-core": {
|
||||
"version": "3.4.31",
|
||||
"resolved": "https://registry.npmjs.org/@vue/compiler-core/-/compiler-core-3.4.31.tgz",
|
||||
|
|
|
@ -14,11 +14,11 @@
|
|||
"vue": "^3.4.29"
|
||||
},
|
||||
"devDependencies": {
|
||||
"@traptitech/markdown-it-katex": "^3.6.0",
|
||||
"@tsconfig/node20": "^20.1.4",
|
||||
"@types/node": "^20.14.5",
|
||||
"@unhead/vue": "^1.9.16",
|
||||
"@vitejs/plugin-vue": "^5.0.5",
|
||||
"@vscode/markdown-it-katex": "^1.1.0",
|
||||
"@vue/language-server": "^2.0.26",
|
||||
"@vue/tsconfig": "^0.5.1",
|
||||
"@vue/typescript-plugin": "^2.0.26",
|
||||
|
|
|
@ -74,18 +74,18 @@ proof2 (a, f) = f a
|
|||
|
||||
I strongly encourage you to play around with this on your own, coming up with some propositions and proving them by hand and using Haskell. The table below gives an overview of the translation from logic to Haskell.
|
||||
|
||||
<table>
|
||||
<tr> <th>Logic</th> <th>Haskell</th> </tr>
|
||||
<tr> <td>Proposition</td> <td>Type</td> </tr>
|
||||
<tr> <td>Proof</td> <td>Term (element of type)</td> </tr>
|
||||
<tr> <td>Atom</td> <td>Type variable</td> </tr>
|
||||
<tr> <td>$\top$</td> <td>Type with a known term</td> </tr>
|
||||
<tr> <td>$\bot$</td> <td>Type with no terms</td> </tr>
|
||||
<tr> <td>$P \land Q$</td> <td><code>(P, Q)</code></td> </tr>
|
||||
<tr> <td>$P \lor Q$</td> <td><code>Either P Q</code></td> </tr>
|
||||
<tr> <td>$P \to Q$</td> <td><code>P -> Q</code></td> </tr>
|
||||
<tr> <td>$\lnot P$</td> <td><code>P -> EmptyType</code></td> </tr>
|
||||
</table>
|
||||
|
||||
| Logic | Haskell |
|
||||
|-------------|------------------------|
|
||||
| Proposition | Type |
|
||||
| Proof | Term (element of type) |
|
||||
| Atom | Type variable |
|
||||
| $\top$ | Type with a known term |
|
||||
| $\bot$ | Type with no terms |
|
||||
| $P \land Q$ | `(P, Q)` |
|
||||
| $P \lor Q$ | `Either P Q` |
|
||||
| $P \to Q$ | `P -> Q` |
|
||||
| $\lnot P$ | `P -> EmptyType` |
|
||||
|
||||
|
||||
## The paradoxes of Haskell
|
||||
|
|
|
@ -3,7 +3,7 @@ import { fileURLToPath, URL } from 'node:url'
|
|||
import Vue from '@vitejs/plugin-vue'
|
||||
import Pages from 'vite-plugin-pages'
|
||||
import Markdown from 'unplugin-vue-markdown/vite'
|
||||
import mk from '@traptitech/markdown-it-katex'
|
||||
import mk from '@vscode/markdown-it-katex'
|
||||
|
||||
export default {
|
||||
plugins: [
|
||||
|
@ -14,7 +14,8 @@ export default {
|
|||
Markdown({
|
||||
headEnabled: true,
|
||||
markdownItSetup(md) {
|
||||
md.use(mk)
|
||||
// @ts-ignore
|
||||
md.use(mk.default)
|
||||
}
|
||||
})
|
||||
],
|
||||
|
|
Loading…
Reference in New Issue
Block a user