Built with
Alectryon , running Lean4. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
/- To compile:
alectryon --frontend lean4 plain-lean4.lean # Lean → HTML; produces ‘plain-lean4.lean.html’ -/
-- Queries:
#check Nat #check Bool
-- Proofs:
theorem test (p q : Prop ) (hp : p) (hq : q): p ∧ q ↔ q ∧ p := by
p, q : Prop hp : p hq : q
p ∧ q ↔ q ∧ p
apply Iff.intro p, q : Prop hp : p hq : q
mp p ∧ q → q ∧ p
p, q : Prop hp : p hq : q
p ∧ q ↔ q ∧ p
. p, q : Prop hp : p hq : q
mp p ∧ q → q ∧ p
p, q : Prop hp : p hq : q
mp p ∧ q → q ∧ p
intro h p, q : Prop hp : p hq : q h : p ∧ q
mp q ∧ p
p, q : Prop hp : p hq : q
mp p ∧ q → q ∧ p
apply And.intro p, q : Prop hp : p hq : q h : p ∧ q
mp.left q
p, q : Prop hp : p hq : q
mp p ∧ q → q ∧ p
. p, q : Prop hp : p hq : q h : p ∧ q
mp.left q
p, q : Prop hp : p hq : q h : p ∧ q
mp.left q
exact hq
p, q : Prop hp : p hq : q
mp p ∧ q → q ∧ p
. p, q : Prop hp : p hq : q h : p ∧ q
mp.right p
p, q : Prop hp : p hq : q h : p ∧ q
mp.right p
exact hp
p, q : Prop hp : p hq : q
p ∧ q ↔ q ∧ p
. p, q : Prop hp : p hq : q
mpr q ∧ p → p ∧ q
p, q : Prop hp : p hq : q
mpr q ∧ p → p ∧ q
intro h p, q : Prop hp : p hq : q h : q ∧ p
mpr p ∧ q
p, q : Prop hp : p hq : q
mpr q ∧ p → p ∧ q
apply And.intro p, q : Prop hp : p hq : q h : q ∧ p
mpr.left p
p, q : Prop hp : p hq : q
mpr q ∧ p → p ∧ q
. p, q : Prop hp : p hq : q h : q ∧ p
mpr.left p
p, q : Prop hp : p hq : q h : q ∧ p
mpr.left p
exact hp
p, q : Prop hp : p hq : q
mpr q ∧ p → p ∧ q
. p, q : Prop hp : p hq : q h : q ∧ p
mpr.right q
p, q : Prop hp : p hq : q h : q ∧ p
mpr.right q
exact hq