../moving-to-verso

Moving to Verso

I vibe ported the site from Zola to Verso, keeping the anemone theme, and I think it worked out quite nicely. As a result, we can now have nice interactive Lean snippets! :)

A function and its specification

/-- Reverse a list twice, returning the original list. -/ def reverseTwice (xs : List α) : List α := xs.reverse.reverse theorem reverseTwice_eq (xs : List α) : reverseTwice xs = xs := α:Type u_1xs:List α⊢ reverseTwice xs = xs All goals completed! 🐙

Inline Lean (hover): reverseTwice [1, 2, 3, 4].

Evaluation with hidden setup

sample is defined in a hidden, checked block.

[1, 2, 3, 4]#eval reverseTwice sample 
[1, 2, 3, 4]

Proof states

Click constructor to see both goals.

example (P Q : Prop) (h : P ∧ Q) : Q ∧ P := P:PropQ:Proph:P ∧ Q⊢ Q ∧ P P:PropQ:Proph:P ∧ Q⊢ QP:PropQ:Proph:P ∧ Q⊢ P P:PropQ:Proph:P ∧ Q⊢ Q All goals completed! 🐙 P:PropQ:Proph:P ∧ Q⊢ P All goals completed! 🐙

Expected error

example : Nat := Type mismatch "not a number" has type String but is expected to have type Nat"not a number" 
Type mismatch
  "not a number"
has type
  String
but is expected to have type
  Nat