Skip to content

Commit 9cacab6

Browse files
shorten line
1 parent bd1074e commit 9cacab6

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

Mathlib/Topology/Defs/Basic.lean

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -198,7 +198,8 @@ scoped[Topology] notation (name := Continuous_of) "Continuous[" t₁ ", " t₂ "
198198
namespace TopologicalSpace
199199
open Topology Lean Meta PrettyPrinter.Delaborator SubExpr
200200

201-
/-- Fails iff argument #`space` has a `TopologicalSpace` instance registered and that instance is defeq to argument #`inst`. -/
201+
/-- Fails iff argument #`space` has a `TopologicalSpace` instance registered and
202+
that instance is defeq to argument #`inst`. -/
202203
def assertNonCanonical (space inst : ℕ) : DelabM Unit := do
203204
let α ← withNaryArg space getExpr
204205
let .some synthInst ← Meta.trySynthInstance (← Meta.mkAppM ``TopologicalSpace #[α]) | return ()

0 commit comments

Comments
 (0)