3 ms·
How does this work? I'm on step 1 and I typed in "rfl 37=37" and nothing happened. I'm not a coder
by hammock 2y ago
How does this work? I'm on step 1 and I typed in "rfl 37=37" and nothing happened. I'm not a coder
- sn9 2y agoYou can just type in `rfl` to assert that `37 = 37` (or anything of the form `X = X`).
- hammock 2y agoI typed in rfl and hit execute and nothing happened (it added a line above but did not say I solved anything)
- lupire 2y agoYou only type in the reasons, not the results. Lean computes the result for you. Otherwise, if you do all the work yourself, you wouldn't need Lean :-)
- hammock 2y agoI still am completely lost. Can you give me the answer so I can see what input is supposed to look like? In my head I want to solve it with 37=37, x=x and q=q. And then run rfl
- sn9 2y agoIf it shows you something of the form `X=X` like `37=37`, you then type in `rfl` to assert that they are equal by the reflective property which completes the proof.