patricktree.me
forked from
danabra.mov/overreacted
my blog https://overreacted.io
oopsie
danabra.mov
+1
-1
public/lean-for-javascript-developers/index.md
+1
-1
public/lean-for-javascript-developers/index.md
···
569
569
570
570
These proofs typecheck, but there's a feeling that it's not any better than writing tests. What we're hoping to capture is a *universal pattern*, not a bunch of cases.
571
571
572
-
The fact is, no matter what `cy` (I'll shorten "current year" to that) and `a` (short for "age") are, `birthYear cy a` is supposed to be equal to `cy`. Let's capture that:
572
+
The fact is, no matter what `cy` (I'll shorten "current year" to that) and `a` (short for "age") are, `a + birthYear cy a` should be equal to `cy`. Let's capture that:
573
573
574
574
```lean {6-7}
575
575
def name := "Alice"