Introduction

Welcome to VersoSlides — a Verso genre for building reveal.js slide presentations from Lean.

This demo exercises all the major features.

Features Overview

VersoSlides supports:

  • Elaborated Lean code blocks with hovers and info panels

  • Inline Lean expressions: elaborated and type-checked

  • Progressive proof reveals with magic comments

  • Hidden setup code and replaced expressions

  • Fragment animations (block and inline)

  • Per-slide metadata (backgrounds, transitions)

  • Speaker notes (press s on your keyboard)

Read on for examples of each.

Code Example

Here is an elaborated Lean code block:

def hello : IO Unit := do IO.println "Hello from VersoSlides!"
#check hello
hello : IO Unit

And some inline hello for good measure. Unit

Code on Light Background

A light-themed slide with Lean code:

def greet (name : String) : String := s!"Hello, {name}!" #eval greet "Lean"
"Hello, Lean!"

Proof

def replicate (n : Nat) (x : α) : List α := match n with | 0 => [] | n' + 1 => x :: replicate n' x
theorem replicate_length : ∀ {n : Nat} {x : α}, (replicate n x).length = n := by intro n
intro x induction n . grind [replicate] next n' ih =>
simp only [replicate] conv => rhs rw [← ih] simp

Proof with Hidden Setup

theorem fact_pos : ∀ n, 0 < fact n := by
intro n induction n with | zero => simp [fact]
| succ n ih => simp [fact] omega

Proof with Fragment Indices

theorem sum_to_formula : ∀ n, 2 * sum_to n = n * (n + 1) := by
intro n induction n with | zero => simp [sum_to]
| succ n ih => grind [sum_to]

Proof with Fragment Effects

def y := hiddenFunction 22
def z := 5
def zz := 22

Hidden Lean

This slide has hidden setup code.

We have α available here:

#check List α
List.{0} α : Type

But not β.

Without Panel

-- There is no info panel here def simple : Nat := 42

Replace Example

def result : Nat := ...

Other Languages

fn main() {
    let nums = vec![3, 1, 4, 1, 5, 9];
    let max = nums.iter().max().unwrap();
    println!("Max: {max}");
}

#include <iostream>
#include <vector>

int main() {
    std::vector<int> v = {1, 2, 3};
    for (auto x : v) std::cout << x << "\n";
}

Complete Modules

module import Std.Data.HashMap open Std def xs : HashMap Nat String := {}

Lake Configs

import Lake open Lake DSL require «verso-slides» from git "https://github.com/leanprover/verso-slides.git"@"main" package «etaps-tutorial» where version := v!"0.1.0" lean_lib MiniRadix

Multi-Module Examples

module public def x : Nat := 1 def y : Nat := 2
module import Lib.A def z := x /-- error: Unknown identifier `y` -/ #guard_msgs in def x' := y

Multi-Module Examples with Lakefiles

import Lake open Lake DSL package p lean_lib A
def x := "Module A!"

We can refer to x.

Fragment Styles

This block fades up.

This block also fades up, but with explicit index 2.

Here is an inline red highlight within a sentence.

And another inline blue highlight with an explicit index.

Math

\frac{dV(t)}{dt} = \delta_t\, V(t) + \pi_t - b_t - \mu_{x+t}\bigl(S_t - V(t)\bigr)

  • \delta_t is the force of interest at time t

  • \pi_t is the premium payment rate

  • b_t is the continuous benefit payment rate

  • \mu_{x+t} is the force of mortality for a life aged x + t

  • S_t is the sum payable on death at time t

Vertical Slides

This content appears on the first implicit vertical sub-slide.

Sub-slide A

This is vertical sub-slide A.

Navigate down to see the next sub-slide.

Sub-slide B

This vertical sub-slide has a custom green background.

Custom Attributes

Big text!

This paragraph has a custom id attribute.

This paragraph has a custom data-id for auto-animate matching.

Auto-Animate

Small title

Auto-Animate (cont.)

Big title

Custom Background

This slide has a purple background and uses the zoom transition.

Horizontal Stack

The :::hstack directive arranges children side by side.

Left column content.

Center column content.

Right column content.

Vertical Stack

The :::vstack directive arranges children vertically with centered alignment.

Top item.

Middle item.

Bottom item.

Stack (Overlay)

The :::stack directive overlays children on top of each other. Combine with fragments to reveal them one at a time.

First layer (visible initially).

Second layer (appears on click).

Frame

The :::frame directive adds a default styled border around content.

This paragraph is framed.

Another framed block, separately bordered.

Stretch

The :::stretch directive makes an element fill the remaining slide space.

This content stretches to fill available vertical space.

A footer line after the stretched content.

Class Directive

The :::class directive pushes one or more CSS classes onto each child block.

Custom-classed text!

Inline Class Role

The {class} role wraps inline content in a <span> with CSS classes.

This sentence has green highlighted text that appears as a fragment.

Inline ID Role

The {id} role wraps inline content with an HTML id attribute.

This word is identifiable by its ID.

Inline Attr Role

The {attr} role applies arbitrary HTML attributes to inline content.

This word has a custom data attribute.

Custom CSS

This text is styled with custom CSS injected via a css code block.

Image Role

The {image} role renders an <img> tag with configurable width and height. The path to the image is relative to the source file.

Demo image

Lean Command Role

The {leanCommand} role renders a single elaborated Lean command inline.

Here is an inline command: #check Nat.add_comm

Nat.add_comm (n m : Nat) : n + m = m + n

Diagram

LeanSource Elaborate Highlight HTML

Animation

Shape Morphing

Square

Circle

Star

Tables

Navigate down through five table examples.

Striped Rows

Column headers and striped rows on a light background.

Type

Size

Signed

Example

Nat

Unbounded

No

0, 42

Int

Unbounded

Yes

-5, 100

Float

64-bit

Yes

3.14

Striped Columns

Striped columns and row headers on a dark background.

Tactic

Closes?

Rewrites?

New goals?

exact

✓

—

—

apply

—

—

✓

intro

—

✓

—

simp

partial

✓

—

omega

✓

—

—

Row Separators

Column headers and row separators, no stripes or border.

Transition

Effect

slide

Default horizontal motion

fade

Cross-fade between slides

convex

Angled away from viewer

concave

Angled toward viewer

zoom

Zoom in from center

none

Instant cut

Bordered Table

Row separators and an outer border.

Directive

Arguments

Effect

notes

—

Speaker notes

fragment

style, index

Progressive reveal

fitText

—

Auto-sizes text to fit

stretch

—

Fills remaining slide height

hstack

—

Horizontal side-by-side layout

Propositional Connectives

Striped

(A, B)

A ∧ B

A ∨ B

A → B

A ↔ B

(T, T)

T

T

T

T

(T, F)

F

T

F

F

(F, T)

F

T

T

F

(F, F)

F

F

T

T

Thank You

That concludes the VersoSlides demo.

Questions?