search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
187 stars 34 forks source link

`have` a hypothesis that has multiple premises #264

Open Qinggao1729 opened 3 weeks ago

Qinggao1729 commented 3 weeks ago

image

mul_ne_zero is defined as (a b : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0. So, in line 13, hne should be ha ∧ hb → a * succ d ≠ 0 But instead, it displays ha → hb → a * succ d ≠ 0

I encounter this problem whenever I use have to introduce a hypothesis with multiple premises.

joneugster commented 3 weeks ago

That seems corrwct as-is and how Lean works.

i.e. a "theorem" with assumptions is just another syntax to write a sequence of implications. (or foralls if they are dependent).

"And" on the other hand is a different inductive type which isnt definitionally equivalent to what's displayed

Is there anything the Natural Number Game could improve in its text which would have helped you understand better?