Commit 2023-09-04 13:19 faba1c3e

View on Github →

chore: delete restate_axiom (#6939) This isn't used in Mathlib4, and wasn't useful during the port, so I think we can just drop it now.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Category/Basic.lean

Modified Mathlib/Mathport/Syntax.lean

Modified Mathlib/Tactic.lean

Deleted Mathlib/Tactic/RestateAxiom.lean

Modified scripts/style-exceptions.txt

Deleted test/restate_axiom.lean

deleted structure A