06fb4bec52
This PR wraps the top-level command parser with `withPosition` to enforce indentation in `by` blocks, combined with an empty-by fallback for better error messages. This subsumes #3215 (which introduced `withPosition commandParser` but without the empty-by fallback). It is also related to #9524, which explores elaboration with empty tactic sequences — this PR reuses that idea for the empty-by fallback, so that a `by` not followed by an indented tactic produces an elaboration error (unsolved goals) rather than a parse error. **Changes:** - `topLevelCommandParserFn` now uses `(withPosition commandParser).fn`, setting the saved position at the start of each top-level command - `tacticSeqIndentGt` gains an empty tactic sequence fallback (`pushNone`) so that missing indentation produces an elaboration error (unsolved goals) instead of a parse error - `isEmptyBy` in `goalsAt?` removed: with strict `by` indentation, empty `by` blocks parse successfully via `pushNone` (producing empty nodes) rather than producing `.missing` syntax, making the `isEmptyBy` check dead code. The `isEmpty` helper in `isSyntheticTacticCompletion` continues to work correctly because it handles both `.missing` and empty nodes from `pushNone` (via the vacuously-true `args.all isEmpty` on `#[]`) - Test files updated to indent `by` blocks and expression continuations that were previously at column 0 **Behavior:** - Top-level `by` blocks now require indentation (column > 0 for commands at column 0) - Commands indented inside `section` require proofs to be indented past the command's column - `#guard_msgs in example : True := by` works because tactic indentation is checked against the outermost command's column - Expression continuations (not just `by`) must also be indented past the command, which is slightly more strict but more consistent - `have : True := by` followed by a dedent now correctly puts `this` in scope in the outer tactic block (the `have` is structurally complete with an unsolved-goal error, rather than a parse error) **Code changes observed in practice (lean4 test suite + Mathlib):** - `by` blocks: top-level `theorem ... := by` / `decreasing_by` followed by tactics at column 0 must be indented - `variable` continuations: `variable {A : Type*} [Foo A]\n{B : Type*}` where the second line starts at column 0 must be indented (most common category in Mathlib) - Expression continuations: `def f : T :=\nexpr` or `#synth Foo\n[args]` where the body/arguments start at column 0 - Structure literals: `.symm\n{ toFun := ...` where the struct literal starts at column 0 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
52 lines
1.6 KiB
Text
52 lines
1.6 KiB
Text
opaque double : Nat → Nat
|
||
def P (n : Nat) : Prop := n >= 0
|
||
theorem pax (n : Nat) : P n := by grind [P]
|
||
def T (n : Nat) : Type := Vector Nat n
|
||
|
||
inductive Foo' (α β : Type u) : (n : Nat) → P n -> Type u
|
||
| even (a : α) (n : Nat) (v : T n) (h : P n) : Foo' α β (double n) (pax _)
|
||
| odd (b : β) (n : Nat) (v : T n) : Foo' α β (Nat.succ (double n)) (pax _)
|
||
|
||
example (α β : Type) (a₁ a₂ : α)
|
||
(n₁ n₂ : Nat)
|
||
(v₁ : T n₁) (v₂ : T n₂)
|
||
(h₁ : P n₁) (h₂ : P n₂)
|
||
(h_1 : double n₁ = double n₂)
|
||
(h_2 : Foo'.even (β := β) a₁ n₁ v₁ h₁ ≍ Foo'.even (β := β) a₂ n₂ v₂ h₂) :
|
||
a₁ = a₂ ∧ n₁ = n₂ ∧ v₁ ≍ v₂ ∧ h₁ ≍ h₂ := by
|
||
grind
|
||
|
||
example (α β : Type) (a : α) (b : β)
|
||
(n₁ n₂ : Nat)
|
||
(v₁ : T n₁) (v₂ : T n₂)
|
||
(h₁ : P n₁)
|
||
(h_1 : double n₁ = (double n₂).succ)
|
||
(h_2 : Foo'.even (β := β) a n₁ v₁ h₁ ≍ Foo'.odd (α := α) b n₂ v₂)
|
||
: False := by
|
||
grind
|
||
|
||
inductive Parity : Nat -> Type
|
||
| even (n) : Parity (double n)
|
||
| odd (n) : Parity (Nat.succ (double n))
|
||
|
||
example
|
||
(motive : (x : Nat) → Parity x → Sort u_1)
|
||
(h_2 : (j : Nat) → motive (double j) (Parity.even j))
|
||
(j n : Nat)
|
||
(heq_1 : double n = double j)
|
||
(heq_2 : Parity.even n ≍ Parity.even j):
|
||
h_2 n ≍ h_2 j := by
|
||
grind
|
||
|
||
opaque q : Nat → Nat → Prop
|
||
axiom qax : q a b → double a = double b
|
||
attribute [grind →] qax
|
||
|
||
example
|
||
(motive : (x : Nat) → Parity x → Sort u_1)
|
||
(h_2 : (j : Nat) → motive (double j) (Parity.even j))
|
||
(j n : Nat)
|
||
(heq_1 : q j n)
|
||
(heq_2 : Parity.even n ≍ Parity.even j):
|
||
h_2 n ≍ h_2 j := by
|
||
grind
|