semicolon

Stream: mathlib4

[Kevin Buzzard]

Is this not a thing any more? Or maybe I'm just doing something silly?

import Mathlib.Tactic.Basic

variables (P Q R : Prop)

example : (P → Q → R) → (P ∧ Q → R) := by
  rintro hPQR ⟨hP, hQ⟩
  apply hPQR; -- two goals
  assumption -- only closes one

[Gabriel Ebner]

It's <;> now.

[Gabriel Ebner]

The ; is the new ,.

[Kevin Buzzard]

Thanks. I've ported some files but this is the first time for a long time that I've tried to write Lean 4 code and I've forgotten a lot of what I knew; being in my 50s I find it hard to retain information which I've only learnt relatively recently and am not constantly using.

[Michael Stoll]

You're still young!

[Kevin Buzzard]

The plan was to get this system proving theorems for me so I could retire early!

[Kevin Buzzard]

Michael Stoll said:

You're still young!

It's just frustrating because once Gabriel pointed this out I remembered that I'd been told it before. I've even seen it in porting. But porting doesn't actually teach me syntax and basic stuff, as the autoporter gets all that stuff right.

[Michael Stoll]

So, porting mathlib files is not such a great way of learning Lean4 after all?

[Kevin Buzzard]

It's a great way of learning about things like the changes in simp, typeclass inference and so on! But on the other hand I couldn't prove 0 + n = n because induction n with d hd has changed, and I didn't notice this because the autoporter is dealing with that correctly and I was not reading the stuff which worked.