patricktree.me
forked from
danabra.mov/overreacted
my blog https://overreacted.io
nit
danabra.mov
+2
-2
public/lean-for-javascript-developers/index.md
+2
-2
public/lean-for-javascript-developers/index.md
···
162
sorry
163
```
164
165
-
A `theorem` is like a `def`, but [aimed](https://proofassistants.stackexchange.com/a/1576) specifically at declaring proofs.
166
167
-
[The declared type of a theorem is a statement that it's supposed to prove.](/beyond-booleans/#propositions-as-types) Your job is now to construct a proof of that type, and the Lean "tactic mode" (activated with `by`) provides you with an interactive and concise way to construct such proofs.
168
169
Initially, the InfoView tells you that your goal is `age + birthYear = 2025`:
170
···
162
sorry
163
```
164
165
+
A `theorem` is [like](https://proofassistants.stackexchange.com/a/1576) a `def`, but aimed specifically at declaring proofs.
166
167
+
The declared type of a theorem is a statement that it's supposed to prove. Your job is now to construct a proof of that type, and the Lean "tactic mode" (activated with `by`) provides you with an interactive and concise way to construct such proofs.
168
169
Initially, the InfoView tells you that your goal is `age + birthYear = 2025`:
170