/- To compile:
     alectryon --frontend lean3 plain-lean3.lean # Lean → HTML; produces ‘plain-lean3.lean.html’ -/

-- Queries:
#check nat
ℕ : Type  #check bool
bool : Type

-- Proofs:
example (p q r : Prop) : p ∧ q ↔ q ∧ p :=
begin
p, q, r: Prop
p ∧ q ↔ q ∧ p
  apply iff.intro,
p, q, r: Prop
p ∧ q → q ∧ p
p, q, r: Prop
q ∧ p → p ∧ q
  intro H,
p, q, r: Prop
H: p ∧ q
q ∧ p
p, q, r: Prop
q ∧ p → p ∧ q
  apply and.intro,
p, q, r: Prop
H: p ∧ q
q
p, q, r: Prop
H: p ∧ q
p
p, q, r: Prop
q ∧ p → p ∧ q
  apply (and.elim_right H),
p, q, r: Prop
H: p ∧ q
p
p, q, r: Prop
q ∧ p → p ∧ q
  apply (and.elim_left H),
p, q, r: Prop
q ∧ p → p ∧ q
  intro H,
p, q, r: Prop
H: q ∧ p
p ∧ q
  apply and.intro,
p, q, r: Prop
H: q ∧ p
p
p, q, r: Prop
H: q ∧ p
q
  apply (and.elim_right H),
p, q, r: Prop
H: q ∧ p
q
  apply (and.elim_left H),
end