Commit 2026-03-10 18:38 b7cc9714

chore(Computability/Partrec): remove linter.flexible exceptions (#35682) This removes all set_option linter.flexible false from this module. Some proofs simply required moving around the usage of simp. For others I used grind, which is permitted to follow flexible tactics. In all cases I prioritized leaving the structure of the proof either mostly as-is or slightly improving readability.