Skip to content

Commit

Permalink
blog: hott
Browse files Browse the repository at this point in the history
  • Loading branch information
ice1000 committed Mar 13, 2024
1 parent cece619 commit 3447269
Show file tree
Hide file tree
Showing 5 changed files with 581 additions and 699 deletions.
2 changes: 1 addition & 1 deletion aya/guide/anqur-story.aya.md
Original file line number Diff line number Diff line change
Expand Up @@ -219,7 +219,7 @@ equality between `a` and `b` nicely.
We may then use the following type signature:

```aya
def ++-assoc (xs : Vec n A) (ys : Vec m A) (zs : Vec o A)
def ++-assoc-type (xs : Vec n A) (ys : Vec m A) (zs : Vec o A)
=> Path (fn i => Vec (+-assoc i) A) ((xs ++ ys) ++ zs) (xs ++ (ys ++ zs))
```

Expand Down
8 changes: 4 additions & 4 deletions package.json
Original file line number Diff line number Diff line change
Expand Up @@ -21,14 +21,14 @@
},
"homepage": "https://github.com/aya-prover/aya-prover-docs#readme",
"dependencies": {
"@vscode/markdown-it-katex": "^1.0.0",
"@vscode/markdown-it-katex": "^1.0.3",
"markdown-it-footnote": "^4.0.0"
},
"devDependencies": {
"@types/markdown-it-footnote": "^3.0.3",
"@types/markdown-it-footnote": "^3.0.4",
"@vitejs/plugin-vue-jsx": "^3.1.0",
"vitepress": "1.0.0-rc.32",
"vue": "^3.3.13"
"vitepress": "1.0.0-rc.45",
"vue": "^3.4.21"
},
"pnpm": {
"overrides": {
Expand Down
Loading

0 comments on commit 3447269

Please sign in to comment.