GitHub Actions Automated Deploy

aya-prover · Jun 3, 2024 · a14dbe4 · a14dbe4
commit a14dbe4
Show file tree

Hide file tree

Showing 88 changed files with 1,539 additions and 0 deletions.
diff --git a/404.html b/404.html
@@ -0,0 +1,24 @@
+<!DOCTYPE html>
+<html lang="en-US" dir="ltr">
+  <head>
+    <meta charset="utf-8">
+    <meta name="viewport" content="width=device-width,initial-scale=1">
+    <title>404 | Aya Prover</title>
+    <meta name="description" content="Not Found">
+    <meta name="generator" content="VitePress v1.2.2">
+    <link rel="preload stylesheet" href="/assets/style.CdGn_S1u.css" as="style">
+
+    <script type="module" src="/assets/app.CN8oZRug.js"></script>
+    <link rel="preload" href="/assets/inter-roman-latin.Di8DUHzh.woff2" as="font" type="font/woff2" crossorigin="">
+    <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/[email protected]/dist/katex.min.css" crossorigin="anonymous">
+    <link rel="stylesheet" href="https://fonts.googleapis.com/css2?family=Merriweather:ital,wght@0,300;0,700;0,900;1,300;1,700&amp;display=swap">
+    <link rel="icon" href="/logo.svg">
+    <script id="check-dark-mode">(()=>{const e=localStorage.getItem("vitepress-theme-appearance")||"auto",a=window.matchMedia("(prefers-color-scheme: dark)").matches;(!e||e==="auto"?a:e==="dark")&&document.documentElement.classList.add("dark")})();</script>
+    <script id="check-mac-os">document.documentElement.classList.toggle("mac",/Mac|iPhone|iPod|iPad/i.test(navigator.platform));</script>
+  </head>
+  <body>
+    <div id="app"></div>
+    <script>window.__VP_HASH_MAP__=JSON.parse("{\"blog_bye-hott.md\":\"oHSpBv52\",\"index.md\":\"RUkObOdP\",\"blog_binops.md\":\"Dr9-j7RW\",\"pubs_index.md\":\"DOswxG58\",\"blog_lang-exts.md\":\"BR4-INkK\",\"blog_ind-prop.md\":\"BEJJ837H\",\"blog_path-elab.md\":\"BQ0zsQ1c\",\"blog_class-defeq.md\":\"BRWO4S-o\",\"blog_extended-pruning.md\":\"CSDGvtp1\",\"guide_vscode-tutorial.md\":\"Clsg6U9F\",\"guide_haskeller-tutorial.md\":\"DebqvM_X\",\"blog_index-unification.md\":\"BBAtZbbv\",\"blog_redirect.md\":\"oU1IrIO-\",\"guide_project-tutorial.md\":\"hPosCHlX\",\"guide_install.md\":\"DYXt-NYj\",\"blog_index.md\":\"Bzluj1q-\",\"blog_pathcon-elab.md\":\"DP0mT13b\",\"guide_fake-literate.md\":\"DraB6mjK\",\"guide_readings.md\":\"D_JBMCqV\",\"guide_prover-tutorial.md\":\"D4psWkOj\",\"guide_index.md\":\"BmZ0zcov\"}");window.__VP_SITE_DATA__=JSON.parse("{\"lang\":\"en-US\",\"dir\":\"ltr\",\"title\":\"Aya Prover\",\"description\":\"A VitePress site\",\"base\":\"/\",\"head\":[],\"router\":{\"prefetchLinks\":true},\"appearance\":true,\"themeConfig\":{\"logo\":\"/logo.svg\",\"socialLinks\":[{\"icon\":\"github\",\"link\":\"https://github.com/aya-prover\"}],\"editLink\":{\"pattern\":\"https://github.com/aya-prover/aya-prover-docs/tree/main/src/:path\",\"text\":\"Suggest changes to this page\"},\"nav\":[{\"text\":\"Guide\",\"link\":\"/guide/\"},{\"text\":\"Publications\",\"link\":\"/pubs/\"},{\"text\":\"Blog\",\"link\":\"/blog/\"}],\"search\":{\"provider\":\"local\"},\"sidebar\":[{\"text\":\"Blog\",\"items\":[{\"text\":\"Extended Pruning\",\"link\":\"/blog/extended-pruning\"},{\"text\":\"Farewell, Univalence\",\"link\":\"/blog/bye-hott\"},{\"text\":\"Inductive Props\",\"link\":\"/blog/ind-prop\"},{\"text\":\"Def. projection in classes\",\"link\":\"/blog/class-defeq\"},{\"text\":\"Path constructor elaboration\",\"link\":\"/blog/pathcon-elab\"},{\"text\":\"Path type elaboration\",\"link\":\"/blog/path-elab\"},{\"text\":\"Binary operators\",\"link\":\"/blog/binops\"},{\"text\":\"Index unification\",\"link\":\"/blog/index-unification\"},{\"text\":\"Language extensions?\",\"link\":\"/blog/lang-exts\"}]},{\"text\":\"Guide\",\"items\":[{\"text\":\"Get Started\",\"link\":\"/guide/\"},{\"text\":\"Install\",\"link\":\"/guide/install\"},{\"text\":\"Functional Programming\",\"link\":\"/guide/haskeller-tutorial\"},{\"text\":\"Theorem Proving\",\"link\":\"/guide/prover-tutorial\"},{\"text\":\"Aya packages\",\"link\":\"/guide/project-tutorial\"},{\"text\":\"VSCode\",\"link\":\"/guide/vscode-tutorial\"},{\"text\":\"Related papers\",\"link\":\"/guide/readings\"},{\"text\":\"Fake literate mode\",\"link\":\"/guide/fake-literate\"}]}]},\"locales\":{},\"scrollOffset\":134,\"cleanUrls\":false}");</script>
+
+  </body>
+</html>
diff --git a/CNAME b/CNAME
@@ -0,0 +1 @@
+www.aya-prover.org
diff --git a/assets/app.CN8oZRug.js b/assets/app.CN8oZRug.js
diff --git a/assets/blog_binops.md.Dr9-j7RW.js b/assets/blog_binops.md.Dr9-j7RW.js
diff --git a/assets/blog_binops.md.Dr9-j7RW.lean.js b/assets/blog_binops.md.Dr9-j7RW.lean.js
diff --git a/assets/blog_bye-hott.md.oHSpBv52.js b/assets/blog_bye-hott.md.oHSpBv52.js
diff --git a/assets/blog_bye-hott.md.oHSpBv52.lean.js b/assets/blog_bye-hott.md.oHSpBv52.lean.js