GitHub Actions Automated Deploy

aya-prover · Dec 5, 2024 · cb4fb78 · cb4fb78
commit cb4fb78
Show file tree

Hide file tree

Showing 95 changed files with 2,208 additions and 0 deletions.
diff --git a/404.html b/404.html
@@ -0,0 +1,25 @@
+<!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.5.0">
+    <link rel="preload stylesheet" href="/assets/style.BNdGpwCa.css" as="style">
+    <link rel="preload stylesheet" href="/vp-icons.css" as="style">
+
+    <script type="module" src="/assets/app.CYoKgUl-.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_binops.md\":\"CdTTQPUm\",\"blog_bye-hott.md\":\"ncK0HKGJ\",\"blog_class-defeq.md\":\"B5iu-E0L\",\"blog_extended-pruning.md\":\"D2UmjS6j\",\"blog_ind-prop.md\":\"gSiorRXd\",\"blog_index-unification.md\":\"8JIbTjsd\",\"blog_index.md\":\"DFYRtLrm\",\"blog_jit-compile.md\":\"C5AOmrXp\",\"blog_lang-exts.md\":\"DfBlE6eJ\",\"blog_path-elab.md\":\"DMxfi4CO\",\"blog_pathcon-elab.md\":\"qxT9XSmx\",\"blog_redirect.md\":\"dnCf5fLC\",\"blog_tt-in-tt-qiit.md\":\"CIV0yP3d\",\"guide_fake-literate.md\":\"wKOOxSKp\",\"guide_haskeller-tutorial.md\":\"F8h72bQL\",\"guide_index.md\":\"CiHHc-gO\",\"guide_install.md\":\"NmQ5a4E1\",\"guide_project-tutorial.md\":\"Brh1y7za\",\"guide_prover-tutorial.md\":\"T4MFcWK_\",\"guide_readings.md\":\"zYAL6Jj9\",\"guide_vscode-tutorial.md\":\"DiZyYf9h\",\"index.md\":\"CMxZ7gZj\",\"pubs_index.md\":\"D4yWMioC\"}");window.__VP_SITE_DATA__=JSON.parse("{\"lang\":\"en-US\",\"dir\":\"ltr\",\"title\":\"Aya Prover\",\"description\":\"Website for the Aya theorem prover\",\"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\":\"JVM JIT HOAS compiler\",\"link\":\"/blog/jit-compile\"},{\"text\":\"TT in TT using QIIT\",\"link\":\"/blog/tt-in-tt-qiit\"},{\"text\":\"Extended Pruning\",\"link\":\"/blog/extended-pruning\"},{\"text\":\"Farewell, Univalence\",\"link\":\"/blog/bye-hott\"},{\"text\":\"Impredicative Props\",\"link\":\"/blog/ind-prop\"},{\"text\":\"Def. projection in classes\",\"link\":\"/blog/class-defeq\"},{\"text\":\"Path cons. 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.CYoKgUl-.js b/assets/app.CYoKgUl-.js
diff --git a/assets/blog_binops.md.CdTTQPUm.js b/assets/blog_binops.md.CdTTQPUm.js
diff --git a/assets/blog_binops.md.CdTTQPUm.lean.js b/assets/blog_binops.md.CdTTQPUm.lean.js
diff --git a/assets/blog_bye-hott.md.ncK0HKGJ.js b/assets/blog_bye-hott.md.ncK0HKGJ.js