delayed calc

Stream: general

[Patrick Massot]

How hard would it be to have a version of calc with delayed proofs? I can write

refine calc
x ≤ y ↔ 0 ≤ y - x : _
  ... ↔ -(y-x) ≤ 0 : _
  ... ↔ x - y ≤ 0 : _,

and then Lean asks for three proofs but, for teaching purposes, I would like to have

calc '
x ≤ y ↔ 0 ≤ y - x
  ... ↔ -(y-x) ≤ 0
  ... ↔ x - y ≤ 0,

and then see the same three goals. It's not very important but I'd be interested if this is not too hard (and I can use a non-standard Lean if needed).

[Floris van Doorn]

we could make calc' a tactic with a custom parser. This should be doable, but I'm not sure what the best way is

• Make a custom parser which parses a list of expressions separated by ..., and with some trickery so that it parses the expressions after the first one correctly
• Make ... (or a similar token) a infix notation so that the whole thing can be parsed as a single pre-expression.
• ...