Skip to content

Commit

Permalink
Enhance readability in VS Code (#239)
Browse files Browse the repository at this point in the history
  • Loading branch information
pitmonticone authored Sep 14, 2024
1 parent 364d319 commit dd607c6
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions MIL/C01_Introduction/S02_Overview.lean
Original file line number Diff line number Diff line change
Expand Up @@ -110,11 +110,11 @@ starting with ``--`` are comments, hence ignored by Lean:
TEXT. -/
-- QUOTE:
example : ∀ m n : Nat, Even n → Even (m * n) := by
-- Say m and n are natural numbers, and assume n=2*k.
-- Say `m` and `n` are natural numbers, and assume `n = 2 * k`.
rintro m n ⟨k, hk⟩
-- We need to prove m*n is twice a natural number. Let's show it's twice m*k.
-- We need to prove `m * n` is twice a natural number. Let's show it's twice `m * k`.
use m * k
-- Substitute for n,
-- Substitute for `n`,
rw [hk]
-- and now it's obvious.
ring
Expand Down

0 comments on commit dd607c6

Please sign in to comment.