weird calc error messages

Stream: lean4

[Eric Rodriguez]

example : 3 = 2 := by
  have h : 3 = 4 := sorry
  calc
    3 = 4 := h
    /- function expected at
  h
term has type
  3 = 4 -/
      _ = 2 := sorry

In this case, the cause of the error is that the _ is not aligned properly on the next line; this is not the case where I originally found the issue, and it's very hard indeed to debug what is going on there (still trying to minimise it). Is there any hope to make calc have better error messages than this?

[Eric Rodriguez]

Ah, the other thing is that it's very brittle; this _does_ work (and similarly in my larger example):

example : 3 = 2 := by
  have h : 3 = 4 := sorry
  calc
    3 = 4 := by exact h
      _ = 2 := sorry

[Utensil Song]

It seems that the cause is actually the term mode h.

[Eric Rodriguez]

but why? term mode works an all subsequent := ...s

[Utensil Song]

def a : Nat → (3=4) := fun b ↦ sorry

example : 3 = 4 := by
  have h : 3 = 4 := a
    1 -- works
  assumption

[Utensil Song]

Check out this #mwe without calc

[Eric Rodriguez]

This does work:

example : 3 = 2 := by
  have h : 3 = 4 := sorry
  calc
    3 = 4 := h
    _ = 2 := sorry

[Utensil Song]

def a : Nat → (3=4) := fun b ↦ sorry

example : 3 = 4 := by
  calc
    3 = 4 := a
      1 -- works

[Utensil Song]

The observation is the next line is being supplied to the term mode a in my example

[Utensil Song]

Or in your case, the next line is being supplied to the term mode h due to indentation

example : 3 = 2 := by
  have h : 3 = 4 := sorry
  calc
    /-
    function expected at
      h
    term has type
      3 = 4
    -/
    3 = 4 := h _
    _ = 2 := sorry