Lean4
/-- `CommandStart.endPos stx` returns the position up until the `commandStart` linter checks the
formatting.
This is every declaration until the type-specification, if there is one, or the value,
as well as all `variable` commands.
-/
def endPos (stx : Syntax) : Option String.Pos :=
if let some cmd := stx.find? (#[``Parser.Command.declaration, `lemma].contains ·.getKind) then
if let some ind := cmd.find? (·.isOfKind ``Parser.Command.inductive) then
match ind.find? (·.isOfKind ``Parser.Command.optDeclSig) with
| none =>
dbg_trace"unreachable?";
none
| some sig => sig.getTailPos?
else
match cmd.find? (·.isOfKind ``Parser.Term.typeSpec) with
| some s => s[0].getTailPos?
| none =>
match cmd.find? (·.isOfKind ``Parser.Command.declValSimple) with
| some s => s.getPos?
| none => none
else if stx.isOfKind ``Parser.Command.variable || stx.isOfKind ``Parser.Command.omit then stx.getTailPos? else none
