The editor

Before any syntax, meet the tool you’ll spend the whole tutorial in. Every Algae block on this site is a live editor running the real kernel in your browser. Here’s one — a small, already-finished proof:

import nat;
import core(refl);

lemma zero_is_zero
  ⊢ 0 = 0;
proof
  by refl(Nat, 0);
qed;

Don’t read the syntax yet

Genuinely — don’t try to parse by refl(Nat, 0) or ⊢ right now. The next few chapters build all of that up from scratch. For this chapter, the editor itself is the subject. Just click the buttons and watch what happens.

Check ▶

The Check ▶ button (or Ctrl-Enter, ⌘-Enter on a Mac) runs the kernel on whatever is in the editor. A results line appears underneath:

  • ✓ checked N proof obligation(s) — success. Every claim in the buffer holds.

  • ✗ … with red underlines — something failed. The message reads line:col  what went wrong, and the offending spot is underlined in the editor. Fix the first error first; later ones are often just fallout.

Press Check ▶ on the proof above — it’s complete, so you should see the green success line. Now change refl(Nat, 0) to refl(Nat, 1) and check again: the kernel objects, because 0 = 0 is not 1 = 1. Change it back.

Holes: wip and ?name

You rarely write a proof top-to-bottom in one go. Algae lets you leave the parts you haven’t figured out as holes, and it still checks everything around them.

  • by wip; admits a goal — it tells the kernel “trust me here for now.” A proof that leans on wip checks as in progress rather than done, and the results line says so.

  • by wip(?goal); admits the goal and prints it — the exact thing you still owe, the assumptions in scope, and a list of rules that might discharge it. Stuck? Drop in a named hole, check, and read what it asks for.

Try it: replace by refl(Nat, 0); above with by wip(?here); and press Check ▶. Instead of an error you’ll get a report of the open goal.

Suggestions

When a check flags something fixable — a hole with candidate rules, a mismatched qed/wip, or a half-applied step — the editor can offer the fix and apply it for you. Click the underlined spot (or press Ctrl-Space) to see the suggestions; pick one and it rewrites the source, then re-checks automatically so the next suggestion is ready. It’s the fastest way to make progress when you’re not sure what to type — accept a suggestion, see what the kernel says next, repeat.

Format

On the docs playground (and from the CLI) a Format button tidies a buffer: it normalises operator glyphs so, for example, the ASCII |- becomes the Unicode ⊢ and /\ becomes ∧. Every operator has both an ASCII and a Unicode spelling and they mean exactly the same thing to the kernel — type whichever you find comfortable and let Format make it pretty.

Tip

That’s the whole toolbox: Check to run the kernel, holes to leave gaps and ask questions, Suggestions to fill them, and Format to tidy up. Keep this chapter’s editor open in another tab if you like — from here on we start explaining what the proofs actually say.