Skip to content

Commit 73dcb81

Browse files
committed
more fix
1 parent fc5f646 commit 73dcb81

File tree

1 file changed

+1
-1
lines changed
  • Mathlib/FieldTheory/IntermediateField/Adjoin

1 file changed

+1
-1
lines changed

Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -521,7 +521,7 @@ scoped macro:max K:term "⟮" xs:term,* "⟯" : term => do ``(adjoin $K $(← mk
521521

522522
open Lean PrettyPrinter.Delaborator SubExpr in
523523
@[app_delab IntermediateField.adjoin]
524-
meta def delabAdjoinNotation : Delab := whenPPOption getPPNotation do
524+
meta partial def delabAdjoinNotation : Delab := whenPPOption getPPNotation do
525525
let e ← getExpr
526526
guard <| e.isAppOfArity ``adjoin 6
527527
let F ← withNaryArg 0 delab

0 commit comments

Comments
 (0)