3
$\begingroup$

I don't understand why #check add_mul (R := ℕ) returns add_mul : ∀ (a b c : ℕ), (a + b) * c = a * c + b * c instead of add_mul : prop. In my opinion add_mul (R := ℕ) is a proposition therefore Lean infoview should say add_mul : Prop (clearly I am wrong, and I want to know why).

$\endgroup$
2
  • $\begingroup$ Perhaps it's our naming convention that confuses you: since we don't care which element of these types we have, we just name an element after the type, instead of giving names according to the structure of the element. $\endgroup$
    – Trebor
    Commented May 21 at 8:57
  • $\begingroup$ You have two judgements here: the first one is that add_mul : ∀ (a b c : ℕ), (a + b) * c = a * c + b * c and the second one is that ∀ (a b c : ℕ), (a + b) * c = a * c + b * c : Prop $\endgroup$ Commented May 21 at 13:30

1 Answer 1

5
$\begingroup$

add_mul is a proof of ∀ (a b c : ℕ), (a + b) * c = a * c + b * c, not the proposition itself.

Consider the difference between these two:

def cat : ∀ (a b c : ℕ), (a + b) * c = a * c + b * c := by ...

def dog : Prop := ∀ (a b c : ℕ), (a + b) * c = a * c + b * c

The type of cat is ∀ (a b c : ℕ), (a + b) * c = a * c + b * c. The type of dog is Prop.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.