theorem foo {g : True → False} : False := by
exact
g <| trivial
theorem foo' {g : True → False} : False := by
exact
g trivial
Lean accepts the first theorem but produces multiple errors on the second theorem. Given that tactic scripts should be indentation-sensitive, I think that both versions should produce an error.
Context
This is a minimization of a mathlib issue. In mathlib, the code looks like this:
lemma coeff_preΨ_ne_zero {n : ℤ} (h : (n : R) ≠ 0) :
(W.preΨ n).coeff ((n.natAbs ^ 2 - if Even n then 4 else 1) / 2) ≠ 0 := by
induction n using Int.negInduction with
| nat n => simpa only [preΨ_ofNat, Int.even_coe_nat]
using W.coeff_preΨ'_ne_zero <| by exact_mod_cast h
| neg n ih => simpa only [preΨ_neg, coeff_neg, neg_ne_zero, Int.natAbs_neg, even_neg]
using ih <| neg_ne_zero.mp <| by exact_mod_cast h
lemma natDegree_preΨ_pos {n : ℤ} (hn : 2 < n.natAbs) (h : (n : R) ≠ 0) :
0 < (W.preΨ n).natDegree := by
induction n using Int.negInduction with
| nat n => simpa only [preΨ_ofNat] using W.natDegree_preΨ'_pos hn <| by exact_mod_cast h
| neg n ih => simpa only [preΨ_neg, natDegree_neg]
using ih (by rwa [← Int.natAbs_neg]) <| neg_ne_zero.mp <| by exact_mod_cast h
Reducing the indentation of the final line of the second theorem causes an error. This seems confusing because the analogous line of the first theorem works fine, but it can be argued that the required indentation in the second theorem is correct and the first theorem should error.
Prerequisites
Please put an X between the brackets as you perform the following steps:
Description
Consider this code:
Lean accepts the first theorem but produces multiple errors on the second theorem. Given that tactic scripts should be indentation-sensitive, I think that both versions should produce an error.
Context
This is a minimization of a mathlib issue. In mathlib, the code looks like this:
Reducing the indentation of the final line of the second theorem causes an error. This seems confusing because the analogous line of the first theorem works fine, but it can be argued that the required indentation in the second theorem is correct and the first theorem should error.
Steps to Reproduce
Versions
4.11.0-nightly-2024-07-23 on live.lean-lang.org
Impact
Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.