-
Notifications
You must be signed in to change notification settings - Fork 0
/
index.html
28 lines (26 loc) · 10.2 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
<!DOCTYPE html>
<html lang="en-US" dir="ltr">
<head>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width,initial-scale=1">
<title>Aya Prover</title>
<meta name="description" content="Website for the Aya theorem prover">
<meta name="generator" content="VitePress v1.5.0">
<link rel="preload stylesheet" href="/assets/style.CQKSSSnG.css" as="style">
<link rel="preload stylesheet" href="/vp-icons.css" as="style">
<script type="module" src="/assets/app.BCzHjXGH.js"></script>
<link rel="preload" href="/assets/inter-roman-latin.Di8DUHzh.woff2" as="font" type="font/woff2" crossorigin="">
<link rel="modulepreload" href="/assets/chunks/theme.Ci4lUjzT.js">
<link rel="modulepreload" href="/assets/chunks/framework.BcOnqcj1.js">
<link rel="modulepreload" href="/assets/index.md.A9xxfSWy.lean.js">
<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&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 class="Layout" data-v-1c81bf91><!--[--><!--]--><!--[--><span tabindex="-1" data-v-e42b5859></span><a href="#VPContent" class="VPSkipLink visually-hidden" data-v-e42b5859> Skip to content </a><!--]--><!----><header class="VPNav" data-v-1c81bf91 data-v-506251e1><div class="VPNavBar" data-v-506251e1 data-v-f9130fed><div class="wrapper" data-v-f9130fed><div class="container" data-v-f9130fed><div class="title" data-v-f9130fed><div class="VPNavBarTitle" data-v-f9130fed data-v-0775cf15><a class="title" href="/" data-v-0775cf15><!--[--><!--]--><!--[--><img class="VPImage logo" src="/logo.svg" alt data-v-d05ac4a5><!--]--><span data-v-0775cf15>Aya Prover</span><!--[--><!--]--></a></div></div><div class="content" data-v-f9130fed><div class="content-body" data-v-f9130fed><!--[--><!--]--><div class="VPNavBarSearch search" data-v-f9130fed><!--[--><!----><div id="local-search"><button type="button" class="DocSearch DocSearch-Button" aria-label="Search"><span class="DocSearch-Button-Container"><span class="vp-icon DocSearch-Search-Icon"></span><span class="DocSearch-Button-Placeholder">Search</span></span><span class="DocSearch-Button-Keys"><kbd class="DocSearch-Button-Key"></kbd><kbd class="DocSearch-Button-Key">K</kbd></span></button></div><!--]--></div><nav aria-labelledby="main-nav-aria-label" class="VPNavBarMenu menu" data-v-f9130fed data-v-6b967084><span id="main-nav-aria-label" class="visually-hidden" data-v-6b967084> Main Navigation </span><!--[--><!--[--><a class="VPLink link VPNavBarMenuLink" href="/guide/" tabindex="0" data-v-6b967084 data-v-f22e2910><!--[--><span data-v-f22e2910>Guide</span><!--]--></a><!--]--><!--[--><a class="VPLink link VPNavBarMenuLink" href="/pubs/" tabindex="0" data-v-6b967084 data-v-f22e2910><!--[--><span data-v-f22e2910>Publications</span><!--]--></a><!--]--><!--[--><a class="VPLink link VPNavBarMenuLink" href="/blog/" tabindex="0" data-v-6b967084 data-v-f22e2910><!--[--><span data-v-f22e2910>Blog</span><!--]--></a><!--]--><!--]--></nav><!----><div class="VPNavBarAppearance appearance" data-v-f9130fed data-v-0fdeee08><button class="VPSwitch VPSwitchAppearance" type="button" role="switch" title aria-checked="false" data-v-0fdeee08 data-v-1087fb40 data-v-cea599f2><span class="check" data-v-cea599f2><span class="icon" data-v-cea599f2><!--[--><span class="vpi-sun sun" data-v-1087fb40></span><span class="vpi-moon moon" data-v-1087fb40></span><!--]--></span></span></button></div><div class="VPSocialLinks VPNavBarSocialLinks social-links" data-v-f9130fed data-v-508e803b data-v-52a05ee7><!--[--><a class="VPSocialLink no-icon" href="https://github.com/aya-prover" aria-label="github" target="_blank" rel="noopener" data-v-52a05ee7 data-v-a14a0be3><span class="vpi-social-github"></span></a><!--]--></div><div class="VPFlyout VPNavBarExtra extra" data-v-f9130fed data-v-19048ef3 data-v-1df60d5f><button type="button" class="button" aria-haspopup="true" aria-expanded="false" aria-label="extra navigation" data-v-1df60d5f><span class="vpi-more-horizontal icon" data-v-1df60d5f></span></button><div class="menu" data-v-1df60d5f><div class="VPMenu" data-v-1df60d5f data-v-0a5695ee><!----><!--[--><!--[--><!----><div class="group" data-v-19048ef3><div class="item appearance" data-v-19048ef3><p class="label" data-v-19048ef3>Appearance</p><div class="appearance-action" data-v-19048ef3><button class="VPSwitch VPSwitchAppearance" type="button" role="switch" title aria-checked="false" data-v-19048ef3 data-v-1087fb40 data-v-cea599f2><span class="check" data-v-cea599f2><span class="icon" data-v-cea599f2><!--[--><span class="vpi-sun sun" data-v-1087fb40></span><span class="vpi-moon moon" data-v-1087fb40></span><!--]--></span></span></button></div></div></div><div class="group" data-v-19048ef3><div class="item social-links" data-v-19048ef3><div class="VPSocialLinks social-links-list" data-v-19048ef3 data-v-52a05ee7><!--[--><a class="VPSocialLink no-icon" href="https://github.com/aya-prover" aria-label="github" target="_blank" rel="noopener" data-v-52a05ee7 data-v-a14a0be3><span class="vpi-social-github"></span></a><!--]--></div></div></div><!--]--><!--]--></div></div></div><!--[--><!--]--><button type="button" class="VPNavBarHamburger hamburger" aria-label="mobile navigation" aria-expanded="false" aria-controls="VPNavScreen" data-v-f9130fed data-v-5b71b537><span class="container" data-v-5b71b537><span class="top" data-v-5b71b537></span><span class="middle" data-v-5b71b537></span><span class="bottom" data-v-5b71b537></span></span></button></div></div></div></div><div class="divider" data-v-f9130fed><div class="divider-line" data-v-f9130fed></div></div></div><!----></header><!----><!----><div class="VPContent is-home" id="VPContent" data-v-1c81bf91 data-v-807785d7><div class="VPHome" data-v-807785d7 data-v-9194c697><!--[--><!--[--><!--[--><div data-v-26586a7a><div class="header-img" data-v-26586a7a><div class="header-img-copyright" data-v-26586a7a><a href="https://www.pixiv.net/artworks/88666068" data-v-26586a7a>"夕"</a> © 2021 <a href="https://www.pixiv.net/users/17796967/artworks" data-v-26586a7a>PZY</a>. </div></div><div class="spacer" data-v-26586a7a></div></div><!--]--><!--]--><!--]--><div class="VPHero VPHomeHero" data-v-9194c697 data-v-47dea997><div class="container" data-v-47dea997><div class="main" data-v-47dea997><!--[--><!--]--><!--[--><h1 class="name" data-v-47dea997><span class="clip" data-v-47dea997>Aya Prover</span></h1><!----><p class="tagline" data-v-47dea997>A proof assistant designed for formalizing math and type-directed programming.</p><!--]--><!--[--><!--]--><!----><!--[--><!--]--></div><!----></div></div><!--[--><!--]--><!--[--><!--]--><!----><!--[--><!--]--><div class="vp-doc container" style="" data-v-9194c697 data-v-e2781743><!--[--><div style="position:relative;" data-v-9194c697><div></div></div><!--]--></div></div></div><!----><!--[--><!--]--></div></div>
<script>window.__VP_HASH_MAP__=JSON.parse("{\"blog_binops.md\":\"CSmB0lMK\",\"blog_bye-hott.md\":\"D7_hD73o\",\"blog_class-defeq.md\":\"2oa40eq7\",\"blog_extended-pruning.md\":\"CD4FZm90\",\"blog_ind-prop.md\":\"DCXkJUOL\",\"blog_index-unification.md\":\"K3LOkCUu\",\"blog_index.md\":\"Dd1cb5Hu\",\"blog_jit-compile.md\":\"CBZPNeAP\",\"blog_lang-exts.md\":\"BAMAIfdu\",\"blog_path-elab.md\":\"CwD-6j7l\",\"blog_pathcon-elab.md\":\"BRG2IXjM\",\"blog_redirect.md\":\"DXnf6qAR\",\"blog_tt-in-tt-qiit.md\":\"aQMDUhRG\",\"guide_fake-literate.md\":\"CwfebdMd\",\"guide_haskeller-tutorial.md\":\"CzLeuNw_\",\"guide_index.md\":\"TrBq96YC\",\"guide_install.md\":\"Dw_TeF2A\",\"guide_project-tutorial.md\":\"D-hygVJE\",\"guide_prover-tutorial.md\":\"GZ8867_l\",\"guide_readings.md\":\"D0kBwdHD\",\"guide_vscode-tutorial.md\":\"CWSehjg1\",\"index.md\":\"A9xxfSWy\",\"pubs_index.md\":\"BoLAeuOQ\"}");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>