Proof terms and Curry–Howard
Behind every tactic is a term. You will write proofs as functions, pairs and projections, see how implication is a function type and conjunction a pair, and learn to read the terms Lean generates for you.
Sign in to track your progress
- An implication is a functionfun hp => hp proves P → P.9 min
- A conjunction is a pair⟨hp, hq⟩ proves P ∧ Q.8 min
- Projectionsh.1 and h.2 read the halves of a conjunction.8 min
- Compose implicationsChaining P → Q and Q → R is function composition.10 min
- Eliminate a disjunctionh.elim takes one handler per case.11 min
- Existentials as dependent pairs⟨witness, proof⟩ proves ∃ n, p n.10 min