Can't express 2 + 2 + 4?

Stream: general

[Marvin]

Hi all. I'm new and likely making a silly mistake. Im trying to express the proposition that 2+2=4 (preferably as a Prop and not as a Bool). But even without specifying prop or bool, the expression itself fails.

def p := 2 + 2 = 4

failed to synthesize instance of type class
  OfNat (N → P) 2
numerals are polymorphic in Lean, but the numeral `2` cannot be used in a context where the expected type is
  N → P
due to the absence of the instance above

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

[Johan Commelin]

Welcome!

The error message is referring to N and P. Looks like we're missing context. Please prepare a #mwe

Orthogonally: do you want to prove 2 + 2 = 4? Or do you want to "store" that claim as a "variable"? You are currently doing the latter.

[Johan Commelin]

I'm writing "variable" in quotes, because really, you're creating a named definition.

Mainly, I want to draw your attention to the fact that 2 + 2 = 4 is the value, and not the type, in your declaration.

[Marvin]

I want to store "2 + 2 = 4" as a claim (proposition, which P is an abbreviation for, sorry, and N is just some atomic type representing "thing")

[Marvin]

I'm not sure why P and N are even being picked up here, I define them somewhere else

[Marvin]

axiom N : Type
abbrev P := Prop

def p := 2 + 2 = 4

[Marvin]

Huh, it works if I put this in a new file...

[Kevin Buzzard]

If you had tried to make a #mwe before posting then you would have been well on the way to answering your own question before you even asked it :-) That just shows the importance of these minimal examples. Now start deleting stuff in your code until it works and then you've answered your own question.

[Marvin]

Sorry, I thought that

def p := 2 + 2 = 4

on it's own was complete since I didn't invoke any of my custom stuff like P or N, I didn't realize those were interfering with the normal interpretation (they are defined in a different file entirely). I should have looked closer at the error message

[Yaël Dillies]

It is always useful to click on the button in the top right of your own code snippet to check whether the error is being reproduced

[Marvin]

I see, thanks!