calc tactic

Stream: general

[Mario Carneiro]

I just noticed that calc is an interactive tactic which somehow unfolds to exact calc by magic

example (x : ℕ) : x + 0 = x :=
begin
  calc x + 0 = 0 + x : add_comm _ _
         ... = x : zero_add _
end

[Mario Carneiro]

I'm not sure exactly how this works, since tactic.interactive.calc doesn't exist

[Mario Carneiro]

yep, it's hardcoded - calc turns into exact calc (https://github.com/leanprover/lean/blob/master/src/frontends/lean/tactic_notation.cpp#L273-L276)