Playground¶
This page runs Agda 2.8.0 itself. Not a recording, not a server, and not a simulation: the checker is a real Agda compiled to WebAssembly, it runs in your tab, and what it says about your proof is what it would say on a terminal.
Nothing is downloaded until you ask.
Fill the hole¶
Two Boolean values, a negation defined by the only two equations it can
have, and a claim: negating twice gets you back where you started. The ? is a hole.
Your job is to replace it.
module Main where
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
not : Bool → Bool
not true = false
not false = true
not-involutive : (b : Bool) → not (not b) ≡ b
not-involutive b = ?
Checking this needs Agda 2.8.0 compiled to WebAssembly: 9.3 MB for the checker and 49 KB for this exercise, which covers 4 compiled modules. Nothing is downloaded until you ask, and nothing you type leaves this tab.
Three hints, in order
What is b, really? It is not a value you can inspect at run time.
It is one of exactly two constructors, and Agda knows that.
Agda will not compute not (not b) until it knows which b it has.
So refl on its own cannot work: there is nothing yet to reduce.
Write one line per constructor. Replace the last line with two,
giving the proof for true and the proof for false separately.
The wrong answers teach more than the right one, and each of these is worth trying before you finish:
| What you write | What Agda says |
|---|---|
not-involutive b = refl |
not (not b) != b of type Bool. Pattern matching is what makes it compute. |
not-involutive b = not-involutive b |
a termination error. Agda will not accept a proof that assumes itself. |
not-involutive true = refl, alone |
Missing cases: not-involutive false. It names the case you forgot. |
The same lemma, as a benchmark states it¶
The exercise above is a toy in one respect: it defines its own not over
Agda's builtin Bool, so it needs no library at all. Below is the
identical claim as it appears in the benchmark behind the
research on proof automation: stated over the standard
library's Data.Bool.Base, and importing this project's own reflection
prelude, which is what a machine-generated attempt would be checked against.
It is the same proof. If you finished the first exercise you have already written the answer to this one.
It is also much heavier, and the page says so before it fetches anything: 56 standard-library modules have to come with it, and each check takes about a second instead of about a tenth of one. That difference is the whole reason the cheap exercise comes first.
module Main where
open import AgdaDojang.Debug
open import Data.Bool.Base using ( Bool ; true ; false ; not )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )
not-involutive : ∀ (b : Bool) → not (not b) ≡ b
not-involutive b = {!!}
Checking this needs Agda 2.8.0 compiled to WebAssembly: 9.3 MB for the checker and 5.8 MB for the standard library modules this one needs, which covers 73 compiled modules. Nothing is downloaded until you ask, and nothing you type leaves this tab.
What is actually running¶
The binary is agda, built for wasm32-wasi, unmodified. It declares 24
imports and they are all wasi_snapshot_preview1: no JavaScript bridge, no
threads, no shared memory. So the only thing standing between it and a
browser is a filesystem, and this page brings one, about four hundred lines
of JavaScript holding a tree of files in memory for the length of one check.
Each exercise ships as a filesystem image: a tar of exactly the sources and compiled interface files that exercise closes over. Building those interfaces ahead of time is what makes the checks fast; without them the second exercise would type-check 56 standard-library modules from scratch on every attempt. The image also carries the exact command line its interfaces were built under, and the page runs that and nothing else, because an interface compiled under different options is silently ignored rather than rejected.
Typing Agda needs Agda's input method, which is here in miniature: a
backslash, a name and a space, so \to becomes an arrow and \== becomes
the equality sign. The row of characters under the editor does the same thing
for a reader who would rather click, and names the sequence for each. It is
about a hundred and fifty of agda-input's several thousand bindings, chosen
for what this site's Agda actually writes.
What this page does not have is interaction. A hole here reports its
position; it does not show you the goal's type or its context, and there is no
refine and no case split. Those need Agda's language server rather than the
batch checker, which is a larger thing to ship and belongs where the library
being explored already lives. For the full experience, against a whole book's
worth of Agda, go to plfa.isotopy.xyz.
Three consequences worth stating plainly:
- Nothing you type leaves your browser. There is no server to send it to. Each check builds a fresh filesystem, runs the checker over it, and throws it away; nothing is stored between checks or between visits.
- Nothing is fetched until you press a button, and the button says how many bytes it is about to spend.
- With JavaScript off this page is still a page: the lemma, the hints and the table of wrong answers are all here, and there is no broken widget where the checker would be.
What it costs, measured¶
Measured in headless Chromium 153 on 2026-09-20, driving this page's own build, with the checker compiled and warm. Sizes are what crosses the wire.
| Fill the hole | The benchmark obligation | |
|---|---|---|
| the checker, once per visit | 9.3 MB | shared |
| the exercise's filesystem image | 49 KB | 5.8 MB |
| compiled interfaces shipped | 4 | 73 |
| a check, steady state | 72 to 104 ms | 1.1 to 1.3 s |
| peak WebAssembly memory | 21.9 MiB | 73.5 MiB |
Credits¶
- The WebAssembly Agda is
agda-web/agda-wasm-dist, MIT, Copyright 2024 Agda Web, shipped unmodified. The browser-side approach followsagda-web/als-demo, MIT, Copyright 2026 Andy Pan, from which no code is taken: the WASI host and the page code are this site's own. - Agda 2.8.0 and the Agda standard library 2.3, both
MIT-licensed, and the benchmark exercise's
AgdaDojangmodules from agda-native-air, Apache-2.0. Every notice the downloads require is published beside them, in the notices file. - The measurements this page was built against were taken against
plfa.isotopy.xyz, a deployment of the same checker with a full editor and interactive goals, built fromplfa-playground, MIT, Copyright 2026 Andy Pan, which grew out ofals-demo. Nothing from it is included here, and it is the place to go for the interactive experience this page does not attempt.